equal
deleted
inserted
replaced
5 text{*\label{sec:VMC} |
5 text{*\label{sec:VMC} |
6 This chapter ends with a case study concerning model checking for |
6 This chapter ends with a case study concerning model checking for |
7 Computation Tree Logic (CTL), a temporal logic. |
7 Computation Tree Logic (CTL), a temporal logic. |
8 Model checking is a popular technique for the verification of finite |
8 Model checking is a popular technique for the verification of finite |
9 state systems (implementations) with respect to temporal logic formulae |
9 state systems (implementations) with respect to temporal logic formulae |
10 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic |
10 (specifications) @{cite "ClarkeGP-book" and "Huth-Ryan-book"}. Its foundations are set theoretic |
11 and this section will explore them in HOL\@. This is done in two steps. First |
11 and this section will explore them in HOL\@. This is done in two steps. First |
12 we consider a simple modal logic called propositional dynamic |
12 we consider a simple modal logic called propositional dynamic |
13 logic (PDL)\@. We then proceed to the temporal logic CTL, which is |
13 logic (PDL)\@. We then proceed to the temporal logic CTL, which is |
14 used in many real |
14 used in many real |
15 model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a |
15 model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a |