--- a/doc-src/TutorialI/CTL/document/Base.tex Thu Jan 11 11:47:57 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex Thu Jan 11 12:12:01 2001 +0100
@@ -2,22 +2,25 @@
\begin{isabellebody}%
\def\isabellecontext{Base}%
%
-\isamarkupsection{Case study: Verified model checking%
+\isamarkupsection{Case Study: Verified Model Checking%
}
%
\begin{isamarkuptext}%
\label{sec:VMC}
-Model checking is a very popular technique for the verification of finite
+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 completely set theoretic
-and this section will explore them a little in HOL\@. This is done in two steps: first
+(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 used in many real
+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, i.e.\ a model checker, albeit not a
-very efficient one. The main proof obligation is to show that the semantics
+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
@@ -66,7 +69,7 @@
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.\ relation between states:%
+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}%