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

lcp's suggestions for CTL

%
\begin{isabellebody}%
\def\isabellecontext{Base}%
%
\isamarkupsection{Case Study: Verified Model Checking%
}
%
\begin{isamarkuptext}%
\label{sec:VMC}
This chapter ends with a case study concerning model checking for 
Computation Tree Logic (CTL), a temporal logic.
Model checking is a popular technique for the verification of finite
state systems (implementations) with respect to temporal logic formulae
(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are set theoretic
and this section will explore them in HOL\@. This is done in two steps.  First
we consider a simple modal logic called propositional dynamic
logic (PDL), which we then extend to the temporal logic CTL, which is
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: it is a model checker, albeit an
inefficient one. The main proof obligation is to show that the semantics
and the model checker agree.

\underscoreon

Our models are \emph{transition systems}, i.e.\ sets of \emph{states} with
transitions between them, as shown in this simple example:
\begin{center}
\unitlength.5mm
\thicklines
\begin{picture}(100,60)
\put(50,50){\circle{20}}
\put(50,50){\makebox(0,0){$p,q$}}
\put(61,55){\makebox(0,0)[l]{$s_0$}}
\put(44,42){\vector(-1,-1){26}}
\put(16,18){\vector(1,1){26}}
\put(57,43){\vector(1,-1){26}}
\put(10,10){\circle{20}}
\put(10,10){\makebox(0,0){$q,r$}}
\put(-1,15){\makebox(0,0)[r]{$s_1$}}
\put(20,10){\vector(1,0){60}}
\put(90,10){\circle{20}}
\put(90,10){\makebox(0,0){$r$}}
\put(98, 5){\line(1,0){10}}
\put(108, 5){\line(0,1){10}}
\put(108,15){\vector(-1,0){10}}
\put(91,21){\makebox(0,0)[bl]{$s_2$}}
\end{picture}
\end{center}
Each state has a unique name or number ($s_0,s_1,s_2$), and in each
state certain \emph{atomic propositions} ($p,q,r$) are true.
The aim of temporal logic is to formalize statements such as ``there is no
path starting from $s_2$ leading to a state where $p$ or $q$
are true'', which is true, and ``on all paths starting from $s_0$ $q$ is always true'',
which is false.

Abstracting from this concrete example, we assume there is some type of
states:%
\end{isamarkuptext}%
\isacommand{typedecl}\ state%
\begin{isamarkuptext}%
\noindent
Command \isacommand{typedecl} merely declares a new type but without
defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
about the type other than its existence. That is exactly what we need
because \isa{state} really is an implicit parameter of our model.  Of
course it would have been more generic to make \isa{state} a type
parameter of everything but declaring \isa{state} globally as above
reduces clutter.  Similarly we declare an arbitrary but fixed
transition system, i.e.\ a 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.
Finally we introduce a type of atomic propositions%
\end{isamarkuptext}%
\isacommand{typedecl}\ atom%
\begin{isamarkuptext}%
\noindent
and a \emph{labelling function}%
\end{isamarkuptext}%
\isacommand{consts}\ L\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ atom\ set{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
telling us which atomic propositions are true in each state.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: