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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Mon Oct 02 14:32:33 2000 +0200
@@ -0,0 +1,53 @@
+%
+\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: