In diesem Abschnitt finden Sie eine kurze Einführung in die Syntax und Semantik von CTL (Computational Tree Logic) und eine Beschreibung der in INA benutzten Zustandsprädikate.
Während der Berechnung minimaler Pfade (siehe im Kapitel 6.5.3 ab Seite ), der Erreichbarkeitsanalyse (siehe unter ,,bad``-Prädikat im Kapitel 6.5.4 auf Seite ) und dem CTL-Modelchecking (siehe im Kapitel 6.5.4 ab Seite ) arbeitet INA mit Zustandsprädikaten.
Ein Prädikat ist eine Disjunktion von Konjunktionen von nicht notwendigerweise negierten Atomen (disjunktive Normalform). Ein Atom besteht aus einer Erklärung der Form
(mit )
Bei den in INA benutzten Zustandsprädikaten ist z.B. value=Anzahl der Marken auf einem Platz, ein Atom ist von allen Zuständen erfüllt, bei denen der Platz p1 eine oder zwei Marken enthält. Bei Zeitbewertungen können analog Restriktionen der Uhrenstellungen formuliert werden.
Bei Anforderung eines Prädikates am predicate input file Prompt kann mit <esc> auf Terminaleingabe umgeschaltet werden. Geben Sie dann die erste Konjunktion von Atomen ein: Nach Eingabe einer Platznummer werden die unteren und oberen Grenzen abgefragt (lower bound, upper bound). Mit <o> können Sie eine unbeschränkte obere Grenze eingeben. Das Atom können Sie negieren oder nicht (negate the atom?) und danach eine weitere Zustandsnummer angeben, oder mit <Q> die aktuelle Konjunktion beenden. Bei einer Zeitbewertung können weitere Zustandsatome bezüglich Zeitrestriktionen definiert werden.
Durch beantworten der Frage next conjunction mit <Y> gelangen Sie zur Definition der nächsten Konjunktion von (eventuell negierten) Atomen.
Prädikate werden in Dateien mit der Extension .pdc gespeichert.
Im Kapitel 6.5.4 ab Seite finden Sie einen Satz von Funktionen, mit denen bestimmte Prädikate automatisch generiert werden können.
Modelchecking basiert auf der Struktur M=[S,R,P] eines beschrifteten Zustandsübergangsgraphen mit
Diese Abbildung ergibt für einen Zustand die Menge der in diesem Zustand erfüllten Prädikate.
Die Relation bedeutet, daß die CTL-Formel f im Zustand s0 bei gegebener Struktur M erfüllt ist. ist induktiv definiert:
es existiert ein unmittelbarer Nachfolgezustand, in dem f erfüllt ist
auf allen Pfaden ist solange f1 erfüllt, bis ein Zustand erreicht wird, der f2 erfüllt
es existiert ein Pfad, auf dem solange f1 erfüllt ist, bis ein Zustand erreicht wird, der f2 erfüllt
es existiert ein Pfad, auf dem einmal zuvor f1 erfüllt ist, bevor ein Zustand erreicht wird, der f2 erfüllt
Die Eingabe von CTL-Formeln wird im Kapitel 6.5.4 ab Seite beschrieben.
f ist in allen Nachfolgezuständen erfüllt
es existiert ein Pfad, der zu einem Zustand führt, in dem f erfüllt ist
f ist in jedem Zustand auf allen Pfaden erfüllt
es existiert ein Pfad, indem f in jedem Zustand erfüllt ist
Die semiformale Bedeutung der einzelnen Quantoren wird durch die verwendeten Zeichen unterstrichen: E steht für ,,exists``, A für ,,always``, X für ,,next``, U für ,,until``, B für ,,before``, F für ,,forward`` und G für ,,globally``.
© 1996-98 Prof. Peter H. Starke (starke@informatik.hu-berlin.de) und Stephan Roch (roch@...)
INA Handbuch Version 2.1 zuletzt geändert: 1998-03-24