src/Doc/Tutorial/CTL/Base.thy
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 48985 5386df44a037
child 58620 7435b6a3f72e
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17914
99ead7a7eb42 fix headers;
wenzelm
parents: 11458
diff changeset
     1
(*<*)theory Base imports Main begin(*>*)
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
     2
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10795
diff changeset
     3
section{*Case Study: Verified Model Checking*}
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
     4
10362
c6b197ccf1f1 *** empty log message ***
nipkow
parents: 10281
diff changeset
     5
text{*\label{sec:VMC}
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10795
diff changeset
     6
This chapter ends with a case study concerning model checking for 
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10795
diff changeset
     7
Computation Tree Logic (CTL), a temporal logic.
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10795
diff changeset
     8
Model checking is a popular technique for the verification of finite
10795
9e888d60d3e5 minor edits to Chapters 1-3
paulson
parents: 10362
diff changeset
     9
state systems (implementations) with respect to temporal logic formulae
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10795
diff changeset
    10
(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10795
diff changeset
    11
and this section will explore them in HOL\@. This is done in two steps.  First
10178
aecb5bf6f76f *** empty log message ***
nipkow
parents: 10133
diff changeset
    12
we consider a simple modal logic called propositional dynamic
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 10983
diff changeset
    13
logic (PDL)\@.  We then proceed to the temporal logic CTL, which is
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10795
diff changeset
    14
used in many real
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    15
model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    16
recursive function @{term mc} that maps a formula into the set of all states of
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    17
the system where the formula is valid. If the system has a finite number of
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10795
diff changeset
    18
states, @{term mc} is directly executable: it is a model checker, albeit an
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10795
diff changeset
    19
inefficient one. The main proof obligation is to show that the semantics
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    20
and the model checker agree.
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    21
10133
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    22
\underscoreon
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    23
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 10983
diff changeset
    24
Our models are \emph{transition systems}:\index{transition systems}
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 10983
diff changeset
    25
sets of \emph{states} with
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 10983
diff changeset
    26
transitions between them.  Here is a simple example:
10133
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    27
\begin{center}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    28
\unitlength.5mm
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    29
\thicklines
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    30
\begin{picture}(100,60)
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    31
\put(50,50){\circle{20}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    32
\put(50,50){\makebox(0,0){$p,q$}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    33
\put(61,55){\makebox(0,0)[l]{$s_0$}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    34
\put(44,42){\vector(-1,-1){26}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    35
\put(16,18){\vector(1,1){26}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    36
\put(57,43){\vector(1,-1){26}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    37
\put(10,10){\circle{20}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    38
\put(10,10){\makebox(0,0){$q,r$}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    39
\put(-1,15){\makebox(0,0)[r]{$s_1$}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    40
\put(20,10){\vector(1,0){60}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    41
\put(90,10){\circle{20}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    42
\put(90,10){\makebox(0,0){$r$}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    43
\put(98, 5){\line(1,0){10}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    44
\put(108, 5){\line(0,1){10}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    45
\put(108,15){\vector(-1,0){10}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    46
\put(91,21){\makebox(0,0)[bl]{$s_2$}}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    47
\end{picture}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    48
\end{center}
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 10983
diff changeset
    49
Each state has a unique name or number ($s_0,s_1,s_2$), and in each state
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 10983
diff changeset
    50
certain \emph{atomic propositions} ($p,q,r$) hold.  The aim of temporal logic
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 10983
diff changeset
    51
is to formalize statements such as ``there is no path starting from $s_2$
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 10983
diff changeset
    52
leading to a state where $p$ or $q$ holds,'' which is true, and ``on all paths
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 10983
diff changeset
    53
starting from $s_0$, $q$ always holds,'' which is false.
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    54
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 10983
diff changeset
    55
Abstracting from this concrete example, we assume there is a type of
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10192
diff changeset
    56
states:
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    57
*}
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    58
10133
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    59
typedecl state
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    60
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    61
text{*\noindent
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 10983
diff changeset
    62
Command \commdx{typedecl} merely declares a new type but without
10983
59961d32b1ae *** empty log message ***
nipkow
parents: 10867
diff changeset
    63
defining it (see \S\ref{sec:typedecl}). Thus we know nothing
10281
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10192
diff changeset
    64
about the type other than its existence. That is exactly what we need
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10192
diff changeset
    65
because @{typ state} really is an implicit parameter of our model.  Of
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10192
diff changeset
    66
course it would have been more generic to make @{typ state} a type
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10192
diff changeset
    67
parameter of everything but declaring @{typ state} globally as above
9554ce1c2e54 *** empty log message ***
nipkow
parents: 10192
diff changeset
    68
reduces clutter.  Similarly we declare an arbitrary but fixed
10867
bda1701848cd lcp's suggestions for CTL
paulson
parents: 10795
diff changeset
    69
transition system, i.e.\ a relation between states:
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    70
*}
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    71
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    72
consts M :: "(state \<times> state)set";
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    73
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    74
text{*\noindent
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 18724
diff changeset
    75
This is Isabelle's way of declaring a constant without defining it.
10133
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    76
Finally we introduce a type of atomic propositions
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    77
*}
10133
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    78
18724
cb6e0064c88c quote "atom";
wenzelm
parents: 17914
diff changeset
    79
typedecl "atom"
10133
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    80
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    81
text{*\noindent
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    82
and a \emph{labelling function}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    83
*}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    84
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    85
consts L :: "state \<Rightarrow> atom set"
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    86
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    87
text{*\noindent
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    88
telling us which atomic propositions are true in each state.
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    89
*}
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset
    90
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset
    91
(*<*)end(*>*)