equal
deleted
inserted
replaced
7 \begin{isamarkuptext}% |
7 \begin{isamarkuptext}% |
8 Model checking is a very popular technique for the verification of finite |
8 Model checking is a very popular technique for the verification of finite |
9 state systems (implementations) w.r.t.\ temporal logic formulae |
9 state systems (implementations) w.r.t.\ temporal logic formulae |
10 (specifications) \cite{Clark}. Its foundations are completely set theoretic |
10 (specifications) \cite{Clark}. Its foundations are completely set theoretic |
11 and this section shall develop them in HOL. This is done in two steps: first |
11 and this section shall develop them in HOL. This is done in two steps: first |
12 we consider a very simple ``temporal'' logic called propositional dynamic |
12 we consider a simple modal logic called propositional dynamic |
13 logic (PDL) which we then extend to the temporal logic CTL used in many real |
13 logic (PDL) which we then extend to the temporal logic CTL used in many real |
14 model checkers. In each case we give both a traditional semantics (\isa{{\isasymTurnstile}}) and a |
14 model checkers. In each case we give both a traditional semantics (\isa{{\isasymTurnstile}}) and a |
15 recursive function \isa{mc} that maps a formula into the set of all states of |
15 recursive function \isa{mc} that maps a formula into the set of all states of |
16 the system where the formula is valid. If the system has a finite number of |
16 the system where the formula is valid. If the system has a finite number of |
17 states, \isa{mc} is directly executable, i.e.\ a model checker, albeit not a |
17 states, \isa{mc} is directly executable, i.e.\ a model checker, albeit not a |