| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/Doc/Tutorial/CTL/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 3 kB |
|
Quelle Base.thy Sprache: Isabelle |
|||||||||
|
(*<*)theory Base imports Main begin(*>*)
section\<open>Case Study: Verified Model Checking\<close> text\<open>\label{sec:VMC} This chapter ends with a case study concerning model checking for Computation Tree Logic (CTL), a temporal logic. Model checking is a popular technique for the verification of finite state systems (implementations) with respect to temporal logic formulae (specifications) \<^cite>\<open>"ClarkeGP-book" and "Huth-Ryan-book"\<close>. Its foundatio and this section will explore them in HOL\@. This is done in two steps. First we consider a simple modal logic called propositional dynamic logic (PDL)\@. We then proceed to the temporal logic CTL, which is used in many real model checkers. In each case we give both a traditional semantics (\<open>\<Turnstile>\<close>) an recursive function \<^term>\<open>mc\<close> that maps a formula into the set of all states of the system where the formula is valid. If the system has a finite number of states, \<^term>\<open>mc\<close> is directly executable: it is a model checker, albeit an inefficient one. The main proof obligation is to show that the semantics and the model checker agree. \underscoreon Our models are \emph{transition systems}:\index{transition systems} sets of \emph{states} with transitions between them. Here is a simple example: \begin{center} \unitlength.5mm \thicklines \begin{picture}(100,60) \put(50,50){\circle{20}} \put(50,50){\makebox(0,0){$p,q$}} \put(61,55){\makebox(0,0)[l]{$s_0$}} \put(44,42){\vector(-1,-1){26}} \put(16,18){\vector(1,1){26}} \put(57,43){\vector(1,-1){26}} \put(10,10){\circle{20}} \put(10,10){\makebox(0,0){$q,r$}} \put(-1,15){\makebox(0,0)[r]{$s_1$}} \put(20,10){\vector(1,0){60}} \put(90,10){\circle{20}} \put(90,10){\makebox(0,0){$r$}} \put(98, 5){\line(1,0){10}} \put(108, 5){\line(0,1){10}} \put(108,15){\vector(-1,0){10}} \put(91,21){\makebox(0,0)[bl]{$s_2$}} \end{picture} \end{center} Each state has a unique name or number ($s_0,s_1,s_2$), and in each state certain \emph{atomic propositions} ($p,q,r$) hold. The aim of temporal logic is to formalize statements such as ``there is no path starting from $s_2$ leading to a state where $p$ or $q$ holds,'' which is true, and ``on all paths starting from $s_0$, $q$ always holds,'' which is false. Abstracting from this concrete example, we assume there is a type of states: \<close> typedecl state text\<open>\noindent Command \commdx{typedecl} merely declares a new type but without defining it (see \S\ref{sec:typedecl}). Thus we know nothing about the type other than its existence. That is exactly what we need because \<^typ>\<open>state\<close> really is an implicit parameter of our model. Of course it would have been more generic to make \<^typ>\<open>state\<close> a type parameter of everything but declaring \<^typ>\<open>state\<close> globally as above reduces clutter. Similarly we declare an arbitrary but fixed transition system, i.e.\ a relation between states: \<close> consts M :: "(state \ text\<open>\noindent This is Isabelle's way of declaring a constant without defining it. Finally we introduce a type of atomic propositions \<close> typedecl "atom" text\<open>\noindent and a \emph{labelling function} \<close> consts L :: "state \ text\<open>\noindent telling us which atomic propositions are true in each state. \<close> (*<*)end(*>*) ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28