src/Doc/Tutorial/CTL/Base.thy
 author wenzelm Sat Nov 01 14:20:38 2014 +0100 (2014-11-01) changeset 58860 fee7cfa69c50 parent 58620 7435b6a3f72e child 67406 23307fd33906 permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*<*)theory Base imports Main begin(*>*)

     2

     3 section{*Case Study: Verified Model Checking*}

     4

     5 text{*\label{sec:VMC}

     6 This chapter ends with a case study concerning model checking for

     7 Computation Tree Logic (CTL), a temporal logic.

     8 Model checking is a popular technique for the verification of finite

     9 state systems (implementations) with respect to temporal logic formulae

    10 (specifications) @{cite "ClarkeGP-book" and "Huth-Ryan-book"}. Its foundations are set theoretic

    11 and this section will explore them in HOL\@. This is done in two steps.  First

    12 we consider a simple modal logic called propositional dynamic

    13 logic (PDL)\@.  We then proceed to the temporal logic CTL, which is

    14 used in many real

    15 model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a

    16 recursive function @{term mc} that maps a formula into the set of all states of

    17 the system where the formula is valid. If the system has a finite number of

    18 states, @{term mc} is directly executable: it is a model checker, albeit an

    19 inefficient one. The main proof obligation is to show that the semantics

    20 and the model checker agree.

    21

    22 \underscoreon

    23

    24 Our models are \emph{transition systems}:\index{transition systems}

    25 sets of \emph{states} with

    26 transitions between them.  Here is a simple example:

    27 \begin{center}

    28 \unitlength.5mm

    29 \thicklines

    30 \begin{picture}(100,60)

    31 \put(50,50){\circle{20}}

    32 \put(50,50){\makebox(0,0){$p,q$}}

    33 \put(61,55){\makebox(0,0)[l]{$s_0$}}

    34 \put(44,42){\vector(-1,-1){26}}

    35 \put(16,18){\vector(1,1){26}}

    36 \put(57,43){\vector(1,-1){26}}

    37 \put(10,10){\circle{20}}

    38 \put(10,10){\makebox(0,0){$q,r$}}

    39 \put(-1,15){\makebox(0,0)[r]{$s_1$}}

    40 \put(20,10){\vector(1,0){60}}

    41 \put(90,10){\circle{20}}

    42 \put(90,10){\makebox(0,0){$r$}}

    43 \put(98, 5){\line(1,0){10}}

    44 \put(108, 5){\line(0,1){10}}

    45 \put(108,15){\vector(-1,0){10}}

    46 \put(91,21){\makebox(0,0)[bl]{$s_2$}}

    47 \end{picture}

    48 \end{center}

    49 Each state has a unique name or number ($s_0,s_1,s_2$), and in each state

    50 certain \emph{atomic propositions} ($p,q,r$) hold.  The aim of temporal logic

    51 is to formalize statements such as there is no path starting from $s_2$

    52 leading to a state where $p$ or $q$ holds,'' which is true, and on all paths

    53 starting from $s_0$, $q$ always holds,'' which is false.

    54

    55 Abstracting from this concrete example, we assume there is a type of

    56 states:

    57 *}

    58

    59 typedecl state

    60

    61 text{*\noindent

    62 Command \commdx{typedecl} merely declares a new type but without

    63 defining it (see \S\ref{sec:typedecl}). Thus we know nothing

    64 about the type other than its existence. That is exactly what we need

    65 because @{typ state} really is an implicit parameter of our model.  Of

    66 course it would have been more generic to make @{typ state} a type

    67 parameter of everything but declaring @{typ state} globally as above

    68 reduces clutter.  Similarly we declare an arbitrary but fixed

    69 transition system, i.e.\ a relation between states:

    70 *}

    71

    72 consts M :: "(state \<times> state)set"

    73

    74 text{*\noindent

    75 This is Isabelle's way of declaring a constant without defining it.

    76 Finally we introduce a type of atomic propositions

    77 *}

    78

    79 typedecl "atom"

    80

    81 text{*\noindent

    82 and a \emph{labelling function}

    83 *}

    84

    85 consts L :: "state \<Rightarrow> atom set"

    86

    87 text{*\noindent

    88 telling us which atomic propositions are true in each state.

    89 *}

    90

    91 (*<*)end(*>*)