doc-src/TutorialI/CTL/document/Base.tex

*** empty log message ***

%
\begin{isabellebody}%
\def\isabellecontext{Base}%
%
\isamarkupsection{A verified model checker}
%
\begin{isamarkuptext}%
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 (\isa{{\isasymTurnstile}}) and a
recursive function \isa{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, \isa{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%
\end{isamarkuptext}%
\isacommand{typedecl}\ atom%
\begin{isamarkuptext}%
\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 \isa{atom} a type parameter of everything
but fixing \isa{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:%
\end{isamarkuptext}%
\isacommand{types}\ state\ {\isacharequal}\ {\isachardoublequote}atom\ set{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
Finally we declare an arbitrary but fixed transition system, i.e.\ relation between states:%
\end{isamarkuptext}%
\isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
Again, we could have made \isa{M} a parameter of everything.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: