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