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(*>*)