next up previous contents index
Next: 6.5.3 Pfadberechnung Up: 6.5 Erreichbarkeitsanalyse Previous: 6.5.1 Reduktionen des Zustandsgraphen

Unterabschnitte


6.5.2 Prädikate und CTL-Modellchecking

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.

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

$low \leq value \leq upp$ (mit $0\leq low\leq upp\leq \infty$)

Bei den in INA benutzten Zustandsprädikaten ist z.B. value=Anzahl der Marken auf einem Platz, ein Atom $p_1:\;low=1,\;upp=2;$ 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

Mit Modelchecking wird die Prüfung der Gültigkeit von CTL-Formeln im Anfangszustand bezeichnet. Dabei können Zeugen für existenzquantifizierte bzw. Gegenbeispiele für allquantifizierte Teilformeln bestimmt und ausgegeben werden. Zum Ablauf der Berechnung und zur Formeleingabe siehe ab Seite [*] im Kapitel 6.5.4, zur Implemetation siehe [Hel96].

Modelchecking basiert auf der Struktur M=[S,R,P] eines beschrifteten Zustandsübergangsgraphen mit


Syntax von CTL

Die Syntax von CTL-Formeln ist induktiv definiert:


Semantik von CTL

Ein Pfad ist eine unendliche Folge von Zuständen $(s_0,s_1,\ldots)$, so daß für alle i $(s_i,s_{i+1})\in R$ ist.

Die Relation $M,s_0\models f$ bedeutet, daß die CTL-Formel f im Zustand s0 bei gegebener Struktur M erfüllt ist. $\models$ ist induktiv definiert:

Die Eingabe von CTL-Formeln wird im Kapitel 6.5.4 ab Seite [*] beschrieben.


Äquivalenzen und weitere Anmerkungen

Zwischen den temporallogischen Quantoren existieren z.B. folgende Äquivalenzen:

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``.


next up previous contents index
Next: 6.5.3 Pfadberechnung Up: 6.5 Erreichbarkeitsanalyse Previous: 6.5.1 Reduktionen des Zustandsgraphen

© 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