1.1 --- a/doc-src/TutorialI/CTL/document/Base.tex	Thu Jul 26 16:08:16 2012 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,130 +0,0 @@
     1.4 -%
     1.5 -\begin{isabellebody}%
     1.6 -\def\isabellecontext{Base}%
     1.7 -%
     1.8 -\isadelimtheory
     1.9 -%
    1.10 -\endisadelimtheory
    1.11 -%
    1.12 -\isatagtheory
    1.13 -%
    1.14 -\endisatagtheory
    1.15 -{\isafoldtheory}%
    1.16 -%
    1.17 -\isadelimtheory
    1.18 -%
    1.19 -\endisadelimtheory
    1.20 -%
    1.21 -\isamarkupsection{Case Study: Verified Model Checking%
    1.22 -}
    1.23 -\isamarkuptrue%
    1.24 -%
    1.25 -\begin{isamarkuptext}%
    1.26 -\label{sec:VMC}
    1.27 -This chapter ends with a case study concerning model checking for 
    1.28 -Computation Tree Logic (CTL), a temporal logic.
    1.29 -Model checking is a popular technique for the verification of finite
    1.30 -state systems (implementations) with respect to temporal logic formulae
    1.31 -(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic
    1.32 -and this section will explore them in HOL\@. This is done in two steps.  First
    1.33 -we consider a simple modal logic called propositional dynamic
    1.34 -logic (PDL)\@.  We then proceed to the temporal logic CTL, which is
    1.35 -used in many real
    1.36 -model checkers. In each case we give both a traditional semantics (\isa{{\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}}) and a
    1.37 -recursive function \isa{mc} that maps a formula into the set of all states of
    1.38 -the system where the formula is valid. If the system has a finite number of
    1.39 -states, \isa{mc} is directly executable: it is a model checker, albeit an
    1.40 -inefficient one. The main proof obligation is to show that the semantics
    1.41 -and the model checker agree.
    1.42 -
    1.43 -\underscoreon
    1.44 -
    1.45 -Our models are \emph{transition systems}:\index{transition systems}
    1.46 -sets of \emph{states} with
    1.47 -transitions between them.  Here is a simple example:
    1.48 -\begin{center}
    1.49 -\unitlength.5mm
    1.50 -\thicklines
    1.51 -\begin{picture}(100,60)
    1.52 -\put(50,50){\circle{20}}
    1.53 -\put(50,50){\makebox(0,0){$p,q$}}
    1.54 -\put(61,55){\makebox(0,0)[l]{$s_0$}}
    1.55 -\put(44,42){\vector(-1,-1){26}}
    1.56 -\put(16,18){\vector(1,1){26}}
    1.57 -\put(57,43){\vector(1,-1){26}}
    1.58 -\put(10,10){\circle{20}}
    1.59 -\put(10,10){\makebox(0,0){$q,r$}}
    1.60 -\put(-1,15){\makebox(0,0)[r]{$s_1$}}
    1.61 -\put(20,10){\vector(1,0){60}}
    1.62 -\put(90,10){\circle{20}}
    1.63 -\put(90,10){\makebox(0,0){$r$}}
    1.64 -\put(98, 5){\line(1,0){10}}
    1.65 -\put(108, 5){\line(0,1){10}}
    1.66 -\put(108,15){\vector(-1,0){10}}
    1.67 -\put(91,21){\makebox(0,0)[bl]{$s_2$}}
    1.68 -\end{picture}
    1.69 -\end{center}
    1.70 -Each state has a unique name or number ($s_0,s_1,s_2$), and in each state
    1.71 -certain \emph{atomic propositions} ($p,q,r$) hold.  The aim of temporal logic
    1.72 -is to formalize statements such as ``there is no path starting from $s_2$
    1.73 -leading to a state where $p$ or $q$ holds,'' which is true, and ``on all paths
    1.74 -starting from $s_0$, $q$ always holds,'' which is false.
    1.75 -
    1.76 -Abstracting from this concrete example, we assume there is a type of
    1.77 -states:%
    1.78 -\end{isamarkuptext}%
    1.79 -\isamarkuptrue%
    1.80 -\isacommand{typedecl}\isamarkupfalse%
    1.81 -\ state%
    1.82 -\begin{isamarkuptext}%
    1.83 -\noindent
    1.84 -Command \commdx{typedecl} merely declares a new type but without
    1.85 -defining it (see \S\ref{sec:typedecl}). Thus we know nothing
    1.86 -about the type other than its existence. That is exactly what we need
    1.87 -because \isa{state} really is an implicit parameter of our model.  Of
    1.88 -course it would have been more generic to make \isa{state} a type
    1.89 -parameter of everything but declaring \isa{state} globally as above
    1.90 -reduces clutter.  Similarly we declare an arbitrary but fixed
    1.91 -transition system, i.e.\ a relation between states:%
    1.92 -\end{isamarkuptext}%
    1.93 -\isamarkuptrue%
    1.94 -\isacommand{consts}\isamarkupfalse%
    1.95 -\ M\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}state\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ state{\isaliteral{29}{\isacharparenright}}set{\isaliteral{22}{\isachardoublequoteclose}}%
    1.96 -\begin{isamarkuptext}%
    1.97 -\noindent
    1.98 -This is Isabelle's way of declaring a constant without defining it.
    1.99 -Finally we introduce a type of atomic propositions%
   1.100 -\end{isamarkuptext}%
   1.101 -\isamarkuptrue%
   1.102 -\isacommand{typedecl}\isamarkupfalse%
   1.103 -\ {\isaliteral{22}{\isachardoublequoteopen}}atom{\isaliteral{22}{\isachardoublequoteclose}}%
   1.104 -\begin{isamarkuptext}%
   1.105 -\noindent
   1.106 -and a \emph{labelling function}%
   1.107 -\end{isamarkuptext}%
   1.108 -\isamarkuptrue%
   1.109 -\isacommand{consts}\isamarkupfalse%
   1.110 -\ L\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ atom\ set{\isaliteral{22}{\isachardoublequoteclose}}%
   1.111 -\begin{isamarkuptext}%
   1.112 -\noindent
   1.113 -telling us which atomic propositions are true in each state.%
   1.114 -\end{isamarkuptext}%
   1.115 -\isamarkuptrue%
   1.116 -%
   1.117 -\isadelimtheory
   1.118 -%
   1.119 -\endisadelimtheory
   1.120 -%
   1.121 -\isatagtheory
   1.122 -%
   1.123 -\endisatagtheory
   1.124 -{\isafoldtheory}%
   1.125 -%
   1.126 -\isadelimtheory
   1.127 -%
   1.128 -\endisadelimtheory
   1.129 -\end{isabellebody}%
   1.130 -%%% Local Variables:
   1.131 -%%% mode: latex
   1.132 -%%% TeX-master: "root"
   1.133 -%%% End: