doc-src/TutorialI/CTL/Base.thy
author nipkow
Wed Dec 06 13:22:58 2000 +0100 (2000-12-06)
changeset 10608 620647438780
parent 10362 c6b197ccf1f1
child 10795 9e888d60d3e5
permissions -rw-r--r--
*** empty log message ***
     1 (*<*)theory Base = Main:(*>*)
     2 
     3 section{*Case study: Verified model checking*}
     4 
     5 text{*\label{sec:VMC}
     6 Model checking is a very popular technique for the verification of finite
     7 state systems (implementations) w.r.t.\ temporal logic formulae
     8 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
     9 and this section shall explore them a little in HOL. This is done in two steps: first
    10 we consider a simple modal logic called propositional dynamic
    11 logic (PDL) which we then extend to the temporal logic CTL used in many real
    12 model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a
    13 recursive function @{term mc} that maps a formula into the set of all states of
    14 the system where the formula is valid. If the system has a finite number of
    15 states, @{term mc} is directly executable, i.e.\ a model checker, albeit not a
    16 very efficient one. The main proof obligation is to show that the semantics
    17 and the model checker agree.
    18 
    19 \underscoreon
    20 
    21 Our models are \emph{transition systems}, i.e.\ sets of \emph{states} with
    22 transitions between them, as shown in this simple example:
    23 \begin{center}
    24 \unitlength.5mm
    25 \thicklines
    26 \begin{picture}(100,60)
    27 \put(50,50){\circle{20}}
    28 \put(50,50){\makebox(0,0){$p,q$}}
    29 \put(61,55){\makebox(0,0)[l]{$s_0$}}
    30 \put(44,42){\vector(-1,-1){26}}
    31 \put(16,18){\vector(1,1){26}}
    32 \put(57,43){\vector(1,-1){26}}
    33 \put(10,10){\circle{20}}
    34 \put(10,10){\makebox(0,0){$q,r$}}
    35 \put(-1,15){\makebox(0,0)[r]{$s_1$}}
    36 \put(20,10){\vector(1,0){60}}
    37 \put(90,10){\circle{20}}
    38 \put(90,10){\makebox(0,0){$r$}}
    39 \put(98, 5){\line(1,0){10}}
    40 \put(108, 5){\line(0,1){10}}
    41 \put(108,15){\vector(-1,0){10}}
    42 \put(91,21){\makebox(0,0)[bl]{$s_2$}}
    43 \end{picture}
    44 \end{center}
    45 Each state has a unique name or number ($s_0,s_1,s_2$), and in each
    46 state certain \emph{atomic propositions} ($p,q,r$) are true.
    47 The aim of temporal logic is to formalize statements such as ``there is no
    48 path starting from $s_2$ leading to a state where $p$ or $q$
    49 are true'', which is true, and ``on all paths starting from $s_0$ $q$ is always true'',
    50 which is false.
    51 
    52 Abstracting from this concrete example, we assume there is some type of
    53 states:
    54 *}
    55 
    56 typedecl state
    57 
    58 text{*\noindent
    59 Command \isacommand{typedecl} merely declares a new type but without
    60 defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
    61 about the type other than its existence. That is exactly what we need
    62 because @{typ state} really is an implicit parameter of our model.  Of
    63 course it would have been more generic to make @{typ state} a type
    64 parameter of everything but declaring @{typ state} globally as above
    65 reduces clutter.  Similarly we declare an arbitrary but fixed
    66 transition system, i.e.\ relation between states:
    67 *}
    68 
    69 consts M :: "(state \<times> state)set";
    70 
    71 text{*\noindent
    72 Again, we could have made @{term M} a parameter of everything.
    73 Finally we introduce a type of atomic propositions
    74 *}
    75 
    76 typedecl atom
    77 
    78 text{*\noindent
    79 and a \emph{labelling function}
    80 *}
    81 
    82 consts L :: "state \<Rightarrow> atom set"
    83 
    84 text{*\noindent
    85 telling us which atomic propositions are true in each state.
    86 *}
    87 
    88 (*<*)end(*>*)