28 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic |
28 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic |
29 and this section will explore them in HOL\@. This is done in two steps. First |
29 and this section will explore them in HOL\@. This is done in two steps. First |
30 we consider a simple modal logic called propositional dynamic |
30 we consider a simple modal logic called propositional dynamic |
31 logic (PDL)\@. We then proceed to the temporal logic CTL, which is |
31 logic (PDL)\@. We then proceed to the temporal logic CTL, which is |
32 used in many real |
32 used in many real |
33 model checkers. In each case we give both a traditional semantics (\isa{{\isasymTurnstile}}) and a |
33 model checkers. In each case we give both a traditional semantics (\isa{{\isaliteral{5C3C5475726E7374696C653E}{\isasymTurnstile}}}) and a |
34 recursive function \isa{mc} that maps a formula into the set of all states of |
34 recursive function \isa{mc} that maps a formula into the set of all states of |
35 the system where the formula is valid. If the system has a finite number of |
35 the system where the formula is valid. If the system has a finite number of |
36 states, \isa{mc} is directly executable: it is a model checker, albeit an |
36 states, \isa{mc} is directly executable: it is a model checker, albeit an |
37 inefficient one. The main proof obligation is to show that the semantics |
37 inefficient one. The main proof obligation is to show that the semantics |
38 and the model checker agree. |
38 and the model checker agree. |
87 reduces clutter. Similarly we declare an arbitrary but fixed |
87 reduces clutter. Similarly we declare an arbitrary but fixed |
88 transition system, i.e.\ a relation between states:% |
88 transition system, i.e.\ a relation between states:% |
89 \end{isamarkuptext}% |
89 \end{isamarkuptext}% |
90 \isamarkuptrue% |
90 \isamarkuptrue% |
91 \isacommand{consts}\isamarkupfalse% |
91 \isacommand{consts}\isamarkupfalse% |
92 \ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequoteclose}% |
92 \ 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}}% |
93 \begin{isamarkuptext}% |
93 \begin{isamarkuptext}% |
94 \noindent |
94 \noindent |
95 This is Isabelle's way of declaring a constant without defining it. |
95 This is Isabelle's way of declaring a constant without defining it. |
96 Finally we introduce a type of atomic propositions% |
96 Finally we introduce a type of atomic propositions% |
97 \end{isamarkuptext}% |
97 \end{isamarkuptext}% |
98 \isamarkuptrue% |
98 \isamarkuptrue% |
99 \isacommand{typedecl}\isamarkupfalse% |
99 \isacommand{typedecl}\isamarkupfalse% |
100 \ {\isachardoublequoteopen}atom{\isachardoublequoteclose}% |
100 \ {\isaliteral{22}{\isachardoublequoteopen}}atom{\isaliteral{22}{\isachardoublequoteclose}}% |
101 \begin{isamarkuptext}% |
101 \begin{isamarkuptext}% |
102 \noindent |
102 \noindent |
103 and a \emph{labelling function}% |
103 and a \emph{labelling function}% |
104 \end{isamarkuptext}% |
104 \end{isamarkuptext}% |
105 \isamarkuptrue% |
105 \isamarkuptrue% |
106 \isacommand{consts}\isamarkupfalse% |
106 \isacommand{consts}\isamarkupfalse% |
107 \ L\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ {\isasymRightarrow}\ atom\ set{\isachardoublequoteclose}% |
107 \ L\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ atom\ set{\isaliteral{22}{\isachardoublequoteclose}}% |
108 \begin{isamarkuptext}% |
108 \begin{isamarkuptext}% |
109 \noindent |
109 \noindent |
110 telling us which atomic propositions are true in each state.% |
110 telling us which atomic propositions are true in each state.% |
111 \end{isamarkuptext}% |
111 \end{isamarkuptext}% |
112 \isamarkuptrue% |
112 \isamarkuptrue% |