14 the system where the formula is valid. If the system has a finite number 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 |
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 |
16 very efficient one. The main proof obligation is to show that the semantics |
17 and the model checker agree. |
17 and the model checker agree. |
18 |
18 |
19 Our models are transition systems. |
19 \underscoreon |
20 |
20 |
21 START with simple example: mutex or something. |
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 transition sequence starting from $s_2$ leading to a state where $p$ or $q$ |
|
49 are true''. |
22 |
50 |
23 Abstracting from this concrete example, we assume there is some type of |
51 Abstracting from this concrete example, we assume there is some type of |
24 atomic propositions |
52 states |
25 *} |
53 *} |
26 |
54 |
27 typedecl atom |
55 typedecl state |
28 |
56 |
29 text{*\noindent |
57 text{*\noindent |
30 which we merely declare rather than define because it is an implicit parameter of our model. |
58 which we merely declare rather than define because it is an implicit |
31 Of course it would have been more generic to make @{typ atom} a type parameter of everything |
59 parameter of our model. Of course it would have been more generic to make |
32 but fixing @{typ atom} as above reduces clutter. |
60 @{typ state} a type parameter of everything but fixing @{typ state} as above |
33 |
61 reduces clutter. |
34 Instead of introducing both a separate type of states and a function |
62 Similarly we declare an arbitrary but fixed transition system, i.e.\ |
35 telling us which atoms are true in each state we simply identify each |
63 relation between states: |
36 state with that set of atoms: |
|
37 *} |
|
38 |
|
39 types state = "atom set"; |
|
40 |
|
41 text{*\noindent |
|
42 Finally we declare an arbitrary but fixed transition system, i.e.\ relation between states: |
|
43 *} |
64 *} |
44 |
65 |
45 consts M :: "(state \<times> state)set"; |
66 consts M :: "(state \<times> state)set"; |
46 |
67 |
47 text{*\noindent |
68 text{*\noindent |
48 Again, we could have made @{term M} a parameter of everything. |
69 Again, we could have made @{term M} a parameter of everything. |
|
70 Finally we introduce a type of atomic propositions |
49 *} |
71 *} |
|
72 |
|
73 typedecl atom |
|
74 |
|
75 text{*\noindent |
|
76 and a \emph{labelling function} |
|
77 *} |
|
78 |
|
79 consts L :: "state \<Rightarrow> atom set" |
|
80 |
|
81 text{*\noindent |
|
82 telling us which atomic propositions are true in each state. |
|
83 *} |
|
84 |
50 (*<*)end(*>*) |
85 (*<*)end(*>*) |