doc-src/TutorialI/CTL/Base.thy

*** empty log message ***

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

section{*A verified model checker*}

text{*
Model checking is a very popular technique for the verification of finite
state systems (implementations) w.r.t.\ temporal logic formulae
(specifications) \cite{Clark}. Its foundations are completely set theoretic
and this section shall develop them in HOL. This is done in two steps: first
we consider a very simple ``temporal'' logic called propositional dynamic
logic (PDL) which we then extend to the temporal logic CTL used in many real
model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a
recursive function @{term mc} that maps a formula into the set of all states of
the system where the formula is valid. If the system has a finite number of
states, @{term mc} is directly executable, i.e.\ a model checker, albeit not a
very efficient one. The main proof obligation is to show that the semantics
and the model checker agree.

Our models are transition systems.

START with simple example: mutex or something.

Abstracting from this concrete example, we assume there is some type of
atomic propositions
*}

typedecl atom

text{*\noindent
which we merely declare rather than define because it is an implicit parameter of our model.
Of course it would have been more generic to make @{typ atom} a type parameter of everything
but fixing @{typ atom} as above reduces clutter.

Instead of introducing both a separate type of states and a function
telling us which atoms are true in each state we simply identify each
state with that set of atoms:
*}

types state = "atom set";

text{*\noindent
Finally we declare an arbitrary but fixed transition system, i.e.\ relation between states:
*}

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

text{*\noindent
Again, we could have made @{term M} a parameter of everything.
*}
(*<*)end(*>*)