summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/TutorialI/CTL/Base.thy

author | nipkow |

Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) | |

changeset 10608 | 620647438780 |

parent 10362 | c6b197ccf1f1 |

child 10795 | 9e888d60d3e5 |

permissions | -rw-r--r-- |

*** empty log message ***

1 (*<*)theory Base = Main:(*>*)

3 section{*Case study: Verified model checking*}

5 text{*\label{sec:VMC}

6 Model checking is a very popular technique for the verification of finite

7 state systems (implementations) w.r.t.\ temporal logic formulae

8 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic

9 and this section shall explore them a little in HOL. This is done in two steps: first

10 we consider a simple modal logic called propositional dynamic

11 logic (PDL) which we then extend to the temporal logic CTL used in many real

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

13 recursive function @{term mc} that maps a formula into the set of all states 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

16 very efficient one. The main proof obligation is to show that the semantics

17 and the model checker agree.

19 \underscoreon

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 path starting from $s_2$ leading to a state where $p$ or $q$

49 are true'', which is true, and ``on all paths starting from $s_0$ $q$ is always true'',

50 which is false.

52 Abstracting from this concrete example, we assume there is some type of

53 states:

54 *}

56 typedecl state

58 text{*\noindent

59 Command \isacommand{typedecl} merely declares a new type but without

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

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

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

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

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

65 reduces clutter. Similarly we declare an arbitrary but fixed

66 transition system, i.e.\ relation between states:

67 *}

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

71 text{*\noindent

72 Again, we could have made @{term M} a parameter of everything.

73 Finally we introduce a type of atomic propositions

74 *}

76 typedecl atom

78 text{*\noindent

79 and a \emph{labelling function}

80 *}

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

84 text{*\noindent

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

86 *}

88 (*<*)end(*>*)