text‹\label{sec:VMC}
chapter ends with a case study concerning model checking for
Tree Logic (CTL), a temporal logic.
checking is a popular technique for the verification of finite
systems (implementations) with respect to temporal logic formulae
specifications) cite‹"ClarkeGP-book" and "Huth-Ryan-book"›. Its foundations are set theoretic
this section will explore them in HOL\@. This is done in two steps. First
consider a simple modal logic called propositional dynamic
(PDL)\@. We then proceed to the temporal logic CTL, which is
in many real
checkers. In each case we give both a traditional semantics (‹⊨›) and a
function term‹mc› that maps a formula into the set of all states of
system where the formula is valid. If the system has a finite number of
, term‹mc› is directly executable: it is a model checker, albeit an
one. The main proof obligation is to show that the semantics
the model checker agree.
underscoreon
models are \emph{transition systems}:\index{transition systems}
of \emph{states} with
between them. Here is a 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}
state has a unique name or number ($s_0,s_1,s_2$), and in each state \emph{atomic propositions} ($p,q,r$) hold. The aim of temporal logic
to formalize statements such as ``there is no path starting from $s_2$
to a state where $p$ or $q$ holds,'' which is true, and ``on all paths
from $s_0$, $q$ always holds,'' which is false.
from this concrete example, we assume there is a type of
: ›
typedecl state
text‹\noindent \commdx{typedecl} merely declares a new type but without
it (see \S\ref{sec:typedecl}). Thus we know nothing
the type other than its existence. That is exactly what we need typ‹state› really is an implicit parameter of our model. Of
it would have been more generic to make typ‹state› a type
of everything but declaring typ‹state› globally as above
clutter. Similarly we declare an arbitrary but fixed
system, i.e.\ a relation between states: ›
consts M :: "(state × state)set"
text‹\noindent
is Isabelle's way of declaring a constant without defining it.
we introduce a type of atomic propositions ›
typedecl"atom"
text‹\noindent
a \emph{labelling function} ›
consts L :: "state → atom set"
text‹\noindent
us which atomic propositions are true in each state. ›
(*<*)end(*>*)
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet am 2026-06-30)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
