Temporale Logiken: CTL und LTL - wi1.uni- · PDF fileTemporale Logiken: CTL und LTL im Rahmen...

Westfälische Wilhelms-Universität Münster

Ausarbeitung

Temporale Logiken: CTL und LTL

im Rahmen des Seminars Formale Spezifikation im WS 2005/06

Thorsten Bruns

Themensteller: Prof. Dr. Herbert Kuchen Betreuer: (Prof. Dr. Herbert Kuchen) Institut für Wirtschaftsinformatik Praktische Informatik in der Wirtschaft

II

Inhaltsverzeichnis

1 Einleitung................................................................................................................... 1

2 Grundlagen der Logik................................................................................................ 2

2.1 Aussagenlogik................................................................................................... 2

2.2 Prädikatenlogik ................................................................................................. 3

2.3 Entscheidbarkeit von Logiken .......................................................................... 6

3 Temporale Logiken.................................................................................................... 7

3.1 Erweiterung der Aussagen- oder Prädikatenlogik ............................................ 7

3.2 Klassifikation temporaler Logiken ................................................................... 7

3.3 Semantik verschiedener Zeitmodelle................................................................ 8

3.4 LTL ................................................................................................................... 9

3.4.1 Syntax von LTL............................................................................................ 9 3.4.2 Semantik von LTL ...................................................................................... 10 3.4.3 Varianten von LTL ..................................................................................... 12

3.5 CTL................................................................................................................. 12

3.5.1 Syntax von CTL.......................................................................................... 12 3.5.2 Semantik von CTL...................................................................................... 13 3.5.3 Semantische Äquivalenzen ......................................................................... 15 3.5.4 CTL Model Checking ................................................................................. 15 3.5.5 Anwendung des Markierungsalgorithmus .................................................. 17

3.6 Fixpunktcharakterisierung .............................................................................. 18

3.7 Theoretische Aspekte temporaler Logiken ..................................................... 19

4 Zusammenfassung ................................................................................................... 20

Literaturverzeichnis ........................................................................................................ 21

Kapitel 1: Einleitung

1

1 Einleitung

Einen Problembereich der Informatik stellt die Qualitätssicherung von Hard- und

Software dar. Dieses Problem kann einerseits durch Testen und andererseits durch

Beweise gelöst werden. Das Testen lässt sich größtenteils automatisieren, es kann aber

nicht sichergestellt werden, dass alle möglichen Fälle berücksichtigt werden. Die

Alternative zum Testen sind Beweise. Hierbei wird zwischen Theorembeweisen und

Model Checkern unterschieden. Theorembeweise müssen interaktiv durchgeführt

werden und erfordern viel Zeit, daher sind sie weniger beliebt. Model Checker bieten

die Möglichkeit, Eigenschaften von Programmen vollständig automatisiert zu prüfen.

Dazu muss das zu prüfende Soft- oder Hardwaresystem als formales Modell mit endlich

vielen Zuständen darstellbar sein. Als weiteres wird eine formale Spezifikation benötigt,

die festlegt, welche Eigenschaften das Programm erfüllen soll. Die Aufgabe eines

Model Checkers besteht darin, zu prüfen, ob die Implementierung der Spezifikation

genügt.

Bei den zu prüfenden Systemen handelt es sich um sogenannte reaktive Systeme, die in

ständiger Interaktion mit Ihrer Umgebung stehen, auf die Signale aus ihrer Umgebung

reagieren und im Normalfall nie terminieren, wie z. B. Betriebssysteme, Netzwerk-

protokolle oder Prozesssteuerungen. Diese Systeme lassen sich in endlichen Modellen

darstellen. Die Eigenschaften, die sich prüfen lassen, sind z. B. Lebendigkeit, Deadlock-

freiheit, Fairness und Sicherheit.

Das Ziel dieser Arbeit ist es, die Möglichkeiten der Darstellung einer formalen

Spezifikation durch temporale Logiken darzustellen und aufzuzeigen, wie diese

Logiken für das Model Checking eingesetzt werden können.

Die Arbeit gliedert sich in ein Grundlagen- und ein Hauptkapitel. Im ersten wird ein

kurzer Überblick über die Aussagen- und die Prädikatenlogik gegeben, da diese als

Voraussetzung für temporale Logiken benötigt werden. Im nächsten Kapitel werden die

beiden temporalen Logiken LTL und CTL genauer untersucht.

Kapitel 2: Grundlagen der Logik

2 Grundlagen der Logik

2.1 Aussagenlogik

Die Aussagenlogik beschäftigt sich mit der Untersuchung des Wahrheitswertes von

Aussagen. Diese können entweder wahr oder falsch sein und sind somit zweiwertig. Die

formale Darstellung von Aussagen geschieht in einer formalen Logik, der Aussagen-

logik. Die Wahrheitswerte von Aussagen sind hier statisch, d. h. sie gelten dauerhaft

und können sich nicht dynamisch ändern.

Die Syntax der Aussagenlogik ist nach [Sc00] folgendermaßen definiert:

Formeln bestehen aus atomaren Formeln der Form mit iA K,3,2,1=i . Formeln werden

durch folgenden induktiven Prozess definiert:

1. Alle atomaren Formeln sind Formeln. iA

2. Für alle Formeln und sind F G ( )GF ∧ und ( )GF ∨ Formeln.

3. Für jede Formel ist F F¬ eine Formel.

Eine Formel der Form wird als Konjunktion bezeichnet, eine Formel der Form

als Disjunktion und als Negation.

( GF ∧ ))( GF ∨ F¬

Nachfolgend werden einige Umformungsregeln aufgestellt. Dabei werden zwei neue

Symbole, und ↔ , sowie die boolschen Konstanten true und eingeführt.

Hierbei bezeichnen und

→ false

A B beliebige aussagenlogische Formeln:

( BA ∨ ) = ( )BA ¬∧¬¬

( BA → )) = ( )BA ∨¬

( BA ↔ = ( ) ( )( )BABA ¬∧¬∨∧

true = AA ¬∨

false = true¬

Die Semantik der Aussagenlogik ist nach [Sc00] wie folgt definiert:

Jede atomare Formel besitzt eine Belegung mit einem Wahrheitswert aus { . Eine

Belegung ist eine Funktion

}1,0

{ }1,0: →DA mit der Menge , die eine Teilmenge der

atomaren Formeln ist. wird zu

D

A { }1,0: →EÂ erweitert, wobei E die Menge aller

2


Formeln ist, die sich aus der Menge der atomaren Formeln zusammensetzt. So lässt

sich jeder beliebigen Formel, die nur aus atomaren Formeln zusammengesetzt ist, ein

Wahrheitswert zuordnen.

D

1. Für jede atomare Formel DAi ∈ gilt ( ) ( )ii AAAÂ = mit K,3,2,1=i .

2. , falls ( )( ) 1=∧ GFÂ ( ) 1=FÂ und ( ) 1=GÂ , sonst 0.

3. , falls ( )( ) 1=∨ GFÂ ( ) 1=FÂ oder ( ) 1=GÂ , sonst 0.

4. , falls , sonst 0. ( ) 1=¬FÂ ( ) 0=FÂ

Zur Berechnung des Wahrheitswertes aussagenlogischer Formeln können diese in

Verknüpfungstabellen dargestellt werden. Anhand dieser Tabellen ist ersichtlich, dass

die Anzahl aller möglicher Wertebelegungen für einen Ausdruck exponentiell in Bezug

auf die Anzahl der in einem Ausdruck enthaltenen atomaren Formeln wächst.

Im folgenden werden weitere Begriffe nach [Sc00] definiert:

Sei eine Formel und eine Belegung. Dann heißt zu passend, wenn für

alle in vorkommenden atomaren Formeln definiert ist. Falls zu passend ist und

gilt, so wird ⊨ geschrieben. gilt unter der Belegung von bzw.

ist ein Modell für . Umgekehrt ist kein Modell für , falls , geschrieben

⊭ . Jede Belegung von Wahrheitswerten, die der Formel den Wert 1 zuordnet,

wird somit als Modell bezeichnet.

F A A F A

F A F

( ) 1=FA A F F A A

F A F ( ) 0=FA

A F F

Eine Formel heißt erfüllbar, falls mindestens ein Modell besitzt, sonst heißt

unerfüllbar. Um zu prüfen, ob eine Formel erfüllbar ist, müssen alle möglichen

Belegungen geprüft werden, ob mindestens eine Belegung für die Formel den Wert 1

ergibt.

F F

Eine Formel heißt gültig oder Tautologie, falls jede zu passende Belegung ein

Modell für ist. In diesem Fall wird nur ⊨ geschrieben.

F

F F

2.2 Prädikatenlogik

Die Prädikatenlogik ist eine Erweiterung der Aussagenlogik um Quantoren, Funktions-

sowie Prädikatsymbole. Hiermit lassen sich Aussagen über Objekte machen, die durch

Variablen repräsentiert werden, z. B., dass Objekte gewisse Eigenschaften haben oder

mit anderen Objekten in Beziehung stehen. 3


Die Syntax prädikatenlogischer Formeln ist nach [Sc00] folgendermaßen definiert:

Zur Definition prädikatenlogischer Formeln werden Variablen, Prädikat- und Funk-

tionssymbole eingeführt. Eine Variable hat die Form mit ix K,3,2,1=i . Ein Prädikat-

symbol hat die Form mit kiP K,3,2,1=i und K,3,2,1,0=k . Ein Funktionssymbol hat

die Form mit und kif K,3,2,1=i K,3,2,1,0=k . Hierbei stellt i den Index und die

Stelligkeit der Prädikate und Funktionen dar.

k

Mit Variablen und Funktionen werden Terme gebildet. Diese sind wie folgt definiert:

1. Jede Variable mit ix K,3,2,1=i ist ein Term.

2. Ist f ein Funktionssymbol mit der Stelligkeit und sind Terme, so ist

auch ein Term.

k ktt ,...,1

( kttf ,...,1 )

Funktionen der Stelligkeit null werden als Konstanten bezeichnet und ohne Klammern

dargestellt.

Prädikatenlogische Formeln sind definiert:

1. Ist P ein Prädikatsymbol der Stelligkeit und sind Terme, so ist

eine Formel.

k ktt ,...,1

( )kttP ,...,1

2. Für jede Formel ist auch F F¬ eine Formel.

3. Für alle Formeln und sind auch F G ( )GF ∧ und ( )GF ∨ Formeln.

4. Ist x eine Variable und eine Formel, so sind auch F xF∃ und Formeln. xF∀

Variablen werden in freie und gebundene unterteilt. Kommt eine Variable x in einer

Teilformel der Formeln oder G xG∃ xG∀ vor, so wird diese Variable als gebunden

bezeichnet, anderenfalls als frei. Eine Formel wird nur dann als Aussage bezeichnet,

wenn diese ausschließlich gebundene Variablen enthält. Das Symbol ∃ wird als

Existenzquantor und das Symbol ∀ als Allquantor bezeichnet.

Die Semantik prädikatenlogischer Ausdrücke ist nach [Sc00] folgendermaßen definiert:

Zur Definition der Semantik der Prädikatenlogik wird zunächst eine Struktur

benötigt. bezeichnet eine beliebige nichtleere Menge, die auch als

Grundmenge von bezeichnet wird. Weiter ist eine Abbildung, die

( AA IUA ,= ) AU

A AI

• jedem k-stelligen Prädikatsymbol P ein k-stelliges Prädikat über zuordnet, AU

• jedem k-stelligen Funktionssymbol eine k-stellige Funktion auf zuordnet f AU 4


• und jeder Variablen x ein Element der Grundmenge zuordnet. AU

Sie eine Formel und eine Struktur. heißt zu passend, falls für

alle in vorkommenden Prädikat- und Funktionssymbole sowie freien Variablen

definiert ist.

F ( AA IUA ,= ) A F AI

F

Sei eine Formel und eine zu passende Struktur. Für jeden Term t , der sich aus

den Bestandteilen von bilden lässt, wird der Wert von t in der Struktur ,

bezeichnet mit

F A F

F A

( )tA , wie folgt definiert:

1. Falls t eine Variable xt = ist, so gilt ( ) AxtA = .

2. Falls t ein k-stelliges Funktionssymbol ( )kttft ,...,1= ist, so gilt

.

Bei nullstelligen Funktionssymbolen

( ) ( ) ( )( )kA tAtAftA ,...,1=

at = gilt ( ) AatA = .

Der Wahrheitswert einer Formel wird folgendermaßen definiert: F

1. Hat F die Form ( )kttPF ,...1= mit den Termen und dem k-stelligen

Prädikatsymbol

ktt ,...,1

P , so ist ( ) 1=FA , falls ( ) ( )( ) Ak PtAtA ∈,...,1 , sonst 0.

2. Hat F die Form , so ist GF ¬= ( ) 1=FA , falls ( ) 0=GA , sonst 0.

3. Hat F die Form ( )HGF ∧= , so ist ( ) 1=FA , falls ( ) 1=GA und ( ) 1=HA ,

sonst 0.

4. Hat F die Form ( )HGF ∨= , so ist ( ) 1=FA , falls ( ) 1=GA oder ( ) 1=HA ,

sonst 0.

5. Hat F die Form xGF ∀= , so ist ( ) 1=FA , falls für alle gilt: AUd ∈

( ) 1]/[ =GdA x , sonst 0.

6. Hat F die Form xGF ∃= , so ist ( ) 1=FA , falls es ein gibt mit: AUd ∈

( ) 1]/[ =GdA x , sonst 0.

Die Modell-, Erfüllbarkeits- und Gültigkeitsdefinitionen gelten hier analog zur

Aussagenlogik.

Die Prädikatenlogik ist ausdrucksstärker als die Aussagenlogik, allerdings kann auch

hiermit nicht jede mathematische Aussage formuliert werden. Die Quantoren lassen sich

in der dargestellten Form nur auf Variablen anwenden, nicht aber auf Funktions-

5


symbole. Daher wird diese Logik Prädikatenlogik erster Stufe genannt. Die zweite Stufe

umfasst zusätzlich die Anwendung der Quantoren auf Funktionssymbole.

2.3 Entscheidbarkeit von Logiken

Für Anwendungszwecke ist es wichtig zu wissen, ob eine Logik entscheidbar ist oder

nicht. Der Ausdruck entscheidbar bedeutet, ob sich ein Algorithmus finden lässt, der in

endlicher Zeit ausgibt, ob es zu einer beliebigen Formel einer gegebenen Logik ein

Modell, d. h. mindestens eine gültige Belegung, gibt oder nicht. Wichtig ist hierbei, dass

so ein Algorithmus nicht nur positive, sondern auch negative Ergebnisse ausgibt und

dabei in jedem Fall stoppt. Für aussagenlogische Ausdrücke ist diese Überlegung

einfach. Das Aufschreiben aller möglichen Belegungen ist bereits ein entsprechender

Algorithmus. Es gibt in einer aussagenlogischen Formel mit atomaren Formeln

immer genau mögliche Belegungen, die überprüft werden müssen, da jede atomare

Formel genau zwei Wahrheitswerte, 0 oder 1, belegen kann. Daraus folgt, dass die

Aussagenlogik entscheidbar ist.

nn2

In der Prädikatenlogik ist bereits das Gültigkeitsproblem unentscheidbar, d. h. es lässt

sich kein Algorithmus finden, der in endlicher Zeit feststellen kann, ob eine Belegung

eines beliebigen prädikatenlogischen Ausdrucks wahr oder falsch ist. Daraus lässt sich

folgern, dass das Erfüllbarkeitsproblem der Prädikatenlogik ebenfalls unentscheidbar

ist, da dieses Problem die Entscheidbarkeit des Gültigkeitsproblems voraussetzt.

Das Aufschreiben aller möglichen Belegungen lässt sich nicht auf die Prädikatenlogik

übertragen, da hier Strukturen anstatt Belegungen existieren. Diese Strukturen können

unendliche Mengen enthalten, die ein vollständiges Aufschreiben verhindern.

Dies alleine ist jedoch noch kein Beweis für die Unentscheidbarkeit des

Gültigkeitsproblems der Prädikatenlogik. Der Beweis erfolgt, indem dieses Problem auf

ein bereits als unentscheidbar bekanntes Problem, das Postsche Korrespondenzproblem,

zurückgeführt wird. Dazu muss ein Algorithmus gefunden werden, der in endlicher Zeit

jedes beliebige Postsche Korrespondenzproblem K in eine prädikatenlogische Formel

überführt, so dass KF K genau dann eine Lösung besitzt, wenn gültig ist. Da dieser

Beweis einen tieferen Einstieg in die Berechenbarkeitstheorie erfordert, wird dieser hier

ausgelassen. Der Beweis kann in [Sc00, S.71-73] nachgelesen werden.

KF

6

Kapitel 3: Temporale Logiken

7

3 Temporale Logiken

3.1 Erweiterung der Aussagen- oder Prädikatenlogik

Temporale Logiken sind Erweiterungen der Aussagen- oder der Prädikatenlogik. Diese

Logiken ermöglichen Aussagen über zeitliche Veränderungen. In der Aussagenlogik

sind Aussagen entweder immer oder nie wahr. Bei temporalen Logiken ist der Wahr-

heitswert einer Aussage zusätzlich vom aktuellen Zeitpunkt abhängig, da es möglich ist,

sowohl Aussagen über die Zukunft als auch über die Vergangenheit zu formulieren. Mit

der Erweiterung der Aussagenlogik um einen Zeitoperator für die Zukunft und einen für

die Vergangenheit lassen sich bereits beliebig komplexe Zeitstrukturen darstellen, die

sprachlich nicht mehr ausgedrückt werden können. Der Ursprung der temporalen Logik

entstammt der Philosophie, daher existiert ein enger Bezug zur Repräsentation der

Zeitformen einer natürlichen Sprache durch eine formale Logik [Bu84].

3.2 Klassifikation temporaler Logiken

Temporale Logiken lassen sich nach [Em90] auf verschiedene Arten klassifizieren.

Temporale Logiken können:

• Auf der Aussagen- oder der Prädikatenlogik basieren. Dazu erweitert eine

temporale Logik entweder die Aussagen- oder die Prädikatenlogik um neue

Operatoren.

• Ein lineares oder ein verzweigtes Zeitmodell besitzen. Die Zeit kann entweder

eindeutig oder nicht eindeutig modelliert werden. Ist die Zeit eindeutig, so

existiert zu jedem Zeitpunkt nur ein möglicher unmittelbarer Nachfolger in der

Zukunft. Bei Verwendung eines verzweigten Zeitmodells können zu jedem

Zeitpunkt mehrere unmittelbare Nachfolger existieren. Dabei ist festzuhalten,

dass dieser Nichtdeterminismus nur für die Zukunft, nicht aber für die

Vergangenheit gilt. Die Vergangenheit ist in jedem Zeitpunkt eindeutig.

• Die Zeit diskret oder kontinuierlich modellieren. Die Zeit kann als Folge von

Zeitpunkten angesehen werden, so dass bei Verwendung eines linearen

Zeitmodells jeder Zeitpunkt genau einen Nachfolger hat und bei einem

verzweigten Zeitmodell jeder Zeitpunkt abzählbar viele Nachfolger besitzt. Hier


8

kann von jedem Zeitpunkt zum nächsten gesprungen werden. Alternativ kann

die Zeit auch kontinuierlich sein, so dass es zu keinem Zeitpunkt einen

unmittelbar nachfolgenden Zeitpunkt gibt. Hier ist nur ein Vergleich auf früher

oder später zwischen zwei Zeitpunkten möglich. Da in Programmen nur diskrete

Berechnungen möglich sind, wird die Zeit in der Regel als diskret angesehen.

• Zeitpunkte oder Zeiträume betrachten. Die Zeit kann als Folge aufeinander-

folgender Zeitpunkte oder auch als Folge von Intervallen betrachtet werden.

• Die Vergangenheit oder die Zukunft berücksichtigen. Es gibt sowohl Operatoren

für die Zukunft als auch für die Vergangenheit. Temporale Logiken, die zur

Programmverifikation eingesetzt werden, besitzen nur Operatoren für die

Zukunft, da jedes Programm einen definierten Startzeitpunkt besitzt und die

Betrachtung der Vergangenheit somit irrelevant ist. Der zusätzliche Operator für

die Vergangenheit bringt außerdem keine Erweiterung der Ausdrucksstärke.

Bis auf den letzten Punkt schließen sich alle Alternativen gegenseitig aus. Eine

temporale Logik kann beim letzten Punkt beide Fälle berücksichtigen.

Die hier dargestellten Kombinationen erlauben, eine Vielzahl möglicher temporaler

Logiken zu definieren. Im folgenden werden zwei Alternativen genauer untersucht, die

sich hauptsächlich im verwendeten Zeitmodell unterscheiden.

3.3 Semantik verschiedener Zeitmodelle

Zur späteren Definition der Semantik einer temporalen Logik wird die Bedeutung der

verschiedenen Zeitmodelle benötigt. Dazu müssen die verschiedenen Zeitmodelle

definiert werden. Im Falle der Modellierung diskreter Systeme, wie eines Soft- oder

Hardwaresystems, muss auch die Zeit diskret modelliert werden. Daher existiert in

diesen Fällen eine Menge von Zuständen, die den zeitlichen Ablauf repräsentieren.

Zudem wird auf dieser Menge von Zuständen wird eine zeitliche Ordnung benötigt, die

festlegt, wie sich die Zustände ordnen lassen. Dazu wird ein Tupel gebildet, das in

diesem Zusammenhang Rahmen genannt wird. Dieser Rahmen enthält die Menge der

Zustände und die zugehörige Ordnungsrelation.

Wird eine lineare Zeitstruktur verwendet, so lässt sich jedem Zustand eindeutig eine

Zahl aus der Menge der natürlichen Zahlen zuordnen. Die auf den natürlichen Zahlen

basierende Ordnungsrelation ist total. Dies bedeutet auf die Menge der Zustände


übertragen, dass für zwei beliebige Zustände und t gilt: Entweder kommt zeitlich

vor t , und t sind gleich oder kommt nach t .

s s

s s

Bei Verwendung einer verzweigten Zeitstruktur ist die Zukunft nicht eindeutig definiert.

Die hier verwendete Ordnungsrelation muss einer Baumordnung entsprechen. Für jeden

Zustand, der mehrere unmittelbare Nachfolger enthält, steht nicht eindeutig fest,

welcher Zustand danach als erstes eintritt. Da die Verzweigung nur in die Zukunft

gerichtet ist, besitzen die Zustände der Vergangenheit eine lineare Ordnungsrelation.

3.4 LTL

LTL steht für linear temporal logic. Diese Logik zeichnet sich durch die Verwendung

einer linearen Zeitstruktur aus. In [Em90] werden folgende drei grundlegende An-

nahmen für LTL getroffen:

1. Die Zeit ist diskret.

2. Es gibt einen Startzustand, der keine Vorgänger besitzt.

3. Die Zukunft ist unendlich.

Die Annahme einer diskreten Zeit ist darauf zurückzuführen, dass heutige Computer

digitale Geräte sind, die nur diskrete Berechnungen ermöglichen. Somit läuft auch die

Zeit diskret ab, indem jeder Zeitpunkt als ein Zustand betrachtet wird. Jedes Programm

beginnt in einem Startzustand ohne vorherige Informationen, dies rechtfertigt die zweite

Annahme. Die letzte Annahme ist damit zu begründen, dass die zu untersuchenden

Programme im Idealfall nie stoppen und unendlich lange laufen sollen.

Zu LTL gibt es Varianten, die entweder auf der Aussagenlogik oder der Prädikatenlogik

basieren. Im folgenden wird nur die Erweiterung der Aussagenlogik untersucht. Diese

Logik wird in [Em90] als PLTL bezeichnet.

3.4.1 Syntax von LTL

Die Syntax von LTL erweitert die Syntax der Aussagenlogik um vier weitere

Operatoren. Sie wird mittels Backus Naur Form (BNF) nach [HR01] folgendermaßen

definiert:

( ) ( ) ( ) ( ) ( ) ( )pUpGpFpXppppppppppPp |||||||||:: ↔→∨∧¬=

P bezeichnet hier eine beliebig atomare aussagenlogische Formel.

9


Die höchste Bindung besitzen die unären Operatoren ¬ , X , und . Danach folgen

zuerst das und anschließend das . Als letztes kommen → ,

F G

∧ ∨ ↔ sowie U .

Zusätzlich zu den Umformungsmöglichkeiten der Aussagenlogik können in LTL

folgende Umformungen durchgeführt werden:

Fp = ( )pUtrue

Gp = pF¬¬

3.4.2 Semantik von LTL

Zur Definition der Semantik von LTL wird neben der Definition des Rahmens der

linearen Zeitstruktur eine Auswertungsfunktion benötigt, die jeder Formel in jedem

Zustand einen Wahrheitswert zuordnet bzw. jedem Zustand die Menge der gültigen

atomaren Aussagen zuweist. Damit wird der Rahmen um eine Funktion erweitet. Die

Zeitstruktur in der Verwendung einer temporalen Logik wird als Struktur

definiert. Diese Strukturen werden auch als Kripkestrukturen bezeichnet. bezeichnet

die Menge der Zustände,

( )LRSM ,,=

S

R die Übergangsrelation SSR ×⊆ über den Zuständen und

die Funktion, die jedem Zustand eine Teilmenge der Menge ( )PePotenzmengSL →:

P aller atomaren Aussagen zuweist, die in diesem Zustand gültig sind.

Da in LTL nur lineare Zeitstrukturen betrachtet werden, sind Aussagen nicht auf

einzelnen Zuständen, sondern auf einem Pfad oder auf Teilpfaden definiert. Im

folgenden bedeutet π,M ⊨ p , dass die Formel p im Pfad ( ,...., 10 ss= )π für die

Struktur M gültig ist, iM π, ⊨ p bedeutet, dass die Formel p in einem Teilpfad von

( ,...., 10 ss= )π beginnend mit dem Zustand gültig ist. Ist die Struktur klar, so kann

das Symbol

is

M weggelassen werden und es wird nur π ⊨ p geschrieben. Die Semantik

von LTL ist nach [HR01] folgendermaßen definiert:

1. π ⊨P gdw. für eine atomare aussagenlogische Formel ( )0sLP ∈ P .

2. π ⊨ p¬ gdw. π ⊭ p .

3. π ⊨ gdw. ( qp ∧ ) π ⊨ p und π ⊨ . q

4. π ⊨ gdw. Xp 1π ⊨ p .

5. π ⊨ gdw. für das gilt: Fp 0≥∃j jπ ⊨ p .

10


6. π ⊨ gdw. gilt: Gp 0≥∀j jπ ⊨ p .

7. π ⊨ gdw. für das gilt:( qUp ) 0≥∃j jπ ⊨ und q jk <≤∀0 gilt: kπ ⊨ p .

Der Wahrheitswert einer Formel ist immer auf den gegenwärtigen Zeitpunkt bzw.

Zustand bezogen. In den nachfolgenden Abbildungen stellt der erste dargestellte

Zustand den jeweils aktuellen Zustand dar. Die vollständig ausgefüllten Zustände sind

diejenigen, in denen die Aussage p wahr ist.

Die Formel ist im aktuellen Zustand wahr, wenn Xp p im nächsten Zustand wahr ist.

Die Formel ist im aktuellen Zustand wahr, wenn Fp p in einem beliebigen Zustand in

der Zukunft wahr ist.

Die Formel ist im aktuellen Zustand wahr, wenn Gp p in jedem Zustand in der

Zukunft wahr ist.

Die Formel ( ist im aktuellen Zustand wahr, wenn )qUp p vom aktuellen Zustand an

solange wahr ist, bis wahr wird. In dem schraffierten Zustand ist q wahr, über q p

wird hierbei keine Aussage mehr getroffen.

Eine Formel verhält sich nach [Mc93] wie ein offener Satz mit einem freien Parameter,

der den aktuellen Zustand repräsentiert. Da eine Formel aber nicht nur in einem

bestimmten Zustand gültig sein muss, steht dieser Parameter für die Menge aller

gültigen Zustände. Anders herum wird durch die Festlegung eines Zustandes eine

Menge von Formeln definiert, die in diesem Zustand gültig sind.

11

Eine Formel p in LTL ist genau dann erfüllbar, wenn es eine Zeitstruktur

gibt, auf der ein Pfad ( LRSM ,,= ) π definiert ist, so dass π,M ⊨ p gilt. Jede

Zeitstruktur, die dies erfüllt, wird somit als Modell für p bezeichnet. Die Formel p

heißt gültig genau dann, wenn diese Formel für alle Zeitstrukturen gilt. In

diesem Fall wird nur ⊨

( LRSM ,,= )

p geschrieben. Die Formel p ist gültig genau dann, wenn p¬

nicht erfüllbar ist.


3.4.3 Varianten von LTL

Es gibt viele Varianten von LTL. Diese betreffen z. B. die Semantik der Operatoren

oder die verwendeten Operatoren überhaupt. Zu den hier verwendeten lassen sich noch

Operatoren hinzufügen, die Aussagen über die Vergangenheit ermöglichen. Die

Semantik der Operatoren lässt sich z. B. auf die Frage hin ändern, ob die Zukunft die

Gegenwart mit einschließt oder nicht. Weitere Beispiele von Varianten, welche die

Semantik von Operatoren betreffen, können in [Em90] nachgelesen werden.

Die zuvor angegebene Logik basiert auf der Aussagenlogik. Eine grundlegende

Änderung dieser Logik besteht darin, diese auf der Prädikatenlogik aufzubauen. Bei

einer solchen Erweiterung muss die Unentscheidbarkeit der Prädikatenlogik beachtet

werden. Da Formeln temporaler Logiken automatisiert auf Gültigkeit überprüft werden

sollen, kann diese Erweiterung nur so restriktiv erfolgen, dass die daraus entstehende

Logik entscheidbar ist. Diese Erweiterung wird in dieser Arbeit nicht weiter untersucht.

3.5 CTL

CTL steht für Computation tree logic. Diese temporale Logik wurde von Clarke und

Emerson [CE81] definiert. CTL basiert auf der Aussagenlogik und benutzt eine

verzweigte Zeitstruktur. Jeder Zeitpunkt kann bei dieser Zeitstruktur mehrere

nachfolgende Zeitpunkte besitzen, d. h. die Zukunft ist nichtdeterministisch. Dieses

Zeitmodell besitzt eine baumähnliche Struktur, da sich die Menge aller möglichen Pfade

eines Modells als Baum darstellen lässt. Hieraus stammt auch der Name dieser Logik,

Berechnungsbaumlogik.

CTL ist syntaktisch eng mit LTL verbunden, da es die gleichen temporalen Operatoren

benutzt. CTL ist im Vergleich zu LTL aber eine syntaktisch sehr restriktive Logik. Dies

schränkt ihre Ausdrucksstärke stark ein.

3.5.1 Syntax von CTL

Formeln in CTL enthalten Paare von temporalen Konnektoren, die aus einem

Pfadquantor gefolgt von einem temporalen Operator bestehen. Die Pfadquantoren sind

die Symbole und A E , die temporalen Operatoren die Symbole und U . Diese

Konnektoren dürfen in einer syntaktisch korrekten Formel nie getrennt vorkommen. Die

Syntax einer Formel in CTL wird in BNF nach [HR01] folgendermaßen definiert:

GFX ,,

12


( ) ( ) ( ) ( ) ( ))(|)(||

||||||||||::pUpEpUpAEGpAGp

EFpAFpEXpAXppppppppppPp ↔→∨∧¬=

P bezeichnet hier eine beliebig atomare aussagenlogische Formel.

Die höchste Bindung besitzen die unären Operatoren AGEFAFEXAX ,,,,,¬ und .

Danach folgen

EG

∧ und . Als letztes kommen → , ∨ ↔ sowie und . Zur

eindeutigen Bindung können beliebig zusätzliche Klammern gesetzt werden.

AU EU

Mit obigen Regeln können zu den Umformungsmöglichkeiten der Aussagenlogik

folgende weitere Umformungen vorgenommen werden:

• ( )pUtrueAAFp ≡

• ( )pUtrueEEFp ≡

• ( )pUtrueEAGp ¬¬≡

• ( )pUtrueAEGp ¬¬≡

3.5.2 Semantik von CTL

Zur Definition der Semantik von CTL wird analog zur Definition der Semantik von

LTL neben der Definition des Rahmens noch eine Auswertungsfunktion benötigt, die

jedem Zustand die Menge der in dem jeweiligen Zustand gültigen atomaren Aussagen

zuweist. Der verwendete Rahmen besitzt hier keine lineare, sondern eine verzweigte

Zeitstruktur. Die um die Auswertungsfunktion erweiterte Zeitstruktur

enthält die Menge der Zustände , die Übergangsrelation über diesen

Zuständen, die jedem Zustand mindestens einen Nachfolger zuweist, und die

Auswertungsfunktion

( )LRSM ,,=

S SSR ×⊆

( )PePotenzmengSL →: , die jedem Zustand eine Teilmenge der

Menge P aller atomaren Aussagen zuweist, die in diesem Zustand gültig sind.

Im folgenden bedeutet ⊨isM , p , dass die Formel p im Zustand für die Struktur is M

gültig ist. Ist die Struktur klar, so kann das Symbol M weggelassen werden und es wird

nur ⊨is p geschrieben. Die Semantik von CTL ist wird nach [CE81] über strukturelle

Induktion folgendermaßen definiert:

1. ⊨0s P gdw. , für eine atomare aussagenlogische Formel )( 0sLP ∈ P .

2. ⊨0s p¬ gdw. ⊭0s p

13


3. ⊨0s ( )21 pp ∧ gdw. ⊨ und ⊨ . 0s 1p 0s 2p

4. ⊨ gdw. für alle Pfade 0s AXp ( ),..., 10 ss gilt: ⊨1s p .

5. ⊨ gdw. für mindestens einen Pfad 0s EXp ( ),..., 10 ss gilt: ⊨1s p .

6. ⊨ gdw. für alle Pfade 0s ( 21 pUpA ) ( ),..., 10 ss für mindestens ein gilt:

⊨ und für alle

0≥i

is 2p ij <≤0 gilt: ⊨ . js 1p

7. ⊨ gdw. für mindestens einen Pfad 0s ( 21 pUpE ) ( ),..., 10 ss für mindestens ein

gilt: ⊨ und für alle 0≥i is 2p ij <≤0 gilt: ⊨ . js 1p

Die übrigen Operatoren werden an dieser Stelle nicht explizit definiert, da diese sich

über die Umformungsregeln ableiten lassen.

Der Pfadquantor bedeutet, dass eine Aussage für alle Pfade gilt, der Pfadquantor A E

besagt, dass eine Aussage für mindestens einen Pfad gilt. Die temporalen Operatoren

X , ,G und U besitzen dieselbe Bedeutung wie in der Logik LTL. F

Die folgenden Abbildungen zeigen die Bedeutungen der Formeln grafisch. In den

Abbildungen sind diejenigen Zustände ausgefüllt, in denen die Aussage p wahr ist. In

den schraffiert dargestellten Zuständen ist die Aussage q wahr. Die Wurzel der

abgebildeten Bäume stellt den aktuellen Zustand dar, in dem die jeweilig angegebene

Formel wahr ist. Jeder Knoten besitzt hier genau zwei Nachfolger. Dies muss nicht

grundsätzlich der Fall sein. Jeder Knoten muss mindestens einen Nachfolger besitzen.

Jeder dargestellte Pfad geht unendlich lange weiter. Zur Veranschaulichung ist die

verwendete Baumtiefe ausreichend.

EXp EFp EGp E(p U q)

14

AXp AFp AGp A(p U q)


3.5.3 Semantische Äquivalenzen

Zwei Formeln p und in CTL sind genau dann äquivalent, wenn in jedem Zustand

eines beliebigen Modells, in dem eine der beiden Formeln erfüllt ist, gleichzeitig auch

die andere Formel gilt.

q

Zur vollständigen Ausdrucksstärke genügt es, die Logik CTL über der Menge der

Operatoren , und ∧ zusammen mit false ¬ EX , ( )UE und zu definieren. Alle

anderen Operatoren lassen sich daraus ableiten. Dafür müssen die folgenden

Äquivalenzen bekannt sein:

EG

pEGAFp ¬¬≡

( )pUtrueEEFp ≡

pEXAXp ¬¬≡

( )pUtrueEAGp ¬¬≡

( ) ( )( )( )qEGqpUqEqUpA ¬∨¬∧¬¬¬≡

Die vollständige Ausdrucksstärke lässt sich auch über andere Operatoren umsetzen.

3.5.4 CTL Model Checking

Der Ausgangspunkt des Model Checking ist die Frage, ob in einem gegebenen Modell,

das sich in einem bestimmten Zustand befindet, eine gegebene Formel in diesem

Zustand wahr ist oder nicht. Die Gleichung ⊨sM , p wird als ein Berechnungsproblem

betrachtet. Alternativ könnte auch nur ein Modell und eine Formel gegeben sein, und es

interessiert die Menge der Zustände, für die diese Formel gültig ist. Dieses Problem

würde die erste Fragegestellung automatisch mit beantworten.

Die zweite Fragestellung lässt sich mit Hilfe des sogenannten Markierungsalgorithmus

berechnen. Dieser läuft folgendermaßen ab: Als Eingabe wird ein Modell M und eine

Formel p erwartet. Die Formel p muss in CTL sein und darf nur die Operatoren

, und ∧ zusammen mit false ¬ EX , ( )UE und besitzen, alle anderen Konnek-

toren müssen vor der Anwendung des Algorithmus entsprechend semantisch äquivalent

umgeformt werden. Die angegebenen Konnektoren sind zur Vollständigkeit der

Ausdrucksstärke von CTL ausreichend. Der Algorithmus gibt die Menge der Zustände

des Modells

AF

M aus, welche die Formel p erfüllen. Der erste Schritt des Algorithmus

15


besteht darin, die Potenzmenge der Teilformeln der Formel p zu bilden. Beginnend mit

der kürzesten Teilformel wird mit jedem Element dieser Potenzmenge einer der

nachfolgenden Schritte durchgeführt. Dieser Schritt hängt vom Inhalt der Teilformel ab:

• : Es wird kein Zustand markiert. false

• p : Alle Zustände werden markiert, für die gilt: ( )sLp ∈ .

• qp ∧ : Markiere alle Zustände mit qp ∧ , die bereits sowohl mit p als auch mit

markiert sind. q

• p¬ : Markiere alle Zustände mit p¬ , die nicht bereits mit p markiert sind.

• : Falls es irgendeinen Zustand gibt, der bereits mit AFp p markiert ist, so

markiere diesen mit . Markiere solange alle Zustände mit , dessen

Nachfolger alle bereits mit markiert sind, bis sich keine Änderungen mehr

ergeben.

AFp AFp

AFp

• : Markiere alle Zustände mit ( qUpE ) ( )qUpE , die bereits mit markiert

sind. Markiere solange alle Zustände mit

q

( )qUpE , die bereits mit p markiert

sind und mindestens einen unmittelbaren Nachfolger besitzen, der bereits mit

markiert ist, bis keine weiteren Änderungen möglich sind. ( qUpE )

• : Markiere jeden Zustand mit , der mindestens einen unmittelbaren

Nachfolger besitzt, der bereits mit

EXp EXp

p markiert ist.

Wurde dieser Algorithmus mit allen Teilformeln und der zu prüfenden Formel selber

durchgeführt, so müssen die Zustände gesucht werden, die mit der zu prüfenden Formel

markiert sind. Für die Menge dieser Zustände ist die eingegebene Formel gültig.

Dieser Algorithmus besitzt die Komplexität ( )( )EVVfO +⋅⋅ . Hierbei ist die Anzahl

der Konnektoren der zu prüfenden Formel, V entspricht der Menge der Zustände des

Modells und

f

E entspricht der Anzahl der Zustandsübergänge. Zur Laufzeitver-

besserung können in der zu prüfenden Formel auch mehr als nur die minimal benötigte

Menge an zulässigen Konnektoren erlaubt werden. Das Problem der Zustandsexplosion

bleibt jedoch auch bei diesen Verbesserungen erhalten. Unter diesem Problem wird die

exponentiell mit der Anzahl der Programmvariablen wachsende Menge der Zustände

eines Modells verstanden.

16


3.5.5 Anwendung des Markierungsalgorithmus

Gegeben sei ein beliebiges Modell dargestellt als gerichteter Graph. Mit Hilfe des

Markierungsalgorithmus sollen alle Zustände gefunden werden, in denen eine gegebene

Formel wahr ist. Dazu werden der nachfolgende Graph und die Formel

untersucht. Der Zustand, in dem die Teilformel

F EFp

p wahr ist, ist entsprechend beschriftet.

ps0 s1 s2 s3

Zur Anwendung des Markierungsalgorithmus wird die Formel so umgeformt, dass

nur Teilformeln enthalten sind, für die der Algorithmus definiert ist.

EFp

( ) ( )pUfalseEpUtrueEEFp ¬≡≡

Als nächstes wird diese Formel in ihre Teilformeln zerlegt. Zusätzlich werden die

Teilformeln der Länge nach sortiert, so dass der Algorithmus der Reihenfolge der Länge

der Teilformeln nach auf jede Teilformel angewandt werden kann. Die Menge der

Teilformeln ergibt:

( )pUfalseEfalsefalsep ¬¬ ,,,

Im ersten Schritt wird der Algorithmus für die Teilformeln der Länge eins, p und

, durchlaufen. Es werden alle Zustände mit false p markiert, in denen die Teilformel

p gilt, dies ist nur der Zustand . Die boolsche Konstante ist immer falsch,

daher werden hiermit keine Zustände markiert. Im zweiten Schritt wird der Algorithmus

auf die Teilformel angewandt. Diese ist überall wahr, daher wird hiermit jeder

Zustand markiert. Im letzten Schritt wird die Formel

1s false

false¬

( )pUfalseE ¬ angewandt. Dazu

werden mit dieser Formel zuerst alle Zustände markiert, in denen p gilt, dies ist

Zustand . Im weiteren werden die Zustände markiert, welche bereits mit

markiert sind und mindestens einen unmittelbaren Nachfolger besitzen, der mit

1s false¬

p

markiert ist. Dies wird solange wiederholt bis keine Änderungen mehr erfolgen. Dabei

wird zuerst Zustand und dann markiert. Danach erfolgen keine weiteren

Änderungen. Damit ist die Formel in den Zuständen , und gültig.

0s 2s

EFp 0s 1s 2s

17


3.6 Fixpunktcharakterisierung

Der zuvor dargestellte Algorithmus nutzt die Eigenschaft, dass sich die Operatoren

temporaler Logiken als Fixpunkte monotoner Funktionale berechnen lassen.

Funktionale werden in der Form fy.λ geschrieben, wobei die Formel und die

Variable bezeichnen. Ein Fixpunkt eines Funktionals ist gegeben, wenn

f y

f ( ) ppf =

gilt. Ein Funktional ist monoton, wenn für alle Teilmengen f x , seiner Definitions-

menge gilt: Aus

y

S yx ⊆ folgt ( ) ( )yfxf ⊆ . Monotone Funktionale besitzen nach

[Ta55] einen kleinsten sowie einen größten Fixpunkt. Zur Berechnung des kleinsten

Fixpunktes wird als Startwert die leere Menge übergeben. Der größte Fixpunkte wird

berechnet, indem als Startwert die Menge aller Elemente der Definitionsmenge

übergeben wird. Auf diese Startwerte wird die Funktion solange auf sich selber

angewandt, bis keine Änderung des Funktionswertes mehr erfolgt. Zur Berechnung der

Fixpunkte der Operatoren einer temporalen Logik wird die Funktion einmal mit

und einmal mit gestartet. Auf das Model Checking übertragen, entspricht dies

einmal der leeren Menge und einmal der Menge der Zustände eines Modells. Diese

Menge ist endlich, da nur Systeme betrachtet werden, die sich in endlichen Modellen

darstellen lassen. Bei einer endlichen Zustandsmenge mit Zuständen muss ein

monotones Funktional maximal -mal auf sich selber angewandt werden, um einen

Fixpunkt zu finden.

false

true

n

f n

Die Fixpunktcharakterisierung der Operatoren von CTL führt zu folgendem Ergebnis,

wobei fy.µ den kleinsten und fy.ν den größten Fixpunkt bezeichnet.

yAXpyAGp ∧= .ν

yEXpyEGp ∧= .ν

yAXpyAFp ∨= .µ

yEXpyEFp ∨= .µ

( ) ( yAXqpypUqA ∧∨= . )µ

( ) (( )yEXqpypUqE ∧∨= . )µ

18

Diese Darstellung der Operatoren als Fixpunkte wird im obigen Algorithmus für das

Model Checking ausgenutzt. Da hiermit gezeigt ist, dass jede Fixpunktberechnung

höchstens so viele Schritte erfordert, wie das entsprechende Modell Zustände enthält, ist

auch bewiesen, dass der Markierungsalgorithmus terminiert.


3.7 Theoretische Aspekte temporaler Logiken

In diesem Abschnitt werden theoretische Aspekte der dargestellten temporalen Logiken

untersucht. Hier geht es darum, Aussagen über die Entscheidbarkeit, Ausdrucksstärke

und Komplexität zu treffen und die verschiedenen Logiken daraufhin zu vergleichen.

Die Entscheidbarkeit ist sowohl bei LTL als auch bei CTL gegeben. Die Grundlage

hierfür ist darin begründet, dass beide Logiken auf der Aussagenlogik basieren, die

ebenfalls entscheidbar ist. Weiter wurde durch die Angabe eines Algorithmus zum

Model Checking gezeigt, dass Aussagen in CTL in endlicher Zeit überprüfbar sind. Für

LTL existieren ebenso Algorithmen. Eine Möglichkeit besteht hier, ein System als

Büchi-Automat darzustellen.

Die Komplexität des dargestellten Markierungsalgorithmus liegt in deterministisch

polynomieller Zeit bezüglich der Modellgröße und der Formellänge. Die Komplexität

der bekannten Algorithmen für LTL Formeln ist weitaus größer und befindet sich in der

Klasse PSPACE-vollständig.

Bezüglich der Ausdrucksstärke sind LTL und CTL unvergleichbar. Es entsteht zunächst

der Eindruck, dass CTL gegenüber LTL ausdrucksstärker ist, da hier zusätzlich zu den

temporalen Operatoren Pfadquantoren erlaubt sind, die Bedeutungen für einzelne

Berechnungspfade besitzen. In einem anderen Punkt ist jedoch LTL ausdrucksstärker.

In LTL sind bestimmte Verschachtelungen boolscher Konnektoren mit den temporalen

Operatoren erlaubt, die in CTL nicht gestattet sind. Daher ist weder LTL noch CTL

ausdrucksstärker. Vielmehr ist es möglich, bestimmte Aussagen in beiden Logiken

auszudrücken. Daher bilden die Ausdrucksmöglichkeiten beider Logiken nur eine

Schnittmenge.

CTL LTL

Die Formel ist nur in CTL enthalten, nicht aber in LTL. Die hier angegebenen

Pfadquantoren existieren in LTL nicht, daher sind dort Aussagen über alle oder nur

einige Pfade nicht möglich. Diese Möglichkeit ist nur in CTL gegeben.

EFpAG

19

Kapitel 4: Zusammenfassung

Die Formel ist nur in LTL enthalten, nicht aber in CTL. Würde diese

Formel in CTL um den Pfadquantor ergänzt, so hätte die neue Formel nicht die

gleiche Bedeutung. Außerdem können in CTL temporale Operatoren nicht wie in LTL

unmittelbar nacheinander folgen.

FqGFp →

A

Die Formel ( )AFqpAG → ist sowohl in CTL als auch in LTL enthalten, da diese

Formel aus syntaktischer Sicht um den Operator gekürzt werden kann, so dass nur

noch übrig bleibt. Dies sagt in LTL immer noch dasselbe aus, da nur ein

Zeitpfad betrachtet wird. Semantisch bedeutet die Formel, dass (für alle Pfade) immer

gilt:

A

( FqpG → )

p impliziert, dass (für alle Pfade) irgendwann q gilt. Dies ist auch in CTL (für

alle Pfade) der Fall, da jeder temporaler Operator den Pfadquantor besitzt. Da in

LTL nur ein Pfad betrachtet wird, entspricht dies der Formel ohne in LTL.

A

A

4 Zusammenfassung

Soft- und Hardwaresystemen lassen sich neben dem Testen auch durch Beweise auf

Korrektheit prüfen. Eine Möglichkeit ist, dies mittels Model Checker durchzuführen.

Dafür wird vorausgesetzt, dass sich ein zu prüfendes System als endliches Modell

darstellen lässt. Model Checker erlauben zudem nur die Prüfung bestimmter Eigen-

schaften wie z. B. Lebendigkeit oder Deadlockfreiheit. Diese Eigenschaften müssen in

einer formalen Spezifikation dargestellt werden. Dazu werden temporale Logiken

benötigt, die eine Erweiterung der Aussagen- oder auch der Prädikatenlogik sind. Diese

Logiken basieren auf unterschiedlichen Zeitmodellen. Unterschieden werden lineare

und verzweigte Zeitmodelle. Die Logik LTL basiert auf einem linearen Zeitmodell,

CTL dagegen basiert auf einem verzweigten Zeitmodell. Der Algorithmus des CTL

Model Checking erwartet als Eingabe die Spezifikation einer zu prüfenden Eigenschaft

in einer temporalen Logik und ein Modell des zu prüfenden Systems. Dieses Modell

enthält die Zustände, Zustandsübergänge und Auswertungsfunktion. Der vorgestellte

Markierungsalgorithmus berechnet die Menge der Zustände, in denen eine gegebene

Formel in CTL gültig ist. Die Grundlage dieses Algorithmus ist die Fixpunkt-

charakterisierung. Diese besagt, dass jede monotone Funktion einen kleinsten und einen

größten Fixpunkt besitzt, die sich bei endlicher Anwendung der Funktion auf sich selber

berechnen lassen. Da die Systeme endlich sind, lässt sich dies auf das Model Checking

übertragen. Als Fixpunkte ergeben sich die Operatoren der temporalen Logiken.

20

Literaturverzeichnis

[Bu84] Burges, John. P.: Basic tense logic. In: Handbook of philosophical logic. Band II: Extensions of Classical Logic. Hrsg.: D. Gabbay, F. Guenthner. Dordrecht, Bosten, Lancester 1984, S. 89-133.

[CE81] Clarke, Edmund M.; Emerson, E. Allen: Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In: Lecture Notes on Computer Science, Hrsg.: Dexter Kozen, Band 131, 1981, S. 52-71.

[Em90] Emerson, E. Allen: Temporal and Modal Logic. In: Formal Models and Semantics. Hrsg.: Jan van Leeuwen, Band B, Amsterdam u.a. 1990, S. 995-1072.

[HR01] Huth, Michael; Ryan, Mark: Logic in Computer Science, Cambridge 2001.

[Mc93] McMillan, Kenneth L.: Symbolic Model Checking, Boston u.a. 1993.

[Sc00] Schöning, Uwe: Logik für Informatiker, 5.Aufl., Heidelberg, Berlin 2000.

[Ta55] Tarski, Alfred: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 1955, S. 285-309.

Temporale Logiken: CTL und LTL - wi1.uni- · PDF fileTemporale Logiken: CTL und LTL im Rahmen...

Documents

Transcript of Temporale Logiken: CTL und LTL - wi1.uni- · PDF fileTemporale Logiken: CTL und LTL im Rahmen...