Quelle Base.thy

Sprache: Isabelle

(*<*)theory Base imports Main begin(*>*)

section‹Case Study: Verified Model Checking›

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
🍋‹state› really is an implicit parameter of our model. Of
it would have been more generic to make 🍋‹state› a type
of everything but declaring 🍋‹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-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.