equal
deleted
inserted
replaced
1 (*<*)theory Base = Main:(*>*) |
1 (*<*)theory Base = Main:(*>*) |
2 |
2 |
3 section{*Case study: Verified model checking*} |
3 section{*Case study: Verified model checking*} |
4 |
4 |
5 text{* |
5 text{*\label{sec:VMC} |
6 Model checking is a very popular technique for the verification of finite |
6 Model checking is a very popular technique for the verification of finite |
7 state systems (implementations) w.r.t.\ temporal logic formulae |
7 state systems (implementations) w.r.t.\ temporal logic formulae |
8 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic |
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 |
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 |
10 we consider a simple modal logic called propositional dynamic |