Was ist Model Checking? 1 - LMU, Informatik, TCS · Model checking is an automatic technique for...

1Was ist Model Checking?

”Model checking is an automatic technique for verifyingcorrectness properties of safety-critical reactive systems“

[Clarke, Schlingloff: Model Checking, in Handbook of Automated Reasoning,Band II, S. 1637–1790, 2001]

Erlauterung:

• Reaktives System

• Korrektheitseigenschaften

• Verifikation

• Automatische Technik

• Sicherheitskritisch

1



Reaktives System:

• besteht aus Komponenten, die miteinander und der Systemumgebunginteragieren

• z.B. Schaltungen, Betriebssysteme, World-Wide Web, Protokolle

• System muss nicht terminieren

• im Gegensatz zu funktional (oder transformationell) beschreibbaren Sy-stemen mit klarem Ein/Ausgabe-Verhalten

2



Korrektheitseigenschaften:

• i.d. Regel temporale Eigenschaften des gewunschten Verhaltens

• ein System erfullt diese Eigenschaften, wenn jeder Ablauf des Systemssie erfullt

• diese Eigenschaften werden in einer temporalen Logik beschrieben alssog. Kripke-Modell

• Systemkorrektheit = Wahrheit von logischen Formeln in Modellen (daherder Name

”Model Checking“)

3



Verifikation:

• formales Verfahren, benotigt:

• Modellierungssprache zur Systembeschreibung:System wird als (endlicher) Zustandsubergangsgraph modelliert

• Spezifikationssprache zur Formulierung der Eigenschaften:Eigenschaften werden in einer temporalen Aussagenlogik spezifiziert

• Verfahren (Kalkul) fur den Verifikationsprozess:Suchverfahren, das den Zustandsubergangsgraph exploriert und die Ei-genschaften in jedem Zustand uberpruft

4



Automatische Technik:

• im Gegensatz zu Verfahren wie z.B. Interaktives Theorembeweisen: allge-meinerer, ausdrucksstarkerer Ansatz, benotigt aber Interaktionen hoch-qualifizierter menschlicher Experten

• Eigentlicher Verifikationsprozess ist voll automatisiert und pruft i.A.alle moglichen Systemzustande (setzt Endlichkeit des Zustandsraumesvoraus)

• Verifikationsverfahren terminiert (theoretisch) immer und zeigt, ob dasSystemmodell die Eigenschaft erfullt; falls nicht, liefert das Verfahren einGegenbeispiel

5



Sicherheitskritisch:

• Sicherheit im Sinne von”safety“ (nicht

”security“)

• Die Anzahl und die Komplexitat sicherheitskritischer Anwendungennimmt standig zu

• Fehler in solchen Anwendungen sind teuer (z.B. ARIANE-5, Pentium)

6



[Clarke, Schlingloff: Model Checking, in Handbook of Automated Reasoning,Band II, S. 1637–1790, 2001]

Erlauterung:

• Reaktives System

• Korrektheitseigenschaften

• Verifikation

• Automatische Technik

• Sicherheitskritisch

7

2Rechnergestutzte (”

computer-aided“) Verifikation

Allgemeiner formaler Ansatz zur Verifikation:

• Bildung eines mathematischen Modells des Systems

• Korrektheitsaussage ist eine mathematisch beweisbare oder widerlegbareBehauptung

Alternative Ansatze zur formalen Verifikation:

• Testen

• Simulation

bieten keine Korrektheitsgarantie und sind u.U. nur eingeschranktanwendbar

8

3Bedeutung der formalen Verifikation

Zunehmende Verbreitung sicherheitskritischer HW und SW-Systeme:

• Beispiele: Elektronischer Handel, Telefonnetze, Luftverkehrskontrolle,Medizinische Instrumente, Agentensysteme, Autonome Systeme, . . .

• Erhohte Sicherheitsstandards (z.T. vom Gesetzgeber)

• Haftungsproblematik

Zunehmende Komplexitat der Systeme:

• Vergrosserung der Wahrscheinlichkeit subtiler Fehler

• Testen und Simulation reichen nicht mehr aus und sind zu zeitaufwendig

• Grosse Menge an Verifikationsaufgaben erfordert automatische Un-terstutzung

9

4Methoden der formalen Verifikation

Model Checking-Paradigma vs.

Interaktives Theorembeweisen:

• Verifikations-Aufgaben werden in einer moglichst ausdrucksstarken Spra-che formuliert (z.B. Logik hoherer Ordnung)

• Experte fuhrt einen mathematischen Beweis der Korrektheit

• unter Zuhilfenahme eines interaktiven Beweisers, der

• die vorgegebenen Schritte des Experten auf Korrektheit uberpruft,• leichte Teilaufgaben mit Hilfe vorgegebener Heuristiken (Taktiken) zu

losen versucht,• aber i.A. unvollstandig ist

10

5Methodologie der Verifikation beim Model Checking

)

PPPPPPPPPPPPPq

)

PPPPPPPPPPPPPq

6 6

Spezifikation

Modifiziere

Gegenbeispiel

Teste nachste

Korrektheit

Abstraktes Modell

Verifikationstool

11

6Ein Beispiel aus der Anwendung

Futurebus+ Protokoll zur Cache-Koharenz (IEEE 1994)

• Sichert Konsistenz der Daten in hierarchischen Systemen aus vielenProzessoren und Caches, die durch Busse verbunden sind

• Grundidee der Koharenzsicherung:Alle Caches beobachten alle Bus-Transaktionen

• Zur Performanzsteigerung ist Splitten von Transaktionen erlaubt, d.h.:

• Beenden einer Transaktion kann verzogert und Bus freigegeben werden• Zwischenzeitlich Ausfuhrung lokaler Aktionen• Zur Beendigung der Transaktion explizite Meldung an Bus

12

7Verifikation des Futurebus+ Protokolls

Automatische Verifikation mit Model Checker SMV

• Standard spezifiziert mogliche Zustande der Cache-Daten in jedem Pro-zessor und den Zustandswechsel in jeder Transaktion

• Besteht aus ca. 300 sog. Attributen, d.h. im Wesentlichen:Boolesche Variablen und Regeln zu ihrer Modifikation

• Modellierung des Problems in SMV:

• zur Formulierung der Attribute ca. 2300 Codezeilen in SMV-Sprache• Formulierung benutzt Abstraktionen• SMV erstellt automatisch interne Reprasentation des Modells (BDDs)• Korrektheitseigenschaften formuliert in temporaler Logik (CTL)

• SMV findet automatisch Fehler im Standard

13

8Fehlerszenario im Futurebus+ Protokoll

SSSSSSSSSw

7

SSSSSSSSSw

SSSSSSSSSw

7

SSSSSSSSSw

SSSSSSSSSw

7

-

-

-

SSSSSSSSSw

7

P1

P2

Bus

data2exclusive

data1

data1shared-unmod

shared-unmod

invalid

invalid

invalid

invalid

invalidateread-shared

read-mod

data1

data1 data1 data2data1

data1exclusive

invalid

Behebung des Fehlers:

P1 muss in Zustand shared-unmod gehen, wenn er die read-mod-Transaktion splitted

14

9Anwendungen des Model Checking

Hardware-Verifikation

• Schaltungen, Pipelines, und Protokolle

• Verwendung als Debugging-Werkzeug

• Interne Verifikations-Gruppen in Firmen wie ATT, Fujitsu, Lucent, IBM,Intel, Motorola, Siemens

• Passt zum Design-Ablauf: Simulation, Synthese, Verifikation

Software-Verifikation

• Modellierung auf hoherer Abstraktionsebene eher unublich

• Anwendungen: Protokolle, Telekommunikation

Kontrollsysteme

• Beginnende Anwendungen: Luftfahrtkontrolle, Robotik

15

10Beschrankungen des Model Checking

• Geeignet fur Kontroll-intensive Anwendungen mit interessanten Interak-tionen zwischen Komponenten

• Komplexitatsproblematik fur grossere Anwendungen: Problemklassenu.U. NP-hart, PSPACE-hart, EXPTIME-hart

• Falsifikation anstatt Verifikation: liefert Fehlerdiagnose aber keinen nach-prufbaren Beweis der Korrektheit (Problem der Korrektheit des ModelCheckers)

• Allgemeine Modellierungsproblematik: Nicht das System, sondern seinModell wird verifiziert

• Modellierungsproblematik fur nicht als endliche Zustandssysteme be-schreibbare Anwendungen: Abstraktion nicht automatisch

16

11Modellierung reaktiver Syteme

Hauptziele der Modellierung: Kontrolle und Interaktion

• keine komplexen Datenstrukturen, keine aufwendige Datenmanipulation

• explizite Konstrukte fur Nichtdeterminismus

• Modellierung von System und Umgebung

• Modellierung auf verschiedenen Abstraktionsebenen

• Einfache Operatoren und prazise mathematische Semantik

Mathematische Modellierungswerkzeuge

• ω-Automaten

• Temporale Logik

17

12Korrektheitsanforderungen an reaktive Syteme

Zwei Haupttypen von Korrektheitsanforderungen

• Universeller Typus:”Ein bestimmter Zustand tritt nie auf“

Beispiel:Niemals gleichzeitig grun fur zwei Ampeln auf kreuzenden Strassen

• Existenzieller Typus:”Ein bestimmter Zustand wird schliesslich immer

erreicht“Beispiel:Jede intakte Ampel schaltet nach endlicher Zeit auf grun.

18

13Aussagenlogik

Syntax der Aussagenlogik

• Gegeben eine Menge P von Aussagenvariablen.

• Die (Formeln der) Aussagenlogik fur P sei(en) definiert durch:

PL(P) := P | ⊥ | (PL→ PL)

• Andere Konnektive ausser ⊥ und → seien wie ublich als Abkurzungendefiniert: ¬A := (A→ ⊥), > := ¬⊥, A ∨B := (¬A→ B),A ∧B := ¬(¬A ∨ ¬B), A↔ B := ((A→ B) ∧ (B → A)).

• Die Prazedenz der Operatoren sei wie folgt festgelegt: ¬,∧,∨,→,↔.Evtl. werden Klammern eingespart und der Parameter P.

• Beispiel: stack1 is empty ∨ ¬stack1 is empty ∧ stack2 is empty

19

14Semantik der Aussagenlogik

Interpretation

• Gegeben eine Aussagenlogik PL(P).

• Eine Interpretation fur PL(P) ist ein Paar 〈U , ι〉 wobei

• das Universum U = true, false und

• die Belegung ι eine Abbildung ι : P −→ U ist.

Fortsetzung einer Interpretation auf Formeln

• Induktiv definiert wie folgt:

• I erfullt p ∈ P, geschrieben I |= p, gdw ι(p) = true,

• I 6|= ⊥,

• I |= (A→ B) gdw I 6|= A oder I |= B.

20

15Bedeutung der Aussagenlogik

Zentrale Rolle in der Komplexitatstheorie

• Erfullbarkeitsproblem ist NP-vollstandig.

• Dennoch gibt es heute leistungsfahige Entscheidungsverfahren

Wichtig als Problem-Spezifikationssprache

• Fur Hardware-Verifikation, Planungsprobleme

• Zunehmend fur weitere Bereiche via effizienter Ubersetzungsverfahren

Fur das Model Checking

• Erfullung einer Formel durch eine Interpretation ist effizient entscheidbar

• Reine Aussagenlogik reicht i.A. nicht zur Modellierung reaktiver Systeme

21

16Pradikatenlogik fur Transitionssysteme

Explizite Modellierung von Transitionssystemen

Syntax der Pradikatenlogik fur Transitionssysteme

• Erweiterung der aussagenlogischen Variablen um eine Argumentstelle furZeitpunkte, explizite Beschreibung von Zustandsubergangen

• Gegeben eine Menge P von 1-stelligen Pradikaten, eine Menge T vonZustandsvariablen, eine Menge R von 2-stelligen Transitionspradikaten,und sei R+ = R∪ ≺, <,=.• Die (Formeln der) Pradikatenlogik fur Transitionssysteme fur P, T undR sei(en) definiert durch: FOL(P, T ,R) :=

P(T ) | ⊥ | (FOL→ FOL) | R+(T , T ) | ∃T FOL

• Analoge Abkurzungen wie in der Aussagenlogik, evtl. Infixnotation, sowie∀tA := ¬∃t¬A, t ≤ t′ := t < t′ ∨ t = t′, etc.

22


Semantik der Pradikatenlogik fur Transitionssysteme

• Gegeben eine Pradikatenlogik fur Transitionssysteme FOL(P, T ,R).

• Interpretation ist ein Paar 〈U , ι〉 mit

• Universum U : nichtleere Menge von Zeitpunkten

• Belegung ι ist eine Funktion mit folgenden Eigenschaften:fur alle p ∈ P : ι(p) ⊆ U , fur alle R ∈ R : ι(R) ⊆ U × U ,ι(=) := 〈s, s〉 | s ∈ U, die Gleichheit,ι(≺) :=

⋃ι(R) | R ∈ R, die Transitionsrelation,

ι(<) ist die transitive Hulle von ι(≺), die Erreichbarkeitsrelation.

• Weiterhin sei V : T −→ U , eine Variablenzuweisung.

Im Model Checking: 〈I,V〉, hier auch geschrieben: IV, heisst Modell

23


Beispiele fur Formeln der Pradikatenlogik fur Transitionssysteme

1. stack is empty(t0)→ ∃t1(put(t0, t1) ∧ ¬stack is empty(t1))

Auf den leeren Stack kann etwas gelegt werden.

2. ∀t1((t0 ≤ t1 ∧ request(t1))→ ∃t2(t1 < t2 ∧ acknowledge(t2)))

Jede Anfrage wird irgendwann beantwortet.

3. ∀t1((t0 ≤ t1 ∧ request(t1))→ ∃t2(t1 < t2 ∧ acknowledge(t2))∧∀t3((t1 < t3 ∧ t3 < t2)→ request(t3))))

Keine Anfrage wird geloscht, bevor sie beantwortet ist.

25

20Prinzip des Model Checking

Formale Reprasentation des Verhaltens eines Transitionssystems

• als Modell (IV) einer logischen Sprache L(z.B. der Pradikatenlogik fur Transitionssysteme)

Formale Reprasentation der Eigenschaften eines Transitionssystems

• als Formel A der Sprache L(z.B. der Pradikatenlogik fur Transitionssysteme)

Formales Uberprufen einer Eigenschaft des Transitionssystems

• Formales prufen, ob das Modell die Formel A erfullt: IV |= A ?

• Falls das Universum U des Modells endlich ist, lasst sich aus der Definitionder Semantik direkt ein Entscheidungsverfahren gewinnen.

26

21Modellierung eines Ampel-Verkehrs-Systems

• 1-stellige Zustandspradikate:P = ampel rot, ampel gruen, verkehr fliesst, verkehr steht• 2-stellige Transitionspradikate:R = ampel schaltet, verkehrsfluss wechselt

System-Modell als Transitionsgraph

?

6

- ampel rotverkehr steht

ampel gruenverkehr steht

ampel gruenverkehr fliesst

ampel rotverkehr fliesst

ampel schaltet

verkehrsfluss wechselt


ampel schaltet

s1 s2

s4 s3

27

22Interpretation I = 〈U , ι〉 des Ampel-Verkehrs-Systems

?

6





ampel schaltet



ampel schaltet

s1 s2

s4 s3

• Universum U = s1, s2, s3, s4• Belegung ι:ι(ampel rot) = s1, s2, ι(ampel gruen) = s3, s4,

ι(verkehr steht) = s2, s3, ι(verkehr fliesst) = s1, s4,ι(ampel schaltet) = 〈s2, s3〉, 〈s4, s1〉,ι(verkehrsfluss wechselt) = 〈s1, s2〉, 〈s3, s4〉

28

23Eigenschaften des Ampel-Verkehrs-Systems

Beispiele fur Systemspezifikationen und ihre Verifikation

1. Die Ampel steht (immer) entweder auf rot oder auf grun.

A = ∀t(ampel rot(t)↔ ¬ampel gruen(t))

Erfullt das System die Eigenschaft, d.h. gilt I |= A?

Beweis: I |= A gdw fur alle Variablenzuweisungen V fur U gilt:IV |= (ampel rot(t)↔ ¬ampel gruen(t)) gdw fur alle V gilt:

entweder V(t) ∈ ι(ampel rot) oder V(t) ∈ ι(ampel gruen),

d.h. gdw ι(ampel rot) ∪ ι(ampel gruen) = U undι(ampel rot) ∩ ι(ampel gruen) = ∅

29

24Eigenschaften des Ampel-Verkehrs-Systems

2. Die Ampel steht (von jedem Zustand aus) irgendwann auf grun.

A = ∀t∃t′(t ≤ t′ ∧ ampel gruen(t′))

Beweis: I |= A gdw fur alle Variablenzuweisungen V fur U gilt:IV |= A′ = ∃t′(t ≤ t′ ∧ ampel gruen(t′));

Fall 1 (von 4): V(t) = s1: IV |= A′ gdw es gibt ein V ′ mit V ′(v) = V(v)fur alle v 6= t′ und IV ′ |= (t ≤ t′ ∧ ampel gruen(t′));

wahle ein solches V ′ mit z.B. V ′(t′) = s3; dann gilt:

(i) 〈V ′(t),V ′(t′)〉 ∈ ι(≤) und damit IV ′ |= (t ≤ t′) und

(ii) IV ′ |= ampel gruen(t′);

Damit gilt die Behauptung fur V(t) = s1. Die anderen Falle gehen analog.

30

25Beziehungen zwischen Spezifikationsformeln

Beziehungen zwischen FOL-Formeln

Gegeben zwei Formeln A und B einer Pradikatenlogik fur Transitionssysteme(FOL(P, T ,R)):

• A impliziert B, geschrieben A |= B, gdw jedes Modell, das A erfullt,auch B erfullt,

• A impliziert B schwach gdw jede Interpretation, die A erfullt, auch Berfullt,

• A und B heissen aquivalent gdw sie sich gegenseitig implizieren,

• A und B heissen schwach aquivalent gdw sie sich gegenseitig schwachimplizieren.

31


1. A = ∀t∃t′(t ≤ t′ ∧ ampel gruen(t′))B = ∃t′(t ≤ t′ ∧ ampel gruen(t′))A impliziert B, aber B impliziert A lediglich schwach.⇒ A und B sind nicht aquivalent, aber schwach aquivalent.

Interpretation des Ampel-Verkehrs-Systems, die A und B erfullt:

?

6





ampel schaltet



ampel schaltet

s1 s2

s4 s3

32



Interpretation des Ampel-Verkehrs-Systems, die weder A noch B erfullt:

6

-

ampel rotverkehr steht




ampel schaltet


verkehrsfluss wechselts1 s2

s4 s3

33



Modell des Ampel-Verkehrs-Systems, das B, aber nicht A erfullt:

6

-





ampel schaltet



s4 s3

V(t) = s3

34


3. ∀t∃t1∃t2(t ≤ t1 ∧ ampel rot(t1) ∧ t1 ≺ t2 ∧ ampel schaltet(t1, t2)∧ampel gruen(t2))

∀t∃t1∃t2(t ≤ t1 ∧ ampel rot(t1) ∧ ampel schaltet(t1, t2)∧ampel gruen(t2))

In der Pradikatenlogik fur Transitionssysteme sind beide Formeln aquivalent.

Beweis: t1 ≺ t2 ∧ ampel schaltet(t1, t2) und ampel schaltet(t1, t2) sindaquivalent, und in der Pradikatenlogik erhalt die Ersetzung von aquivalentenTeilformeln die Aquivalenz.

35

28Die Bedeutung der Sprache FOL

Eigenschaften und Rolle der Sprache FOL

• relativ ausdrucksstarke Modellierungs- und Spezifikationssprache

• dafur hohe Komplexitat der Verifikation

• geeignet als Vergleichsbasis fur die i.A. ausdrucksschwacheren temporalenLogiken

• hier auch benutzt zur Veranschaulichung von Modellierungs- und Spezi-fikationsproblemen

36

29Ein nichtdeterministisches Ampel-Verkehrs-Systems

-

?

6







s4 s3

ampel schaltet ampel schaltet


ι(verkehr steht) = s2, s3, ι(verkehr fliesst) = s1, s4,ι(ampel schaltet) = 〈s2, s3〉, 〈s4, s1〉,ι(verkehrsfluss wechselt) = 〈s1, s2〉, 〈s3, s4〉

37

29Ein nichtdeterministisches Ampel-Verkehrs-Systems

-

?

6 6

?







s4 s3

ampel schaltet ampel schaltet


ι(verkehr steht) = s2, s3, ι(verkehr fliesst) = s1, s4,ι(ampel schaltet) = 〈s2, s3〉, 〈s4, s1〉, 〈s3, s2〉, 〈s1, s4〉,ι(verkehrsfluss wechselt) = 〈s1, s2〉, 〈s3, s4〉

38

30Dynamik von Transitionssystemen

Darstellung deterministischen Verhaltens

Das zeitliche Verhalten eines deterministischen Transitionssystems mit einemAnfangszustand lasst sich als Funktion w : N −→ U darstellen, wobeiN = N oder ein endliches Anfangsstuck von N.

Dynamik deterministischer Ampel-Verkehrs-Systeme:

• Ursprungliches System mit Anfangszustand s1:

s3

s4

s1

s2- -- -

s3

s4

s1

s2- -- -

• System von S. 27 (unten) mit Anfangszustand s3:

s3

s1- -

-

s4 s2

39

31Dynamik nichtdeterministischer Transitionssysteme

Darstellung nichtdeterministischen Verhaltens

• Das zeitliche Verhalten eines beliebigen (nichtdeterministischen) Tran-sitionssystems mit einem Anfangszustand lasst sich als mit Zustandenmarkierter (u.U. unendlicher) Baum darstellen.

• Der Berechnungsbaum entsteht durch Auffalten des Transitionsgraphen.

• Intendierte Systemeigenschaften konnen Zustande oder ganze Pfade einesBerechnungsbaumes betreffen, z.B.:

1. Es ist (vom Anfangszustand aus) ein Zustand erreichbar, in dem dieAmpel grun ist und der Verkehr fliesst.

2. Von jedem erreichbaren Zustand, in dem die Ampel rot ist, ist einZustand erreichbar, in dem die Ampel grun ist.

3. Es gibt einen Pfad, auf dem die Ampel immer grun ist bis sie rot ist.4. Auf jedem Pfad kommt unendlich oft ein Zustand vor, in dem die

Ampel grun ist (der Verkehr fliesst).

40


Dynamik des nichtdeterministischen Ampel-Verkehrs-Systems von S. 38(unten) mit Anfangszustand s1:

s4

s1

s2

s1

s2

s4

s3

s4

s2

s1

s2

s3

s4

HHHHHj

HHHHHj

*

*

HHHHHj

*

*

HHHHHj

-

-

-

-

6

?

?

6

-

Transitionsgraph Berechnungsbaum

Welche der Eigenschaften erfullt das System?

41



s4

s1

s2

s1

s2

s4

s3

s4

s2

s1

s2

s3

s4

HHHHHj

HHHHHj

*

*

HHHHHj

*

*

HHHHHj

-

-

-

-

6

?

?

6

-


1. Es ist (vom Anfangszustand aus) ein Zustand erreichbar, in dem dieAmpel grun ist und der Verkehr fliesst.

42



s4

s1

s2

s1

s2

s4

s3

s4

s2

s1

s2

s3

s4

HHHHHj

HHHHHj

*

*

HHHHHj

*

*

HHHHHj

-

-

-

-

6

?

?

6

-


2. Von jedem erreichbaren Zustand, in dem die Ampel rot ist, ist ein Zustanderreichbar, in dem die Ampel grun ist.

43



s4

s1

s2

s1

s2

s4

s3

s4

s2

s1

s2

s3

s4

HHHHHj

HHHHHj

*

*

HHHHHj

*

*

HHHHHj

-

-

-

-

6

?

?

6

-


3. Es gibt einen Pfad, auf dem die Ampel immer grun ist bis sie rot ist. gibteinen Pfad, auf dem die Ampel immer grun ist bis si

44



s4

s1

s2

s1

s2

s4

s3

s4

s2

s1

s2

s3

s4

HHHHHj

HHHHHj

*

*

HHHHHj

*

*

HHHHHj

-

-

-

-

6

?

?

6

-


4a. Auf jedem Pfad kommt unendlich oft ein Zustand vor, in dem die Ampelgrun ist.

45



s4

s1

s2

s1

s2

s4

s3

s4

s2

s1

s2

s3

s4

HHHHHj

HHHHHj

*

*

HHHHHj

*

*

HHHHHj

-

-

-

-

6

?

?

6

-


4b. Auf jedem Pfad kommt unendlich oft ein Zustand vor, in dem derVerkehr fliesst.

46

33Modellierung asynchroner Systeme

• Asynchrone Systeme: Systeme aus Komponenten, die unabhangig von-einander Zustandsanderungen bewirken konnen

• Modellierungsparadigma Interleaving-Semantik: Zu jeder Zeit andert sichgenau eine Komponente

Beispiel: Jede Komponente ist im 0 oder 1-Zustand. Jede Komponentekann den Zustand der anderen um den eigenen Wert erhohen (+) odervermindern (−) modulo 2.

AAAAU

AAAAAAK

-

k2k1

k3

++−

−

+−

47

34Kombinatorisches Grundproblem des Model Checking

Explosion des Zustandsraumes

• Transitionsgraph bzw. Modell simuliert nicht direkt die Komponentenund Interaktionen des modellierten Systems, sondern die gesamten Sy-stemzustande und deren Anderung

• Hinzufugung von Komponenten lasst Zustandsraum explodieren

-

k2k1 +−

-

k2k1 +−

AAAAU

AAAAAAK

-?

66

?

k3

++−

−

k4 k3

−

+

−+ +−

48

35Tableaus fur die Logik FOL

• Sei 〈I,V〉 ein Modell mit Universum U = t1, . . . , tn und F eine Formelder Pradikatenlogik fur Transitionssysteme

• Bearbeite einen mit Erfulltheitsproblemen markierten Baum

• Markiere Wurzel des Baumes mit dem Problem 〈I,V〉 |= A

• Je nach dominierendem logischem Symbol, dem Typ der Formel (→ oder∃), und der Beziehung (|= oder 6|=) expandiere den Baum rekursiv nachden folgenden Auswertungs- bzw. Dekompositionsregeln

• Propagiere die Werte zur Wurzel zuruck

• Arbeite den Baum im Tiefenverfahren durch (Backtracking)

49

36Tableau-Regeln fur die Logik FOL

Regel fur quantorenfreie Formeln

Falls die Formel keine Quantoren enthalt, prufe aussagenlogisch, ob dasmomentane Modell die Formel erfullt oder nicht

Regeln fur das Konnektiv

Positive →-Regel:

〈I,V〉 |= (A→ B)〈I,V〉 6|= A oder 〈I,V〉 |= B

gdw

Negative →-Regel:

〈I,V〉 6|= (A→ B)〈I,V〉 |= A und 〈I,V〉 6|= B

gdw

50

37Tableau-Regeln fur die Logik FOL

Regeln fur den Quantor

Positive ∃-Regel:

〈I,V[t/s1]〉 |= ∃tA〈I,V[t/s1]〉 |= A oder · · · oder 〈I,V[t/sn]〉 |= A

gdw

Negative ∃-Regel:

〈I,V[t/s1]〉 6|= ∃tA〈I,V[t/s1]〉 6|= A und · · · und 〈I,V[t/sn]〉 6|= A

gdw

• dabei bezeichne V[t/s] := (V \ 〈t,V(t)〉) ∪ 〈t, s〉), d.h. die Modifi-kation der Variablenzuweisung V, die t auf den Zustand s abbildet

51

38Komplexitat des Model Checking fur FOL

Worst-Case Abschatzung fur das Tableauverfahren

• Maximale Tiefe des Tableaus = quantorielle Tiefe q der Formel F , d.h.maximale logische Schachtelungstiefe eines Quantors in F : q < |F |

• Maximale Anzahl der Blatter des Tableaus: O(max(|U |, 2)q

• Zeitbedarf fur Auswertung der Blattprobleme: jeweils linear in |IV|+ |F |

• Zeitbedarf fur Dekomposition und Ruckgabe: jeweils linear in max(|U |, 2)

• Platzbedarf: |IV|+ |F |

Komplexitat des Modell-Erfullungsproblems fur FOL:

• Allgemeines Problem ist PSPACE-vollstandig,

• fur Formeln mit begrenzter quantorieller Tiefe in P (polynomiell)

52

39Optimierungen von Tableauverfahren

• Partielle Evaluierung

• Heuristische Selektion der Unterprobleme

• Lemmas und Schnitte

• Intelligentes Backtracking

53

40Modale und temporale Aussagenlogik

• Keine explizite Verwendung von Zustandsvariablen t

• Elementaraussagen nullstellig wie in der Aussagenlogik:stack is empty bedeutet: der Keller ist jetzt leer.

• Feste Einbettung der Transitionsrelation(en) in die Logik durch neue lo-gische Konnektive, z.B. (notwendig), ♦ (moglich) oder die temporalenX (neXt), F (Future), G (Globally, always), U (Until)

• (Temporale) Lesart modaler bzw. temporaler Formeln:

♦ stack is empty oder X stack is empty bedeutet: es gibt einen un-mittelbaren Folgezustand, in dem der Keller leer ist.

stack is empty: Keller ist in jedem unmittelbaren Folgezustand leer.

F stack is empty: es gibt erreichbaren Zustand, in dem Keller leer ist.

G stack is empty: Keller ist in jedem erreichbaren Zustand leer.

stack1 is emptyU stack2 is empty: es gibt erreichbaren Zustand, indem Keller 2 leer ist und Keller 1 ist in allen Zwischenzustanden leer.

54

41Modale Aussagenlogik

Syntax der modalen Aussagenlogik


• Die (Formeln der) modalen Aussagenlogik fur P sei(en) definiert durch:

ML(P) := P | ⊥ | (ML→ML) | ♦ML

• Andere aussagenlogische Konnektive wie ublich als Abkurzungen definiertsowie A := ¬♦¬A• Prazedenz der Operatoren: ¬,♦,,∧,∨,→,↔.

55


Semantik der modalen Aussagenlogik

• Pioniere: Kripke, Kanger, Hintikka

• (Kripke-)Rahmen: Paar 〈U ,≺〉 wobei

– U nichtleere Menge (moglicher Welten) und– ≺⊆ U × U , die Ubergangsrelation

• (Kripke-)Struktur I fur eine modale Aussagenlogik ML(P):Tripel 〈U ,≺, ι〉 wobei

– 〈U ,≺〉 ein Rahmen und– ι eine Funktion P −→ 2U ,

d.h. eine Belegung wie in der Pradikatenlogik fur Transitionssysteme

• (Kripke-)Modell Is fur ML(P): Quadrupel 〈U ,≺, ι, s〉 wobei

– 〈U ,≺, ι, s〉 eine Struktur fur P und– s ∈ U , der Referenzpunkt

56

44Systemmodellierung mittels Modallogik

Ein Kripke-Rahmen 〈U ,≺〉:U = s1, s2, s3, s4,≺ = 〈s1, s2〉, 〈s1, s3〉, 〈s1, s4〉,

〈s2, s3〉, 〈s2, s4〉, 〈s3, s4〉

s2

s1

s4

s3

3

QQQQQs

QQQQQs

3

?

-

Eine Kripke-Struktur I furP = stack1 is empty︸︷︷︸

e1

, stack2 is empty︸︷︷︸e2


:

Rahmen wie oben sowie ι(e1) = s2, s3, s4, ι(e2) = s3, s4, ι(e3) = s4

Dann gelten z.B.:Is1 |= ♦¬e2, aber Is2 6|= ♦¬e2;Is1 |= ♦¬e2 ∧ ♦¬e3, aber Is1 6|= ♦ (¬e3 ∧ ♦¬e3)Is1 |= ♦♦ (e1 ∧ e2 ∧ e3);Is4 |= ⊥

58

45Modallogik vs. Pradikatenlogik

Ausdrucksstarke der (aussagenlogischen) Modallogik

• Formel der Pradikatenlogik fur Transitionssysteme FOL:stack is empty(t0)→ ∃t1(put(t0, t1) ∧ ¬stack is empty(t1))

entspricht in Modallogik ML (unter Unterschlagung des Transitionstyps):stack is empty → ♦¬stack is empty

• Zur Modellierung von Transitionstypen Erweiterung der Modallogik zurMultimodallogik

• FOL-Formel:∀t1((t0 ≤ t1 ∧ request(t1))→ ∃t2(t1 < t2 ∧ acknowledge(t2)))

hat keine naturliche Entsprechung in Modallogik ML

• ⇒ Erweiterung der Modallogik um ausdrucksstarkere Operatoren

59

46Multimodale Aussagenlogik

Syntax der multimodalen Aussagenlogik

• Gegeben eine Menge P von Aussagenvariablen und eine Menge R vonUbergangsvariablen

• Die (Formeln der) multimodalen Aussagenlogik fur P und R sei(en)definiert durch:

ML(P,R) := P | ⊥ | (ML→ML) | 〈R〉ML

• Andere aussagenlogische Konnektive wie ublich als Abkurzungen definiertsowie [R]A := ¬ 〈R〉¬A

• Prazedenz der Operatoren: ¬, 〈R〉, [R],∧,∨,→,↔

60


Semantik der multimodalen Aussagenlogik

• (Kripke-)Rahmen fur eine multimodale Aussagenlogik MML(P,R):Paar 〈U , ρ〉 wobei

– U nichtleere Menge (moglicher Welten) und– ρ : R −→ 2U×U , die Ubergangsbelegung

• (Kripke-)Struktur I fur MML(P,R): Tripel 〈U , ρ, ι〉 wobei

– 〈U , ρ〉 ein Rahmen und– ι eine Funktion P −→ 2U ,

d.h. eine Belegung wie in der modalen Aussagenlogik

• (Kripke-)Modell Is fur MLL(P,R): Quadrupel 〈U , ρ, ι, s〉 wobei

– 〈U , ρ, ι, s〉 eine Struktur fur MLL(P,R) und– s ∈ U , der Referenzpunkt

61

49Systemmodellierung mittels Modallogik

Ein Kripke-Rahmen 〈U ,≺〉:U = s1, s2, s3, s4,≺ = 〈s1, s2〉, 〈s1, s3〉, 〈s1, s4〉,

〈s2, s3〉, 〈s2, s4〉, 〈s3, s4〉

s2

s1

s4

s3

3

QQQQQs

QQQQQs

3

?

-

Eine Kripke-Struktur I furP = stack1 is empty︸︷︷︸

e1



:

Rahmen wie oben sowie ι(e1) = s2, s3, s4, ι(e2) = s3, s4, ι(e3) = s4

Dann gelten z.B.:Is1 |= ♦¬e2, aber Is2 6|= ♦¬e2;Is1 |= ♦¬e2 ∧ ♦¬e3, aber Is1 6|= ♦ (¬e3 ∧ ♦¬e3)Is1 |= ♦♦ (e1 ∧ e2 ∧ e3);Is4 |= ⊥

63

50Multimodallogik vs. Pradikatenlogik

Ausdrucksstarke der (aussagenlogischen) Multimodallogik

• Formel der Pradikatenlogik fur Transitionssysteme FOL:stack is empty(t0)→ ∃t1(put(t0, t1) ∧ ¬stack is empty(t1))

entspricht in Multimodallogik MML:stack is empty → 〈put〉 ¬stack is empty

• FOL-Formel:∀t1((t0 ≤ t1 ∧ request(t1))→ ∃t2(t1 < t2 ∧ acknowledge(t2)))

hat keine naturliche Entsprechung in Multimodallogik MML

• ⇒ Erweiterung der Multimodallogik um ausdrucksstarkere Operatoren

64

51Verallgemeinerung der Modallogik

Semantik der verallgemeinerten Modallogik

• Semantik wie in der Modallogik mit folgenden Modifikationen bei derErfulltheit von Formeln:

• Is |= XA gdw es ein s′ ∈ U gibt mit s ≺ s′ und Is′ |= A,

• Is |= F+A gdw es ein s′ ∈ U gibt mit s < s′ und Is′ |= A,

• Is |= F∗A gdw es ein s′ ∈ U gibt mit s ≤ s′ und Is′ |= A

• Dabei sei < die transitive Hulle von ≺, die Erreichbarkeitsrelation

Weitere Operatoren als Abkurzungen definiert

• XA := ¬X¬A entspricht A

• G+A := ¬F+¬A• G∗A := ¬F∗¬A

65

52Ausdrucksstarke generalisierter Modallogiken

Generalisierte Modallogik vs. Pradikatenlogik

• Formel der Pradikatenlogik fur Transitionssysteme FOL:∀t1((t0 ≤ t1 ∧ request(t1))→ ∃t2(t1 < t2 ∧ acknowledge(t2)))

entspricht in der verallgemeinerten Modallogik EML mit OperatormengeO = X,F+,F∗:G∗ (request→ F

+ acknowledge) (man beachte, dass (G∗ := ¬F∗¬)

Relative Ausdrucksstarke zwischen generalisierten Modallogiken

• Der Operator F∗ ist redundant in der generalisierten Modallogik EMLmit O = X,F+,F∗, denn F∗A ist aquivalent zu A ∨ F+A

• Der Operator F+ ist ebenfalls redundant in dieser Logik, denn F+A istaquivalent zu XF∗A

• F∗ kann in jeder generalisierten Modallogik durch F+ definiert werden,aber nicht umgekehrt.

66


Definition relativer Ausdrucksstarke: Gegeben zwei generalisierte Modal-logiken EML1 und EML2 (mit gemeinsamem P): EML2 ist so ausdrucks-stark wie EML1, wenn es zu jeder Formel A1 in EML1 eine aquivalenteFormel A2 in EML2 gibt.

Satz: Die Logik L1 := EML mit O = F∗ ist nicht so ausdrucksstark wieL2 := EML mit O = F+.

Beweis: Wir zeigen, dass es zur Formel F+> (> := p→ p) keine aquivalenteFormel in L1 gibt. Betrachte dazu zwei Kripke-ModelleM1 = 〈s,≺1, ι, s〉und M2 = 〈s,≺2, ι, s〉 mit ≺1= ∅, ≺2= 〈s, s〉.Es gilt: M1 6|= F

+> und M2 |= F+>.

Man zeigt nun (durch Induktion uber den Formelaufbau) fur alle L1-FormelnA, dass M1 |= A gdw M2 |= A.

67


Ausdrucksstarke generalisierter Modallogiken vs. Pradikatenlogik

• Formel der Pradikatenlogik fur Transitionssysteme FOL:∀t1((t0 ≤ t1 ∧ request(t1))→ ∃t2(t1 < t2 ∧ acknowledge(t2))∧

∀t3((t1 < t3 ∧ t3 < t2)→ request(t3))))(keine Anfrage wird geloscht, bevor sie beantwortet ist)

kann in keiner generalisierten Modallogik ausgedruckt werden, da inletzterer keine Aussagen uber Intervalle moglich sind.

Temporallogik im engeren Sinne

• Einfuhrung nichtmodaler 2-stelliger (Intervall-)Operatoren wie U (Until)

• stack1 is emptyU stack2 is empty bedeutet:Es gibt einen erreichbaren Zustand, in dem Keller 2 leer ist und Keller 1ist in allen Zwischenzustanden leer.

68

55Lineare Temporale Logik

Syntax der linearen temporalen Logik


• Die (Formeln der) linearen temporalen Logik fur P sei(en) definiert durch:

LTL(P) := P | ⊥ | (LTL→ LTL) | (LTL U+ LTL) |(LTL U− LTL)

• Andere aussagenlogische Konnektive wie ublich sowie UnlessAW+B := ¬(¬BU+¬(A ∨B))

• Prazedenz der Operatoren: ¬,∧,∨,→,↔,U

• LTL ermoglicht die Formulierung von Intervallaussagen

69


Semantik der linearen temporalen Logik

• Semantik wie in der Modallogik mit folgenden Modifikationen bei derErfulltheit von Formeln:

• Is |= AU+B gdw es ein s′ ∈ U gibt mit s < s′ und Is′ |= B und

fur alle s′′ ∈ U mit s < s′′ < s′ gilt: Is′′ |= A

• Is |= AU−B gdw es ein s′ ∈ U gibt mit s′ < s und Is′ |= B und

fur alle s′′ ∈ U mit s′ < s′′ < s gilt: Is′′ |= A

Naturliche Modelle

Ein Modell 〈U,≺, ι, s〉 heisst naturlich wenn < eine lineare Ordnung mitkleinstem Element s ist.

70


Ausdrucksstarke von LTL

• Operatoren der generalisierten Modallogik konnen durch U+ ausgedrucktwerden:

• XA ≡ (aquivalent) (⊥U+A)

• F+A ≡ (>U+A)

• U− ermoglicht Vergangenheitsbezuge auszudrucken

• Formel der Pradikatenlogik fur Transitionssysteme FOL:∀t1((t0 ≤ t1 ∧ request(t1))→ ∃t2(t1 < t2 ∧ acknowledge(t2))∧

∀t3((t1 < t3 ∧ t3 < t2)→ request(t3))))(keine Anfrage wird geloscht, bevor sie beantwortet ist)

entspricht in LTL: G∗(request→ (requestU+ acknowledge))

71

58Relative Ausdrucksstarke von FOL

• Multimodallogiken, generalisierte aussagenlogische Modallogiken sowiedie temporale Logik LTL konnen als Fragmente der Pradikatenlogik furTransitionssysteme angesehen werden

• Es genugen FOL-Formeln mit hochstens einer freien Variable

• Bei nichtparametrisierten Operatoren reicht weiterhin die Beschrankungauf FOL-Formeln mit einem Transitionspradikat ≺

Aquivalenzsatz: Fur jede Formel A aus LTL oder einer generalisiertenModallogik gibt es eine FOL-Formel A′ mit hochstens einer freien Variablent und einem Transitionspradikat ≺ derart, dass fur jedes Kripke-Modell〈U ,

.≺, ι, s〉 und jede Variablenbelegung V mit V(t) = s gilt:

〈U ,.≺, ι, s〉 |= A gdw 〈U , ι,V〉 |= A′

wobei ι(≺) =.≺.

72

59Relative Ausdrucksstarke von FOL

Sog. Standardubersetzung F von Formeln der generalisierten Modal-logik und der linearen temporalen Logik LTL in FOL

• F(p) := p(t) fur alle atomaren Formeln

• F(⊥) := ⊥• F((A→ B)) := (F(A)→ F(B))

• F(XA) := ∃t′(t ≺ t′ ∧ F(A)[t/t′])

• F(F+A) := ∃t′(t < t′ ∧ F(A)[t/t′])

• F(F∗A) := ∃t′(t ≤ t′ ∧ F(A)[t/t′])

• F(AU+B) := ∃t′(t < t′ ∧ F(B)[t/t′] ∧ ∀t′′(t < t′′ < t′ → F(A)[t/t′′]))

• F(AU−B) := ∃t′(t′ < t ∧ F(B)[t/t′] ∧ ∀t′′(t′ < t′′ < t→ F(A)[t/t′′]))

t′, t′′ seien Variablen, die nicht in der jeweiligen Formel vorkommen

73

60Standardubersetzung in FOL

Beispiele fur die Standardubersetzung

F(((¬ackU− req)U+ack)) =

∃t1(t < t1 ∧ ack(t1) ∧ ∀t2(t < t2 < t1 → F((¬ackU− req))[t/t2])) =

∃t1(t < t1 ∧ ack(t1) ∧ ∀t2(t < t2 < t1 →∃t3(t3 < t2 ∧ req(t3) ∧ ∀t4(t3 < t4 < t2 → ¬ack(t4)))))

F(G∗(req → F∗ack)) =

F(¬F∗¬(req → F∗ack)) ≡

∀t1(t ≤ t1 ∧ req(t1)→ F(F∗ack)[t/t1]) =

∀t1(t ≤ t1 ∧ req(t1)→ ∃t2(t1 ≤ t2 ∧ ack(t2)))

74

61Ubersetzung von Multimodallogiken in FOL

Ubersetzung von Multimodallogiken in FOL ist moglich

Erweiterung der Standardubersetzung F um die Regel

F(〈R〉A) := ∃t′(R(t, t′) ∧ F(A)[t/t′])

Aquivalenzsatz fur Multimodallogiken:

Fur jede Formel A aus einer Multimodallogik gibt es eine FOL-Formel A′

mit hochstens einer freien Variablen t derart, dass fur jedes Kripke-Modell〈U , ρ, ι, s〉 und jede Variablenbelegung V mit V(t) = s gilt:

〈U , ρ, ι, s〉 |= A gdw 〈U , ρ ∪ ι,V〉 |= A′ .

75


Weitere Einschrankungen von FOL sind moglich

Verscharfung der Aquivalenzsatze

• Fur LTL- Formeln: es gibt aquivalente FOL-Formeln mit hochstens dreiverschiedenen Variablen

• Fur Formeln der Modallogik: es gibt aquivalente FOL-Formeln mithochstens zwei verschiedenen Variablen (guarded fragment der Pradika-tenlogik)

Konsequenzen

• Bestimmte 2-stellige Operatoren wie U konnen nicht in der Modallogikausgedruckt werden

• FOL-Eigenschaften, die mehr als 3 Variablen wesentlich benotigen,konnen nicht in LTL (temporaler Logik) ausgedruckt werden

76


Einsparung durch Wiederverwendung von Variablen

Beispiele

F(((¬ackU− req)U+ack)) =

∃t1(t < t1 ∧ ack(t1) ∧ ∀t2(t < t2 < t1 →∃t3(t3 < t2 ∧ req(t3) ∧ ∀t4(t3 < t4 < t2 → ¬ack(t4))))) ≡

∃t1(t < t1 ∧ ack(t1) ∧ ∀t2(t < t2 < t1 →∃t(t < t2 ∧ req(t) ∧ ∀t1(t < t1 < t2 → ¬ack(t1)))))

F(G∗(req → F∗ack)) ≡

∀t1(t ≤ t1 ∧ req(t1)→ ∃t2(t1 ≤ t2 ∧ ack(t2))) ≡

∀t1(t ≤ t1 ∧ req(t1)→ ∃t(t1 ≤ t ∧ ack(t)))

77

64Ausdrucksgrenzen der temporalen Aussagenlogik

Eine Eigenschaft mit inharent vier verschiedenen Variablen:

”Vom Startzustand aus sind drei verschiedene Zustande erreichbar, die

untereinander verbunden sind“:

∃t1∃t2∃t3(t < t1 ∧ t < t2 ∧ t < t3 ∧ t1 < t2 ∧ t1 < t3 ∧ t2 < t3)

Ein Kripke-Rahmen 〈U ,≺〉, der die Formel erfullt (d.h. dessen samtlicheModelle die Formel erfullen):

U = s1, s2, s3, s4≺ = 〈s1, s2〉, 〈s1, s3〉, 〈s1, s4〉,

〈s2, s3〉, 〈s2, s4〉, 〈s3, s4〉

s2

s1

s4

s3

3

QQQQQs

QQQQQs

3

?

-

Es gibt keine aquivalente FOL-Formel mit weniger als vier verschie-denen Variablen.

78

65Einschrankungen an Rahmen und Modelle

Naturliche Modelle: Ein Kripke-Modell 〈U ,≺, ι, s〉 gdw < eine lineareOrdnung mit kleinstem Element s ist, d.h. dessen Rahmen 〈U ,≺〉 isomorphist zu den naturlichen Zahlen bzw. einem Anfangsstuck der naturlichenZahlen 0, 1, 2, 3, . . . und der Nachfolgerfunktion wobei s der 0 entspricht.

Falls man sich auf naturliche Modelle beschrankt, lasst sich die FOL-Formelausdrucken durch:

∃t1(t < t1 ∧ ∃t2(t1 < t2 ∧ ∃t3(t2 < t3))) ≡

∃t1(t < t1 ∧ ∃t(t1 < t ∧ ∃t1(t < t1)))

das aquivalent ist zu einer generalisierten Modallogik-Formel: F+F

+F

+>

79

66Relative Ausdrucksstarke von LTL

Satz: LTL ist fur naturliche Modelle so ausdrucksstark wie FOL mit einerfreien Variablen und einem Transitionspradikat.

Original-Beweis von Kamp [1968] sehr kompliziert, vereinfachter Beweis vonGabbay [1989] benutzt Separierungseigenschaft

Eine temporallogische bzw. LTL-Formel heisst:

• zukunftsbezogen gdw wenn sie den Operator U− nicht enthalt,

• vergangenheitsbezogen gdw wenn sie den Operator U+ nicht enthalt,

• separiert gdw wenn sie eine junktorenlogische Kombination zukunfts-oder vergangenheitsbezogener Formeln ist.

Eine Logik hat die Separierungseigenschaft (fur eine Klasse K von Modellen)gdw fur jede Formel der Logik eine (bzgl. aller Modelle in K) aquivalenteseparierte Formel der Logik existiert.

80

67Relative Ausdrucksstarke von LTL

Hilfssatz: LTL hat die Separierungseigenschaft fur naturliche Modelle.

Zentrale Idee des Beweises: Fur alle naturlichen Modelle M gilt z.B.:

M |= F+(A ∧G−B)↔ G

−B ∧B ∧ (BU+A)

Beobachtung: Die Separierungs-Transformation kann zu einer nichtelemen-taren Verlangerung der Formel fuhren.

Hilfssatz: Falls eine temporale Logik die Separierungseigenschaft fur eineKlasse von Modellen K hat, dann ist sie so ausdrucksstark wie FOL miteiner freien Variablen und einem Transitionspradikat.

Satz: Es gibt eine Folge von FOL-Formeln derart, dass die Lange derentsprechenden kurzesten aquivalenten LTL-Formeln nicht durch eine ele-mentare Funktion der Lange der FOL-Formeln beschrankt werden kann.D.h. obwohl LTL auf naturlichen Modellen dieselbe Ausdruckskraft wieFOL hat, hat es nicht dieselbe Ausdruckskurze oder -bundigkeit.

81

68Berechnungsbaume und Pfade

Formulierung von Systemeigenschaften hoherer Ordnung

• Eigenschaften von Ablaufen (d.h. Ausfuhrungsfolgen) eines(nichtdeterministischen) Computerprogramms oder Systems

• Modellierung aller Ablaufe als Berechnungsbaum

6

? @@

@@I

-

s3s2

s1

p

82

69Berechnungsbaume und Pfade

• Insbesondere interessant: Aussagen uber bestimmte Pfade im Berech-nungsbaum eines Systems

• Gegeben (die Ubergangsrelation) ein(es) Transitionssystem(s), d.h. einKripke-Rahmen 〈U ,≺〉

• Pfad π in einem Kripke-Rahmen 〈U ,≺〉 oder einer Kripke-Struktur〈U ,≺, ι〉: endliche oder unendliche Folge von Zustanden s0, s1, s2, . . .wobei jeweils si ≺ si+1

(Folge: Funktion N −→ S mit N ⊆ N und 0 < i ∈ N ⇒ i− 1 ∈ N)

• s-Pfad: Pfad π mit π(0) = s

• Maximaler Pfad π : N −→ U : fur alle i ∈ N gilt: wenn es ein s ∈ U gibtmit π(i) ≺ s, dann ist i+ 1 ∈ N (d.h. ein maximaler Pfad ist entwederunendlich oder sein letzter Zustand ist ein Endpunkt in ≺)

• Pfad in einem Kripke-Modell 〈U ,≺, ι, s〉: s-Pfad in 〈U ,≺〉.

83

70Berechnungsbaum-Logik (Computation Tree Logic)

Syntax der Berechnungsbaum-Logik


• Die (Formeln der) Berechnungsbaum-Logik (Computation Tree Logic)fur P sei(en) definiert durch:

CTL(P) := P | ⊥ | (CTL→ CTL) | E(CTL U+ CTL) |A(CTL U+ CTL)

• CTL ermoglicht die Formulierung von Aussagen uber alle maximalenBerechnungspfade

• CTL wird normalerweise auf Baummodellen interpretiert, d.h. Modellen,bei denen die transitive Hulle < der Transitionsrelation ≺ eine partielleOrdnung mit einem kleinsten Element ist

84


Semantik der Berechnungsbaum-Logik

• Semantik wie in der Modallogik, d.h. eine Struktur ist ein Triple I =〈U ≺, ι〉 und ein Modell ist ein Paar 〈I, s〉 mit s ∈ U

• Definition der Erfulltheit von neuen CTL-Formeln:

• Is |= E(AU+B) gdw es ein s′ ∈ U gibt mit s < s′ und Is′ |= B und

fur alle s′′ ∈ U mit s < s′′ < s′ gilt: Is′′ |= A

• entspricht genau der Semantik von (AU+B)

• Is |= A(AU+B) gdw wenn alle maximalen Pfade π, die in s beginnen,

ein s′ enthalten mit s < s′ und Is′ |= B und fur

alle s′′ mit s < s′′ < s′ gilt: Is′′ |= A

85


Weitere als Abkurzungen definierte Operatoren

EXB := E(⊥U+B) AXB := A(⊥U+B)EXB := ¬AX¬B AXB := ¬EX¬B

EF+B := E(>U+B) AF

+B := A(>U+B)∃s′ > s : Is

′|=t B ∀ max. Pfade π : ∃s′ > s auf π : Is

′|=t B

EG+B := ¬AF+¬B AG

+B := ¬EF+¬B∃ max. Pfad π : ∀s′ > s auf π : Is

′|=t B ∀s′ > s : Is

′|=t B

E(AU∗B) := (B ∨A ∧ E(AU+B)) A(AU∗B) := (B ∨A ∧ A(AU+B))EF∗B := (B ∨ EF+B) AF

∗B := (B ∨ AF+B)EG∗B := (B ∧ EG+B) AG

∗B := (B ∧ AG+B)

E(AW+B) := ¬A(¬BU+¬(A ∨B))A(AW+B) := ¬E(¬BU+¬(A ∨B))

86


Wichtige Zusammenhange zwischen den Operatoren

A(AU+B) ≡ A(AW+B) ∧ AF+B = ¬E(¬BU+¬(A ∨B)) ∧ AF+B

A(AU+B) ≡ ¬E(¬BU+¬(A ∧B)) ∧ ¬EG+¬B

⇒ EU+ und AF+ reichen als Basis-Operatoren aus und

EU+ und AG+ reichen als Basis-Operatoren aus

(gunstig fur formale Beweise und Algorithmen)

E(AW+B) ≡ E(AU+B) ∨ EG+B

Aber keine negationsfreie duale Charakterisierung von AW+ und EU+

87

74Beispiele von CTL-Spezifikationsformeln

Typische Korrektheitseigenschaften eines reaktiven Systems

Es ist ein Zustand erreichbar, in dem started gilt, aber ready nicht:

EF+(started ∧ ¬ready)

Jede Anfrage wird irgendwann beantwortet:

AG∗(request→ AF

+acknowledge)

Auf jedem Ast des Berechnungsbaums ist der Stack unendlich oft leer:

AG∗AF

+stack is empty

Von jedem Zustand s aus ist ein restart-Zustand erreichbar oder s ist selbstein restart-Zustand:

AG∗EF∗restart

88

75Vergleich der Ausdrucksstarke von CTL und LTL

• Beschrankung auf zukunftsbezogenes Fragment der LTL

• Direkter Vergleich schwierig, da intendierte Modelle unterschiedlich

• Auf naturlichen Modellen (Baumen mit Verzweigungsgrad 1) sind EU+

und AU+ gleichbedeutend

• Auf echten Baummodellen ist AU+ nicht in LTL ausdruckbar

• Deshalb: Vergleich auf von allgemeinen Kripke-Modellen generiertennaturlichen bzw. Baummodellen

89

76Generierte spezielle Modelle

Generierte naturliche ModelleGegeben ein beliebiges Kripke-Modell M = 〈U ,≺, ι, s〉. Ein Modell M′ =〈U ′,≺′, ι′, s′〉 heisst ein direkt von M generiertes naturliches Modell gdw

• U ′ ein maximaler Pfad π : N −→ U in M ist mit π(0) = s,

• ≺′:= 〈〈i, π(i)〉, 〈i+ 1, π(i+ 1)〉〉 : 0 < i+ 1 ∈ N,• ι′(p) = 〈i, s〉 ∈ U : s ∈ ι(p),• s′ = 〈0, s〉.

Folgen-Gultigkeit bzw. -ErfulltheitEine LTL-Formel A heisst Folgen-gultig in (oder Folgen-erfullt von) einemKripke-Modell M, geschrieben M |=s A, gdw A von allen direkt von Mgenerierten naturlichen Modellen erfullt wird.

90

77Generierte spezielle Modelle

Generierte Baum-ModelleGegeben ein beliebiges Kripke-Modell M = 〈U ,≺, ι, s〉.

• Sei 〈K,≺′〉 der von M erzeugte Berechnungsbaum (K Knotenmenge,≺′⊆ K ×K Kantenmenge),

• ` die Knotenmarkierungsfunktion K −→ U , d.h. k ≺′ k′ gdw `(k) ≺`(k′);

• weiterhin sei ι′(p) = k ∈ K : `(k) ∈ ι(p),• und k die Wurzel von K.

Dann ist das Modell M′ = 〈K,≺′, ι′, k〉 das direkt von M generierteBaummodell.

Baum-Gultigkeit bzw. -ErfulltheitEine CTL-Formel A heisst Baum-gultig in (oder Baum-erfullt von) einemKripke-Modell M, geschrieben M |=t A, gdw A vom von M generiertenBaummodell erfullt wird.

91

78Vergleich der Ausdrucksstarke von CTL und LTL

Vergleich der relativen Ausdrucksstarke von LTL bzw. CTL uber diegenerierten naturlichen bzw. Baummodelle beliebiger Kripke-Modelle

Satz: Es gibt eine LTL-Formel A, fur die es keine CTL-Formel A′ gibtderart, dass fur jedes Kripke-Modell M gilt: M |=s A gdw M |=t A

′.

Beispiel: A = F+G

+p (ist z.B. s6≡t Q1F+Q2G

+p mit Qi ∈ A,E;unterscheidende Modelle: 〈s, s′, 〈s, s〉, 〈s, s′〉, 〈p, s〉, s bzw.

〈s, s′, 〈s, s〉, 〈s, s′〉, 〈p, s′〉, s)

Satz: Es gibt eine CTL-Formel A, fur die es keine LTL-Formel A′ gibtderart, dass fur jedes Kripke-Modell M gilt: M |=t A gdw M |=s A

′.

Beispiel: A = AG+EF

+p (ist z.B. t6≡s G+F

+p;unterscheidendes Modell: 〈s, s′, 〈s, s〉, 〈s, s′〉, 〈s′, s′〉, 〈p, s′〉, s)

⇒ LTL und CTL haben unterschiedliche Ausdrucksstarke und keine derbeiden Logiken subsumiert die andere

92

79Die volle Berechnungsbaum-Logik CTL∗

Syntax der vollen Berechnungsbaum-Logik CTL∗

• Gegeben eine Menge von aussagenlogischen Variablen P.

• Zwei Typen von Formeln: Zustandsformeln und Pfadformeln definiertdurch simultane Induktion:

1. jede aussagenlogische Variable ∈ P und ⊥ sind Zustandsformeln,2. Wenn B eine Pfadformel ist, dann ist EB eine Zustandsformel,3. jede Zustandsformel ist eine Pfadformel,4. Wenn A und B Pfadformeln sind, dann sind auch (A → B) und

(AU+B) Pfadformeln.

• Die Menge der Formeln der vollen Berechnungsbaum-Logik CTL∗(P)fur P besteht aus allen Zustandsformeln.

• Definierter Operator: AB := ¬E¬B• CTL∗ subsumiert sowohl die CTL als auch das zukunftsbezogene Frag-

ment der LTL.

93


Semantik der vollen Berechnungsbaum-Logik CTL∗

• Semantik basiert auf der Semantik der Modallogik, d.h. eine Struktur istein Triple I = 〈U ≺, ι〉 und ein Modell ist ein Paar 〈I, s〉 mit s ∈ U• Ein Pfadmodell ist ein Paar 〈I, π〉, geschrieben Iπ, wobei π ein maximaler

Pfad in I ist

• Gegeben ein Pfad π mit einer Lange ≥ i, der Suffixpfad πi von π und isei wie folgt definiert: πi(j) = π(i+ j), d.h. πi = 〈j, s〉 : 〈i+ j, s〉 ∈ π.

1. Is |= EB gdw es einen maximalen s-Pfad π in I gibt und Iπ |= B2. Iπ |= p ∈ P gdw Iπ(0) |= p3. Iπ 6|= ⊥4. Iπ |= (A→ B) gdw Iπ 6|= A oder Iπ |= B

5. Iπ |= (AU+B) gdw es ein i > 0 gibt und Iπi |= B und fur alle

0 < j < i gilt: Iπj |= A

94


Beispiele fur CTL∗-Formeln

• Auf jedem maximalen Pfad gibt es einen Zustand, ab dem p immer gilt:

AF∗G∗p

• Disjunktion der kritischen Formeln fur LTL und CTL:

F+G

+p ∨ AG+EF

+p

Ausdrucksstarke der vollen Berechnungsbaum-Logik CTL∗

• CTL∗ subsumiert CTL und zukunftsbezogenes Fragment der LTL.

• Ausdrucksstarke der CTL∗ entspricht Erweiterung der Logik FOL umQuantifikation uber Pfade, der Monadischen Logik zweiter Stufe.

Komplexitat von CTL∗

• Model Checking ist PSPACE-vollstandig.

• Erfullbarkeit ist vollstandig fur doppelt exponentielle Zeit.

95

82Model Checking Probleme

Zwei Typen von Model Checking Problemen

• Standard oder”Initiales“ Model Checking

• Universelles Model Checking

Allgemein gegeben sind (fur Logiken mit einer Transitionsrelation)

• eine beliebige Kripke-Struktur I = 〈U ,≺, ι〉,• eine Formel A in einer Temporallogik L,

• ein Erfulltheitsbegriff |= fur L

Initiales Model Checking:Weiterhin gegeben ein Referenzpunkt s ∈ U , gilt: Is |= A?

Universelles Model Checking: Gilt Is |= A fur alle s ∈ U?

96

83Model Checking Verfahren

Zwei reine Typen von Model Checking VerfahrenTop-down oder lokales vs. bottom-up oder globales Model Checking

Top-down oder lokale Model Checking Verfahren

• Rekursives Losen von Erfulltheitsproblemen der Form Is |= F durchlokale Dekomposition unter Ausnutzung der Struktur I, d.h. Explorationeines Tableaus mit Wurzelmarkierung Is |= A (A initiale Formel)

• I.A. zusatzliche Benutzung dynamischer Programmierungstechniken zurVermeidung der wiederholten Losung gleicher Probleme

Bottom-up oder globale Model Checking VerfahrenF I bezeichne die Menge aller Zustande s ∈ U mit Is |= F .

• Berechnen und speichern aller Mengen F I, wobei F Teilformel von A

• Kompositionelles Vorgehen beginnend bei atomaren Teilformeln

• Abschliessendes Prufen, ob Referenzpunkt s ∈ AI bzw. AI = U

97

84Bottom-up Model Checking fur die Modallogik

Gegeben: Kripke-Struktur I = 〈U ,≺, ι〉 und Formel A der ModallogikML

Universelles bottom-up Model Checking fur die ModallogikFur alle Teilformeln F von A beginnend mit den atomaren Formeln:

• Setze ⊥I := ∅• Falls F atomare Formel p, setze F I := ι(p)

• Falls F = (B → C), setze F I := (U \BI) ∪ CI

• Falls F = ♦B, setze F I := s′ ∈ U : es gibt ein s′′ ∈ BI und s′ ≺ s′′

Effizienz- und Komplexitatsbetrachtungen

• Berechne (♦B)I durch Zuruckverfolgen der Kanten aus BI

• Speichere alle Zwischenwerte F I

• Verfahren quadratisch in (|I|+ |A|)• Effiziente Reprasentation und Operationen auf Mengen erforderlich

98

85Bottom-up Model Checking fur CTL

CTL mit Basis-Operatoren EU+ und EG+

Wir betrachten eine Variante der CTL mit den beiden temporalen Basis-Operatoren EU+ und EG+, die ausreichen um jede CTL-Formel aquivalentauszudrucken, da aus

A(AU+B) ≡ ¬E(¬BU+¬(A ∨B)) ∧ AF+B

und

AF+B ≡ ¬EG+¬B

folgt, dass

A(AU+B) ≡ ¬E(¬BU+¬(A ∨B)) ∧ ¬EG+¬B.

Semantik von EG+

Is |= EG+B gdw es einen maximalen s-Pfad gibt, auf dem fur alle s′ > s

gilt, dass Is′ |= B

99

86CTL-Model Checking

Intendierte Semantik des CTL-Model Checking

• Eigenschaften beliebiger Transitionssysteme sollen modelliert werden

• Welche Semantik, Standard-Semantik (|=) oder Baum-Semantik (|=t)?

• |= 6= |=t, betrachte dazu E(pU+q) in folgender Kripke-Struktur:

-

?

6

p

q

s1 s2

s3s4

• Is1 |=t E(pU+q), aber Is1 6|= E(pU+q), da s1 < s4 < s3 und Is4 6|= p

• Intendierte Semantik ist die Baumsemantik |=t

100


Gegeben:

• eine beliebige Kripke-Struktur I = 〈U ,≺, ι〉• und eine Formel A der CTL mit Basis-Operatoren EU+ und EG+

Universelles bottom-up Model Checking fur CTL mit EU+ und EG+

Fur alle Teilformeln F von A:

• Setze ⊥I := ∅• Falls F atomare Formel p, setze F I := ι(p)

• Falls F = (B → C), setze F I := (U \BI) ∪ CI

• Falls F = E(BU+C), setze F I := check-EU+(B,C)

• Falls F = EG+(B), setze F I := check-EG+(B)

101


Die Teilprozedur check-EU+

• Prozedur berechnet (E(BU+C))I = s ∈ U : Is |=t E(BU+C))

• Globale Datenstrukturen: zwei Zustande s, s′, zwei Mengen T,H,eine Menge (E(BU+C))I

Prozedur check-EU+(B,C) (E(BU+C))I := ∅ ;T := CI; H := CI;while T 6= ∅

s := select element(T ) ; T := T \ s;forall s′ mit s′ ≺ s

(E(BU+C))I := (E(BU+C))I ∪ s′ ;if s′ 6∈ H and s′ ∈ BI then H := H ∪ s′ ; T := T ∪ s′

102


JJJJJJJ

JJJJJJJ

ZZZZZZZZZZZZ~

=

6

3

5

2

4

1

p

q

6

q

p

Berechne die Menge der Zustandeder Kripke-Struktur, die die FormelA = E(pU+q) Baum-erfullen!

Prozedurablauf fur check-EU+(p, q):

Op. T H AI

init. 1,5 1,5 s := 1 5 1,5 s′ := 6 5 1,5 6s := 5 1,5 6s′ := 2 2 1,2,5 2,6s′ := 4 2 1,2,5 2,4,6s := 2 1,2,5 2,4,6s′ := 1 1,2,5 1,2,4,6

103

90CTL-Model Checking

Wichtige Eigenschaft der Baumsemantik: Baumsemantik ist eine”Zu-

standssemantik“, d.h. alle Knoten k im Berechnungsbaum mit gleicherZustandsmarkierung `(k) konnen

”identifiziert“ werden

Satz: Gegeben eine Kripke-Struktur I = 〈U ,≺, ι〉, die direkt von Mgenerierte Baumstruktur I ′ = 〈K,≺′, ι′〉 und eine CTL-Formel A.

Dann gilt: Is |=t A gdw I ′k |= A fur alle k ∈ K mit `(k) = s, wobei ` dieKnotenmarkierungsfunktion ist.

Beweis: Zwei beliebige Knoten k, k′ ∈ K mit `(k) = `(k′) sind Wurzelnisomorpher Unterbaume.

⇒ Zustandssemantik ermoglicht effizientes Model Checking

104

91Stark konnektierte Komponenten

Stark konnektierte Komponente (SCC) eines Graphen G = 〈U ,≺〉:Maximaler Teilgraph 〈U ′,≺′〉 von G derart, dass fur alle s, s′ ∈ U ′ mit s 6= s′

gilt: es gibt einen endlichen Pfad π : N −→ U ′ von s nach s′.

Eine SCC 〈U ′,≺′〉 heisst nicht-trivial, wenn ≺′ 6= ∅, d.h. wenn der Graphmindestens eine Kante enthalt.

s2

s5

s4s1

s3

s6

s7

s8

s9

DDDDDDDDDDDDD

AAAA

llll

,,,,

. .

..

Nicht-triviale stark konnektierte Komponenten

105





s2

s5

s4s1

s3

s6

s7

s8

s9

DDDDDDDDDDDDD

AAAA

llll

,,,,

!!!!!!EEEEEEE

%%%%%%%

TTTTTTTcccccc

QQ

QEEEEEEEEEEE

. .

..

Stark konnektierte Komponenten

106





s2

s5

s4s1

s3

s6

s7

s8

s9

DDDDDDDDDDDDD

AAAA

llll

,,,,

!!!!!!EEEEEEE

%%%%%%%

TTTTTTTcccccc

QQ

QEEEEEEEEEEE

. .

..

Nicht-triviale stark konnektierte Komponenten

107


Bedeutung stark konnektierter Komponenten (SCCs):

SCCs sind fundamental fur effiziente Model Checking-Verfahren, z.B. furEG

+-Formeln in CTL

Satz: Gegeben ein Kripke-Modell Is = 〈U ,≺, ι, s〉 und eine CTL-FormelB. Der B-Teilgraph GB = 〈U ′,≺′〉 des Rahmens von I ist der maximaleTeilgraph, der alle Zustande (Knoten) s in U mit Is |=t B enthalt.

Dann gilt: Is |=t EG+B gdw

• s ein Endpunkt in I ist oder

• es Zustande s′, s′′ gibt mit folgenden Eigenschaften:

– s ≺ s′ und– s′ ≤′ s′′, wobei s′′ ein Endpunkt in I oder in einer nicht-trivialen SCC

von GB ist.

108

93Berechnung aller stark konnektierten Komponenten

Verfahren zur Berechnung der SCCs eines Graphen:

• Tarjan [1972], Aho, Hopcroft, Ullman [1974]

• Die SCCs eines Graphen konnen in linearer Zeit berechnet werden.

Prozedur zur Berechnung der SCCs eines Graphen G = 〈U ,≺〉

• Die Zustande s ∈ U seien eindeutig nummeriert nr(s) von 1− |U|• Globale Datenstrukturen: ein Zahler c (initial = 0), zwei Arrays p und v

der Lange |U|• Nach Ablauf der Prozedur soll folgendes gelten: p[nr(s)] = p[nr(s′)] gdws und s′ in derselben SCC von G sind, d.h. jeder SCC wird ein Knotenals Reprasentant zugewiesen

Prozedur compute-SCCs forall s ∈ U compute-SCCs1(s) ;forall s ∈ U update-link(s)

109

94Berechnung aller stark konnektierten Komponenten

Prozedur compute-SCCs1(s) let i := nr(s) if v[i] = undefiniert then v[i] := c ; p[i] := s ; c := c+ 1 ;forall s′ ∈ s′ : s′ ≺ s

compute-SCCs1(s′) ;let c′ := v[nr(s′)]

if c′ ≤ v[i] then v[i] := c′ ; p[i] := s′ ;

v[nr(s′)] := |U|

Prozedur update-link(s) if p[nr(s)] 6= s then p[nr(s)] := update-link(p[nr(s)])

return p[nr(s)]

110

95Berechnung stark konnektierter Komponenten

Ablauf der Prozedur compute-SCCs1 fur alle s ∈ U (nr(si) = i)

s2

s5

s4s1

s3

s6

s7

s8

s9

DDDDDDDDDDDDDD

XX

AAAAADD

cccc

,,,,,

CC

. .

..Prozedur compute-SCCs1(s)

let i := nr(s) if v[i] = undefiniert then v[i] := c ; p[i] := s ; c := c+ 1 ;forall s′ ∈ s′ : s′ ≺ s

compute-SCCs1(s′) ;let c′ := v[nr(s′)]

if c′ ≤ v[i] then v[i] := c′ ; p[i] := s′ ;

v[nr(s′)] := |U|

Nach Ablauf der Prozedur hat c den Wert 8, die Werte von v und p sind:

nr(si) 1 2 3 4 5 6 7 8 9v[i] 0 0 0 5 0 0 6 7 8p[i] s1 s1 s6 s4 s6 s2 s7 s8 s9

nach update-link: p[i] s1 s1 s1 s4 s1 s1 s7 s8 s9

111


Die Teilprozedur check-EG+

• Prozedur berechnet (EG+B)I = s ∈ U : Is |=t EG+B

• Globale Datenstrukturen: 2 Zustande s, s′, 3 Mengen S, T ,(EG+B)I

• Sei GB der B-Teilgraph des Rahmens von I

Prozedur check-EG+(B) S := U ′ : 〈U ′,≺′〉 ist nicht-triviale SCC in GB ;T := s : s ∈

⋃S oder s in GB und Endpunkt in I ;

(EG+B)I := T ;while T 6= ∅

s := select element(T ) ; T := T \ s;forall s′ mit s′ ≺ s

if s′ 6∈ (EG+B)I then (EG+B)I := (EG+B)I ∪ s′ ;

if s′ ∈ BI then T := T ∪ s′ (EG+B)I := (EG+B)I ∪ s : s Endpunkt in I

112

97Komplexitat des Model Checking fur CTL

Effizienz- und Komplexitatsbetrachtungen des universellen ModelChecking in CTL

• Gegeben eine Kripke-Struktur I = 〈U ,≺, ι〉 und eine CTL-Formel A.Berechne mit angegebenem Bottom-up-Verfahren AI, d.h. die Mengealler Zustande s ∈ U mit Is |=t A

• Zeitkomplexitat der Berechnung aller (nicht-trivialen SCCs) linear inGroße |I| der Kripke-Struktur I• Zeitkomplexitat jeder einzelnen Teilprozedur (check-EU+, check-EG+,

etc.) linear in |I|• Anzahl der Aufrufe von Teilprozeduren linear in Große |A| der Eingabe-

formel A.

• Gesamtkomplexitat quadratisch in (|I|+ |A|), genauer O(|A| · |I|).

113

98LTL-Model Checking

Intendierte Semantik des LTL-Model Checking

• Eigenschaften beliebiger Transitionssysteme sollen modelliert werden

• Welche Semantik, Standard-Semantik (|=) oder Folgen-Semantik (|=s)?

• |= 6= |=s, betrachte dazu pU+q in folgender Kripke-Struktur:

-

?

6

p

q

s1 s2

s3s4

• Is1 |=s pU+q, aber Is1 6|= pU+q, da s1 < s4 < s3 und Is4 6|= p

• Intendierte Semantik ist die Folgensemantik |=s

114


Eigenschaften der Folgensemantik |=s:

• Is |=s A gdw fur alle von Is = 〈U ,≺, ι, s〉 generierten naturlichenModelle M gilt: M |= A.

• Eineindeutige Entsprechung von naturlichen Modellen von Is und maxi-malen s-Pfaden in I• Is |=s A gdw fur alle maximalen s-Pfade π in I gilt: Iπ |= A.

• Folgensemantik ist keine”Zustandssemantik“ sondern eine

”Pfadseman-

tik“, d.h. man kann i.A. nicht jedem Zustand s ∈ U eindeutig eineMenge von Formeln zuordnen die in s gelten. Eine Formel kann in einemmaximalen s-Pfad gelten und in einem anderen nicht.

Beispiel I:6

?

-

@@@@@I

s3s2

s1

p

Sei π1 = [s1, s2, s3, ]ω und π2 = [s1, s2, ]ω.π1 und π2 sind maximale s1-Pfade in I.Dann gilt Iπ1 |= F

+p, aber Iπ2 6|= F+p.

bla

115


Folgen- bzw. Pfadsemantik aus CTL∗:

• Iπ |= p ∈ PL (Aussagenlogik) gdw Iπ(0) |= p

• Iπ |= (A→ B) gdw Iπ 6|= A oder Iπ |= B

• Iπ |= (AU+B) gdw es ein i > 0 gibt und Iπi |= B und fur alle 0 < j < i

gilt: Iπj |= A

⇒ Pfadsemantik erschwert effizientes Model Checking

Prinzip des indirekten Beweises:

• Is |=s A gdw fur alle maximalen s-Pfade π in I gilt: Iπ |= A gdw eskeinen maximalen s-Pfad π in I gibt mit: Iπ |= ¬A• Indirekte Methode:

– Suche systematisch nach einem solchen s-Pfad, einem Gegenbeispiel.– Falls ein solches gefunden wird, gilt Is 6|=s A.– Falls die Suche scheitert, gilt Is |=s A.

116

101Folgengultigkeit in der Modallogik

• Gegeben ein Kripke-Modell Is = 〈U ,≺, ι, s〉 und eine modallogischeFormel F

• Frage: Gilt F in allen von Is generierten naturlichen Modellen, d.h.indirekt: gibt es keinen maximalen s-Pfad in I mit Iπ |= ¬F = A,keinen sog. akzeptierenden Pfad fur die Negation von F?

• Systematische Suche durch alle Paare, sog. Atome, 〈s,m〉, wobei s ∈ Uund m eine aussagenlogisch konsistente L-maximale Menge, wobei L dieMenge aller Unterformeln von A

• Beispiel: A = (¬♦ (p ∨ q) ∧ ♦ q),mogliches m fur A : ♦ (p ∨ q),¬♦ q, p, q

• Begrundung:

– Nur aussagenlogisch konsistente Formelmengen gelten auf einem Pfad– jede Formel, die weder Unterformel noch Negation einer Unterformel

von A ist, ist irrelevant (Filtrierung)

117

102Pfad-Model Checking in der Modallogik

• Gegeben ein Kripke-Modell Is0 = 〈U ,≺, ι, s0〉 und eine modallogischeFormel A

• Weitere Einschrankung der relevanten Atome 〈s,m〉 mit s ∈ U :

– 〈s,m〉 heisst zulassig gdw fur alle aussagenlogischen Unterformeln Fvon A gilt: Is |= F gdw F ∈ m

– 〈s,m〉 heisst initial, wenn A ∈ m und 〈s,m〉 zulassig (und s = s0 beiinitialem Model Checking)

• Definition einer zweistelligen Relation X zwischen zulassigen Atomen:〈s,m〉X〈s′,m′〉 gdw die folgenden Bedingungen gelten:

1. s ≺ s′,2. Wenn ♦B Teilformel von A ist, dann gilt: ♦B ∈ m gdw B ∈ m′.• Modellsuche: Aufbau eines Tableaus (mit Atomen markierter Baum) fur

jedes initiale Atom

118


• Konstruktion aller Tableaus zulassiger Atome wie folgt:

– Wurzel jedes Tableaus markiert mit einem initialen Atom– Nachfolger eines Knoten mit Atom 〈s,m〉: entsprechende Knoten fur

alle zulassigen 〈s′,m′〉 mit 〈s,m〉X〈s′,m′〉• Tableauknoten K mit Markierung α = 〈s,m〉 auf einem Ast heisst offen,

wenn s Endpunkt in ≺ ist und m keine Formel der Form ♦B enthalt;andernfalls heisst K geschlossen.

• Ein Tableauast heisst schleifenfrei, wenn jedes Atom hochstens einmalauf dem Ast vorkommt.

• Entscheidbarkeit durch Vermeidung von Schleifen im Tableau, d.h. keineErweiterung des Tableaus, wenn Atom bereits auf Ast

• Akzeptierender Ast π eines Tableaus:Tableauast P = 〈s1,m1〉, . . . , 〈sn,mn〉 derart, dass:

– entweder 〈sn,mn〉 offen oder– es gibt ein i ≤ n und 〈sn,mn〉X〈si,mi〉

119


Satz: Gegeben ein Kripke-Modell Is = 〈U ,≺, ι, s〉, eine modallogischeFormel A und die Menge aller Tableaus T fur Is und A.

Es gibt ein Tableau T ∈ T mit einem akzeptierenden Ast gdw es einenmaximalen s-Pfad π gibt mit Iπ |= A.

Beweis:”⇒“: Sei P = 〈s1,m1〉, . . . , 〈sn,mn〉 ein akzeptierender Ta-

bleauast. Entweder P ist offen, dann gilt: Iπ |= A fur π = s1, . . . , sn.Oder es gibt ein 1 ≤ i ≤ n mit 〈sn,mn〉X〈si,mi〉. Dann gilt: Iπ |= A furπ = s1, . . . , si−1, [si, . . . , sn, ]ω.

”⇐“: Sei π akzeptierender Pfad, d.h. ein maximaler s-Pfad mit Iπ |= A. π

entspricht ein direkt generiertes naturliches Modell I ′s′ = 〈U ′,≺′, ι′, s′〉von Is. Beweis durch Konstruktion eines akzeptierenden TableauastesP = 〈s1,m1〉, . . . , 〈sn,mn〉 durch Angabe einer Funktion f : P −→ U ′mit der folgenden Invariante: fur alle Formeln B ∈ mi gilt: I ′f(〈si,mi〉) |= B.Gultigkeit der Invariante garantiert Existenz eines Folgeknotens, der Invari-ante erfullt. Fuhrt schliesslich zu offenem Ast oder Schleife.

120


Modallogisches Pfad-Model Checking am Beispiel:

Gilt Is1 |=s ¬♦♦♦ p?

Indirektes Verfahren: Prufe, ob es einenmaximalen s1-Pfad gibt, der ♦♦♦ p erfullt!

Anwendung des naiven Tableauverfahrens:

6

?

-

@@

@@@I

s3s2

s1

p

• L = ♦♦♦ p,♦♦ p,♦ p, p• 2|L| = 16 zulassige L-maximale Mengen

• 4 initiale Atome: 〈s1, ♦♦♦ p, [¬]♦♦ p, [¬]♦ p,¬p〉• Akzeptierender Ast P = α1, α2, wobei α1 = 〈s1, ♦♦♦ p,¬♦♦ p,♦ p,¬p〉

und α2 = 〈s2, ¬♦♦♦ p,♦♦ p,¬♦ p, p〉. Schleife liegt vor, da α2Xα1.

• Akzeptierender Pfad π = [s1, s2, ]ω. Damit gilt: Is1 6|=s ¬♦♦♦ p.

Offensichtliche Schwache des naiven Tableauverfahrens:Fur A = ♦ · · ·♦︸︷︷︸

n

p ergeben sich 2n−1 initiale Atome.

121


Angegebenes Tableauverfahren kann optimiert werden

1. Speichern aller geschlossenen Atome bzw. aller Atome an der Wurzelgeschlossener Unterbaume und keine Expansion solcher Atome:⇒ Exponentieller Zeitgewinn moglich, ublicher Zeit-Platz-Trade-off

2. Reduktion jedes m in einem Atom 〈s,m〉 auf eine Teilmenge k, aus derm eindeutig konstruierbar, z.B. auf alle Teilformeln der Form ♦B. Jedesk kodiert die L-maximale Menge m, die eindeutig bestimmt ist durch:

– falls p ∈ P, dann p ∈ m gdw s ∈ ι(p)– ansonsten B ∈ m gdw B ∈ k⇒ Polynomieller Platzgewinn/Zeitverlust

3. Alternativ zu vorhergehendem: nur Menge der zu erfullenden Formelnspeichern, d.h. Arbeiten mit partiellen Interpretationen k: Jedes k kodierteine Menge von L-maximalen Mengen.⇒ ermoglicht exponentiellen Zeitgewinn (und Ignorieren von Schleifen)

122

107Optimiertes modallogisches Pfad-Model Checking

Grundprinzip: Arbeiten mit Mengen zu erfullender Formeln

Vorzunehmende Anderungen am naivem Verfahren:

• Gegeben ein Kripke-Modell Is0 = 〈U ,≺, ι, s0〉 und eine modallogischeFormel A; sei L Menge der Unterformeln von A.

• Formelmenge m heisst abwarts gesattigt (saturiert) gdw gilt:

– wenn (B → C) ∈ m, dann ¬B ∈ m oder C ∈ m,– wenn ¬(B → C) ∈ m, dann B ∈ m und ¬C ∈ m,– wenn ¬¬B ∈ m, dann B ∈ m.

• Definition eines Atoms 〈s,m〉: m ist abwarts saturiert und Teilmengeeiner aussagenlogisch konsistenten L-maximalen Menge.

• 〈s,m〉 heisst zulassig gdw fur alle aussagenlogischen Unterformeln F vonA gilt: wenn F ∈ m, dann Is |= F .

• 〈s,m〉 heisst initial gdw m ist minimale abwarts saturierte Menge, die Aenthalt (und s = s0 bei initialem Model Checking).

123

108Optimiertes modallogisches Pfad-Model Checking

Vorzunehmende Anderungen am naivem Verfahren:

• Definition der Transitionsrelation X zwischen zulassigen Atomen:〈s,m〉X〈s′,m′〉 gdw die folgenden Bedingungen gelten:

1. s ≺ s′,2. wenn ♦B ∈ m, dann B ∈ m′,3. wenn ¬♦B ∈ m, dann ¬B ∈ m′,4. m′ ist minimal, d.h. wenn 〈s,m〉X〈s′,m′′〉, dann m′′ 6⊂ m′.• Tableauknoten K mit Markierung α = 〈s,m〉 auf einem Ast heisst offen,

wenn m keine Modalformel enthalt oder wenn s Endpunkt in ≺ ist undm keine Formel der Form ♦B enthalt; andernfalls heisst K geschlossen.

• Bei akzeptierendem offenen Ast 〈s1,m1〉, . . . , 〈sn,mn〉 gilt: Jeder s1-Pfadin I mit Anfangsstuck s1, . . . , sn erfullt A.

• Keine Schleifenbedingung notig ⇒ ermoglicht Tabulierungsverfahrenbzw. Arbeiten mit gerichteten azyklischen Graphen anstatt mit Baumen

124


Modallogisches Pfad-Model Checking am Beispiel:

Gilt Is1 |=s ¬♦♦♦ p?

Indirektes Verfahren: Prufe, ob es einenmaximalen s1-Pfad gibt, der ♦♦♦ p erfullt!

6

?

-

@@

@@@I

s3s2

s1

p

Anwendung des optimierten Tableauverfahrens:

• Nur ein initiales Atom: 〈s1, ♦♦♦ p〉• Intuitiv naturliche Vorgehensweise

• Suchraum kleiner als bei naivemVerfahren

• Tableautiefe grosser

PPPPPPP

〈s3, ♦ p〉

〈s2, ♦♦ p〉

∗

〈s1, ♦♦♦ p〉

〈s1, ♦ p〉

offen〈s2, p〉

Vollstandiges Tableau:

125

110Pfad-Model Checking in generalisierter Modallogik

Optimierte Variante mit zu erfullenden Formeln:

• Operatormenge sei: F+• Atome, zulassige, initiale wie bei optimierter Variante der Modallogik

• Analoge Definition der Relation X zwischen zulassigen Atomen:〈s,m〉X〈s′,m′〉 gdw die folgenden Bedingungen gelten:

1. s ≺ s′,2. wenn F+B ∈ m, dann B ∈ m′ oder F+B ∈ m′,3. wenn ¬F+B ∈ m, dann ¬B ∈ m′ und ¬F+B ∈ m′,4. m′ ist minimal, d.h. wenn 〈s,m〉X〈s′,m′′〉, dann m′′ 6⊂ m′.• Tableauknoten K mit Markierung α = 〈s,m〉 auf einem Ast heisst offen,

wenn m keine Modalformel enthalt oder wenn s Endpunkt in ≺ ist undm keine Formel der Form F

+B enthalt; andernfalls heisst K geschlossen.

126


Bei generalisierter Modallogik sind i.A. Schleifen notig!

Probleme mit der modallogischen Schleifenbedingung:

• Evtl. F+B in allen Atomen der Schleife enthalten, aber B in keinem.

Beispiel:-

s1 s2

Schleife: 〈s1, F+p〉, 〈s2, F+p〉, 〈s1, F+p〉

Beobachtung:

• Um alle Bedingungen auf einem Pfad wirklich zu erfullen, sind u.U.mehrere verschiedene Durchlaufe durch denselben Zustand notig.

Beispiel: Offener Ast:〈s1, F+p,F+q〉, 〈s2, F+p,F+q〉,〈s3, F+q, p〉, 〈s1, F+q〉,〈s2, F+q〉, 〈s4, q〉

PPPP

PPPPi

)

-

3

QQQs

p

qs1

s3

s4

s2

127


Schleifenbedingung:

• Gegeben ein Tableaupfad P = 〈s1,m1〉, . . . , 〈sn,mn〉. Eine Schleife inP ist ein Teilpfad P ′ = 〈si,mi〉, . . . , 〈sl,ml〉 derart, dass sl = si undml = mi (bzw. alle modallogischen Formeln in ml sind in mi).

• Eine Schleife heisst selbsterfullend, wenn fur alle Formeln des Typs F+Bin⋃lj=imj gilt: B ∈

⋃lj=imj.

• Akzeptierender Ast π eines Tableaus:Tableauast P = 〈s1,m1〉, . . . , 〈sn,mn〉 derart, dass:

– entweder 〈sn,mn〉 offen oder– P hat eine selbsterfullende Schleife als Teilpfad.

Satz: Gegeben ein Kripke-Modell Is = 〈U ,≺, ι, s〉, eine Formel A dergeneralisierten Modallogik und die Menge aller Tableaus T fur Is und A.

Es gibt ein Tableau T ∈ T mit einem akzeptierenden Ast gdw es einenmaximalen s-Pfad π gibt mit Iπ |= A.

128


Selbsterfullende Schleifen und stark konnektierte Komponenten

Eine stark konnektierte Komponente G des Transitionsgraphen X heisstselbsterfullend, wenn fur alle F+B, die in der zweiten Komponente einesAtoms α vorkommen, ein Atom α′ existiert, in dessen zweiter KomponenteB vorkommt und 〈α, α′〉 in der transitiven Hulle von X ist.

Satz: Es gibt einen akzeptierenden Pfad fur A in einem Kripke-Modell gdweine selbsterfullende SCC in der entsprechenden Relation X existiert, dievon einem initialen Atom erreicht werden kann.

Verschiedene Paradigmen fur Model Checking-Verfahren

• Globale Verfahren: Erzeuge den Graphen X, berechne stark konnektierteKomponenten, prufe Selbsterfulltheit (Vorteil: nur maximale konnektierteKomponenten zu betrachten, Nachteil: EXPSPACE-Verfahren)

• Lokale Verfahren: Erzeuge alle Tableaus wie o.g. (Vorteil: u.U. PSPACE-Verfahren zu erreichen, Nachteil: beliebige Teilpfade zu betrachten, Red-undanzen im Tableau)

129

114Model Checking in LTL

• Hier nur Beschrankung auf zukunftsbezogenes Fragment: U+

• Anderungen bei der Definition der Relation X zwischen zulassigen Ato-men: 〈s,m〉X〈s′,m′〉 gdw die folgenden Bedingungen gelten:

1. s ≺ s′,2. wenn BU+C ∈ m, dann C ∈ m′ oder B,BU+C ⊆ m′,3. wenn ¬(BU+C) ∈ m, dann ¬C,¬B ⊆ m′ oder

¬C,¬(BU+C) ⊆ m′,4. m′ ist minimal, d.h. wenn 〈s,m〉X〈s′,m′′〉, dann m′′ 6⊂ m′.• Tableauknoten K mit Markierung α = 〈s,m〉 auf einem Ast heisst offen,

wenn m nur aussagenlogische Formeln enthalt oder wenn s Endpunkt in≺ ist und m keine Formel der Form BU+C enthalt; andernfalls heisstK geschlossen.

• Schleife wie in generalisierter Modallogik heisst selbsterfullend, wenn furalle Formeln des Typs BU+C in

⋃lj=imj gilt: C ∈

⋃lj=imj.

130


Prozedur check-U+(α, P ) /∗ α Atom, P Liste von Atomen ∗/let 〈s,m〉 := α ;

if m propositional or ( no BU+C ∈ m and s′ : s ≺ s′ = ∅ )then return(α · P ) /∗ akzeptierender Ast ∗/

elsif α ∈ P then let P ′ · α · P ′′ := P ; /∗ · sei Konkatenation ∗/if check-fulfilled(α · P ′) then

return(P ) /∗ akzeptierender Ast ∗/else let S := α′ : αXα′ ;

forall α′ ∈ S check-U+(α′, α · P )

Prozedur check-fulfilled(P ) let E := C : es gibt 〈s,m〉 ∈ P mit BU+C ∈ m ;

if E ⊆⋃m : es gibt 〈s,m〉 ∈ P then return true

else return false

Aufruf von check-U+ fur alle initialen Atome mit P = ∅

131


Komplexitatsanalyse des vorgestellten Algorithmus

• Problem: Große der Relation X ist O(|I| × 2|A|+1), im worst-caseexponentiell in der Große der Eingabe; bei nichtexpliziter Erzeugung vonX zu beheben.

• check-fullfilled: Zeitkomplexitat jedes Aufrufs polynomiell in P

• check-U+: Platzkomplexitat: exponentiell in der Eingabe

– Anzahl der Nachfolger |S|: bei inkrementeller Erzeugung der Nachfol-ger zu beheben

– Pfadlange |P |: Lasst sich die maximale Pfadlange polynomiell be-schranken? Wenn ja, ware Problem in NP. Wenn nein, wie erreichtman polynomielle Platzbeschrankung (und praktisch effizientes Ver-fahren)?

Satz: (Sistla und Clarke [1986], Lichtenstein und Pnueli [1985])Folgengultigkeit in LTL ist PSPACE-vollstandig.

132


Komplexitaten in der Praxis

• |X| ist O(|I| × 2|A|+1)

• In der Praxis ist aber normalerweise |I| >> 2|A|

• Mit explizitem Model Checking sind lediglich Problemgrossen bis ca. 106

Atomen behandelbar

Wie lasst sich generell die Große von I reduzieren?

• Ansatz: Implizites Model Checking:symbolische Reprasentation von Zustandsmengen

133

118Modellierung reaktiver Systeme

Reaktive Systeme

• Zu modellierende Systeme bestehen i.A. aus Komponenten, die sichunabhangig voneinander andern konnen (asynchrones Verhalten).

• Ein beliebtes Modellierungsparadigma ist z.B. die Interleaving-Semantik:Zu jeder Zeit andert sich genau eine Komponente

• Das Verhalten jeder Teilkomponente ki kann durch eine Transitionsrela-tion ti beschrieben werden

• Das Verhalten des Gesamtsystems wird i.A. durch das kartesische Pro-dukt Πn

i=1ti der einzelnen Transitionsrelationen beschrieben (bzw. durcheine Teilmenge des kartesischen Produktes, falls gemeinsame Resourcenbetroffen sind)

134


Beispiel:

• Jede Komponente ist im 0 oder 1-Zustand.

• Jede Komponente kann den Zustand einer benachbarten anderen um deneigenen Wert erhohen (+) oder vermindern (−) modulo 2 oder nichtstun (Problem der Synchronizitat bzw. Asynchronizitat!).

AAAAU

AAAAAAK

-

k2k1

k3

++−

−

+−

135

120Kombinatorisches Grundproblem des Modellierens

Explosion des Zustandsraumes

• Ein Kripke-Modell simuliert ein System von Komponenten und derenInteraktionen durch Beschreibung des Gesamtzustandes (aller System-komponenten) und dessen Anderung

• ⇒ Hinzufugung von Komponenten lasst Zustandsraum im Kripke-Modellexplodieren

Beispiel:

-

k2k1 +−

-

k2k1 +−

AAAAU

AAAAAAK

-?

66

?

k3

++−

−

k4 k3

−

+

−+ +−

136

121Symbolisches Model Checking

Arbeiten mit symbolischer Reprasentation von Zustandsmengen

• Der Erfolg des Model Checking in der Praxis grundet sich zum großenTeil auf die Verwendung effizienter Datenstrukturen

• Jede aussagenlogische Formel F , die die Aussagenvariablen p1, . . . , pnenthalt, kann aufgefasst werden als n-stellige Boolesche Funktion vonBelegungen der p1, . . . , pn auf die Menge der Wahrheitswerte

• Es existieren sehr effiziente Methoden fur die Manipulation BoolescherFunktionen

• ⇒ Versuch der Reprasentation temporaler Formeln mittels BoolescherFunktionen

137

122Effiziente Reprasentation endlicher Mengen

Moglichkeiten der Reprasentation von Teilmengen einer Grundmenge

Beispiel: Teilmenge S = 0, 2, 4, 6, 8, 10, 12, 13, 14, 15einer Grundmenge G = 0, . . . , 15

• Mogliche Standard-Reprasentationen von S: als Liste, als Array, alsBitfolge

• Verschiedene Datenstrukturen bieten unterschiedliche Effizienz bei Zugriffund Anderung der Daten, erfordern aber unterschiedlichen Platzbedarf(z.B. bei Array konstanter Zugriff bei linearem Platzbedarf)

• In der Praxis des Model Checking ist ein Hauptproblem der Platzbedarf,d.h. hochste Zugriffseffizienz ist nachrangig

138

123Effiziente Reprasentation endlicher Mengen

Ansatz: Symbolische Darstellung von Mengen

Beispiel: Teilmenge S = 0, 2, 4, 6, 8, 10, 12, 13, 14, 15einer Grundmenge G = 0, . . . , 15

• Sei ~v = v1v2v3v4 ein binare Kodierung der Zahlen in G, dann lasst sichS explizit darstellen durch:

S = 0000, 0010, 0100, 0110, 1000, 1010, 1100, 1101, 1110, 1111

• Alternativ lasst sich aber S auch symbolisch kurzer ausdrucken durch:

S = ~v : v4 = 0 oder (v1 = 1 und v2 = 1)

• Letzteres entspricht einer aussagenlogischen Formel: ¬p4 ∨ (p1 ∧ p2),wobei pi := vi = 1 und ¬pi := vi = 0

139

124Binare Entscheidungsdiagramme (BDDs)

Anforderungen an eine symbolische Reprasentation

• Moglichst kompakte Darstellbarkeit endlicher Mengen

• Moglichst effiziente Manipulation (z.B. Vereinigung, Schnitt, Komple-ment) der Reprasentationsobjekte

• Moglichst einfacher Vergleich zweier Reprasentationsobjekte, die diesel-ben Mengen darstellen

• Beliebige aussagenlogische Formeln zu allgemein fur effiziente Manipula-tionen und Vergleich

• Erfolgreicher Kompromiß in der Praxis des Model Checking:Binare geordnete Entscheidungsdiagramme (OBDDs)

140


Grundlage: logisches Konnektiv Ite (if then else)

• Definition: Ite(A,B,C) gdw ((A→ B) ∧ (¬A→ C))

• Es gilt weiterhin: Ite(A,B,C) ≡ ((A ∧B) ∨ (¬A ∧ C))

• Da (A → B) ≡ Ite(A,B,>), ist die Junktorenmenge Ite,>,⊥ aussa-genlogisch vollstandig.

• Gegeben eine Menge P aussagenlogischer Variablen.Die Menge der BDD-Formeln (in Baum-Form) fur P ist wie folgt definiert:

BDD(P) := ⊥ | > | Ite(P, BDD,BDD)

• Jede BDD-Formel F kann als binarer Entscheidungsbaum bzw. alsbinarer Entscheidungsgraph dargestellt werden.

141


Grundlage: Binare Entscheidungsbaume

• Jede BDD-Formel F kann als binarer Entscheidungsbaum dargestelltwerden, der wie folgt definiert ist.

• Jeder Teilformel der Form Ite(p,B,C) von F entspricht ein markierterBinarbaum:

– dessen Wurzel ist mit p markiert,– von ihr gehen zwei Kanten aus, eine ist mit 1 markiert (die zum Baum

fur B fuhrt) und eine mit 0 (die zum Baum fur C fuhrt),– der Baum fur > und ⊥ ist ein Knoten, der mit 1 bzw. 0 markiert ist.

• Der so beschriebene Baum ist der Entscheidungsbaum der BDD-Formel.

142


Geordnete reduzierte BDD-Formeln und binare Entscheidungsbaume

• Sei < eine Ordnung auf den aussagenlogischen Variablen P.

• Eine BDD-Formel F ist in geordneter Form (bzgl. <) oder ist eineOBDD-Formel gdw fur jede Teilformel Ite(p,B,C) von F und jedeTeilformel Ite(q,B′, C ′) von B und C gilt: p < q.

• Eine BDD-Formel F ist in reduzierter Form gdw wenn sie keine Teilformelder Form Ite(p,B,B) enthalt.

• Der einer OBDD-Formel in reduzierter Form (bzgl. <) entsprechendebinare Entscheidungsbaum heisst geordneter reduzierter binarer Entschei-dungsbaum (bzgl. <).

Satz: Zu jeder aussagenlogischen Formel uber einer beliebigen vollstandi-gen Junktorenmenge und jeder Ordnung < auf den aussagenlogischen Va-riablen gibt es genau eine logisch aquivalente OBDD-Formel in reduzierterForm bzgl. <.

143


Erzeugung geordneter reduzierter BDD-Formeln

• Hier fur aussagenlogische Formeln uber →,>,⊥

• Vorgehen: zunachst wiederholte Anwendung der sog. Shannon-Expansion:

A ≡ Ite(p,A[p/>], A[p/⊥])

auf Teilformeln, die nicht in geordneter BDD-Form, wobei p die kleinsteVariable bzgl. < in A

• Dann Reduzierung: durch Boolesche Vereinfachungen wie:

Ite(p,B,B) ≡ B oder (⊥ → >) ≡ >

144


”Sharing“ in BDD-Formeln und Entscheidungsbaumen

• In einer BDD-Formel kann dieselbe Teilformel mehrmals vorkommen.

• Diese Redundanz lasst sich durch Einfuhrung von Abkurzungen (Namenfur komplexe Teilformeln) beseitigen

• Eine BDD-Formel mit Abkurzungen ist eine BDD-Formel uber ei-nem erweiterten Variablenalphabet P ∪ δ1, . . . , δn plus eine Liste vonAbkurzungen der Form

δi := Ite(p,B,C),

wobei Ite(p,B,C) eine BDD-Formel uber P ∪ δi+1, . . . , δn ist.

• Der Einfuhrung von Abkurzungen entspricht in der graphischen Darstel-lung der Ubergang von Baumen zu azyklischen gerichteten Graphen, sog.binaren Entscheidungsdiagrammen.

145

130Geordnete binare Entscheidungsdiagramme (OBDDs)

• Ein binares Entscheidungsdiagramm heisst minimal gdw kein Teilgraphmehr als einmal vorkommt und kein Knoten zwei gleiche Nachfolger hat.

• Zu jedem binaren Entscheidungsbaum gibt es genau ein minimales binaresEntscheidungsdiagramm.

Satz: Sei < eine Ordnung auf den aussagenlogischen Variablen und B dieeiner beliebigen aussagenlogischen Formel F und < entsprechende logischaquivalente reduzierte OBDD-Formel F ′. Sei B das minimale binare Ent-scheidungsdiagramm des binaren Entscheidungsbaums von F ′. Wir nennenB das Entscheidungsdiagramm fur F und <. Dann gilt: Bezuglich ei-ner Variablenordnung < haben alle logisch aquivalenten aussagenlogischenFormeln dasselbe Entscheidungsdiagramm.

• Verschiedene aussagenlogische Formeln konnen u.U. dieselbe BoolescheFunktion darstellen

• Starke Kanonizitat: Fur jede Variablenordnung entspricht jeder Boole-schen Funktion genau ein minimales geordnetes Entscheidungsdiagramm.

146

131Erzeugung von OBDDs

Erzeugung eines OBDD aus einer aussagenlogischen Formel A mit nVariablen: Initaler Aufruf ist pl2bdd(A, 1).

• Ein innerer BDD-Knoten δ sei implementiert als eine Struktur 〈i, j, δ0, δ1〉,wobei i ∈ N der Index, j die j-te Variable in <, δ0 der 0-Nachfolger undδ1 der 0-Nachfolger von δ.

• Alle neu erzeugten BDD-Knoten werden in einer Struktur struct gespei-chert, die initial leer ist.

Prozedur pl2bdd(F, j) : (Formel,nat)if j > n then return evaluate(F ) /∗ liefert 0 bzw. 1 ∗/

else δ0 := pl2bdd(F [vj/⊥], j + 1) ; δ1 := pl2bdd(F [vj/>], j + 1) ;if δ0 = δ1 then return δ0 elsif ∃i: 〈i, j, δ0, δ1〉 ∈ struct then return 〈i, j, δ0, δ1〉 else δ := 〈|struct|+ 1, j, δ0, δ1〉 ; struct := struct ∪ δ ;

return δ

147

132Operationen auf OBDDs

Gegegen zwei OBDDs (bzgl. einer Variablenordnung < von aussagenlogi-schen Formeln bzw. Booleschen Funktionen F1 und F2).

Reduktion: Minimierung der OBDDs

Kombinationen Boolescher Funktionen:

•”Komplement“bildung: Erzeugung des minimalen OBDDs (bzgl. <) von¬F1

• Direkte Bildung der minimalen OBDDs (bzgl. <) von F1 → F2, F1∨F2,F1 ∧ F2, F1 ↔ F2 aus den gegebenen OBDDs.

Satz: Fur jede der Operationen gibt es Verfahren, deren Zeitkomplexitatlinear ist in der Grosse der Eingabegraphen.

Satz: Es gibt aussagenlogische Formeln/Boolesche Funktionen, derenOBDD fur alle Variablenordnungen exponentiell ist. (Z.B. die Funktion furden n-ten Output einer Integer-Multiplikationsschaltung)

148

133Operationen auf OBDDs

Anwendung beliebiger Boolescher Funktionen [Bryant, 1986]:

Prozedur BDD-apply(, δ, δ′) : (Operator,BDD,BDD)

if δ, δ′ ∈ 0 , 1 then return δ”“ δ′ /∗ liefert 0 bzw. 1 ∗/

else j := index(min-var(δ, δ′)) ;〈f0, f1〉 := co-factor(δ, j) ; 〈g0, g1〉 := co-factor(δ′, j) ;δ0 := BDD-apply(, f0, g0) ; δ1 := BDD-apply(, f1, g1) ;if ∃δ′′ ∈ struct mit δ′′ = 〈i, j, δ0, δ1〉 then return δ′′ else δ′′ := 〈|struct|+ 1, j, δ0, δ1〉 ; struct := struct ∪ δ′′ ;

return δ′′

Prozedur co-factor(δ, j) : (BDD,nat)

if δ ∈ 0 , 1 then return 〈δ, δ〉 else 〈i, k, δ0, δ1〉 := δ ;

if k > j then return 〈δ, δ〉 else return 〈δ0, δ1〉

149

134Bedeutung der Variablenordnung in OBDDs

Bei Anderung der Variablenordnung u.U. exponentielle Unterschiede

Beispiel:

• Modellierung eines Vergleichers zweier Bit-Vektoren

a = a1 · · · an und b = b1 · · · bn.

• Bei Variablenordnung a1 < b1 < · · · < an < bn: 3n+ 2 Knoten

• Bei Variablenordnung a1 < · · · < an < b1 < · · · < bn: 3× 2n− 1 Knoten

Satz: Finden einer Ordnung mit kleinstem OBDD ist NP-hart.

Methoden der Ordnungsfestlegung:

• Praktisch erfolgreiche Heuristik zur Ordnungsbestimmung: Zusammen-gruppierung

”abhangiger“ Variablen

• Falls keine offenkundige Ordnung gegeben, in periodischen Abstandendynamischer Wechsel der Ordnung.

150

135Anwendungen von OBDDs

• Feststellung der logischen Implikation bzw. Aquivalenz zweier aussagen-logischer Formeln: Komplexitat linear in der Grosse der BDDs

• Entscheidungsverfahren fur aussagenlogische Erfullbarkeit:

– Falls Formel unerfullbar, liefert Verfahren pl2bdd das BDD 0 .

– Falls Formel allgemeingultig, liefert Verfahren pl2bdd das BDD 1 .

– Im worst-case exponentielle Platzkomplexitat

• Praktisch effiziente Reprasentation der Menge aller erfullenden Belegun-gen einer aussagenlogischen Formel

• Damit praktisch effiziente Reprasentation von Teilmengen aus einer end-lichen Grundmenge G

• Praktisch effiziente Reprasentation von Relationen uber einer endlichenGrundmenge G

• Praktisch effiziente Reprasentation der Anzahl der erfullenden Belegungeneiner aussagenlogischen Formel

151

136Die Standardparadigmen fur SAT-Verfahren

Semantische Baume [Davis, Loveland, Logemann, 1962]

• Verbesserung der Wahrheitstafelmethode

• Partitionierung der Interpretationen und partielle Evaluierung

• Effiziente Implementierungstechnik (Backtracking-Verfahren)

Geordnete binare Entscheidungsdiagramme (OBDDs) [Bryant, 1986]

• Formalismus zur Darstellung Boolescher Funktionen

• Verschiedene Funktionalitaten

• Effiziente Modifikationsverfahren (Kombination, Reduktion)

152

137Arbeitsweise von OBDD-Verfahren

Klauseln

c1: ¬a ∨ ¬bc2: b ∨ ¬cc3: b ∨ cc4: a ∨ ¬b

Ordnung

a < b < c

a

a

0

0

%%%

eee

%%%

eee

%%%

eee

%%%

eee

eee

%%%

eee

%%%

eee

%%%

eee

%%%

b0

1

0 1

1 0

G(c1)

1

0

0 1

1 0

b

c

G(c2)

1

0

1 0

1 0

b

c

G(c3)

b0 1

1 0

1

0

G(c4)

01

b

c

1

1

0 0

1

0 1

a

b

0

1

1

a

b

0

01

G(c1 ∧ c2)

G(c1 ∧ c2 ∧ c3)

G(c1 ∧ · · · ∧ c4)

153

138Semantische Baume

• Optimierung der Wahrheitstafelmethode

• Schrittweise Partitionierung der Belegungsmenge (Aste)

• Typischerweise fur Klauselformeln

Definition Semantischer Baum fur Klauselmenge S:

Binarbaum, dessen Kanten mit Literalen und dessen Blattknoten moglicher-weise mit Klauseln aus S markiert sind wie folgt:

• Jedes Paar von Kanten, die aus einem gemeinsamen Knoten entspringen,ist mit einer Variablen p, die in S vorkommt, bzw. mit ¬p markiert,wobei p nicht bereits auf dem Ast vorkommt.

• jeder Blattknoten kann mit einer Klausel c ∈ S markiert sein, falls dieKomplemente aller Literale in c auf dem Ast vorkommen.

Eine Semantischer Baum fur S heisst geschlossen, falls jeder Blattknotenmit einer Klausel (aus S) markiert ist.

154

139Semantischer Baum: Beispiel

Geschlossener Semantischer Baum Klauseln

JJJJJJ

JJJJJJ

JJJJJJ

JJJJJJ

ZZZZZZZZ

b ∨ cb ∨ ¬cb ∨ cb ∨ ¬c

¬c ¬c

¬b ¬b

¬a

a ∨ ¬b¬a ∨ ¬b

b

a

b

cc 2

2

2

2 ¬a ∨ ¬b

b ∨ ¬c

a ∨ ¬b

b ∨ c

155

140Arbeitsweise Semantischer Baum-Verfahren

Semantischer Baum Klauseln

2

2

2

2 ¬a ∨ ¬b

b ∨ ¬c

b ∨ c

a ∨ ¬b

156



2

2

2

1 ¬a ∨ ¬b

b ∨ ¬c

b ∨ c

a ∨ ¬b

ZZZZZZZZ

¬aa

157



2

2

2

0 ¬a ∨ ¬b

b ∨ ¬c

b ∨ c

a ∨ ¬b

JJJJJJ

ZZZZZZZZ

¬b

¬a

¬a ∨ ¬b

b

a

158



2

1

1

1 ¬a ∨ ¬b

b ∨ ¬c

a ∨ ¬b

b ∨ c

JJJJJJ

ZZZZZZZZ

¬b

¬a

¬a ∨ ¬b

b

a

159



2

0

0

¬a ∨ ¬b

b ∨ ¬c

a ∨ ¬b

b ∨ c

1

JJJJJJ

JJJJJJ

ZZZZZZZZ

b ∨ cb ∨ ¬c

¬c

¬b

¬a

¬a ∨ ¬b

b

a

c

160



1

2

2

2 ¬a ∨ ¬b

b ∨ ¬c

a ∨ ¬b

b ∨ c

JJJJJJ

JJJJJJ

ZZZZZZZZ

b ∨ cb ∨ ¬c

¬c

¬b

¬a

¬a ∨ ¬b

b

a

c

161



0

2

2

2 ¬a ∨ ¬b

b ∨ c

a ∨ ¬b

b ∨ ¬cJJJJJJ

JJJJJJ

JJJJJJ

ZZZZZZZZ

b ∨ cb ∨ ¬c

¬c

¬b ¬b

¬a

a ∨ ¬b¬a ∨ ¬b

b

a

b

c

162



1

1

1

2 ¬a ∨ ¬b

b ∨ ¬c

b ∨ c

a ∨ ¬b

JJJJJJ

JJJJJJ

JJJJJJ

ZZZZZZZZ

b ∨ cb ∨ ¬c

¬c

¬b ¬b

¬a

a ∨ ¬b¬a ∨ ¬b

b

a

b

c

163



JJJJJJ

JJJJJJ

JJJJJJ

ZZZZZZZZJJJJJJ

b ∨ cb ∨ ¬cb ∨ cb ∨ ¬c

¬c ¬c

¬b ¬b

¬a

a ∨ ¬b¬a ∨ ¬b

b

a

b

cc 1

0

2 ¬a ∨ ¬b

b ∨ ¬c

a ∨ ¬b

0

b ∨ c

164



JJJJJJ

JJJJJJ

JJJJJJ

JJJJJJ

ZZZZZZZZ

b ∨ cb ∨ ¬cb ∨ cb ∨ ¬c

¬c ¬c

¬b ¬b

¬a

a ∨ ¬b¬a ∨ ¬b

b

a

b

cc 2

2

2

2 ¬a ∨ ¬b

b ∨ ¬c

a ∨ ¬b

b ∨ c

165

141Vergleich der Standardparadigmen

Semantischer Baum OBBD

Datenstruktur Baum”Dag“

Platzkomplexitat PSPACE EXPSPACE

Zeitkomplexitat EXPTIME EXPTIME

Variablenordnung sehr flexibel weniger flexibel

Inferenzraten sehr hoch weniger hoch

(Backtracking) (Saturierung)

Mittlere Beweislange sehr lang weniger lang

(Baumresolution) (Geordnete Resolution)

Allerdings gilt: Die Baumresolution und die geordnete Resolution konnensich nicht gegenseitig polynomiell simulieren.

166

142Reprasentation von Kripke-Strukturen als BDDs

Reprasentation von Teilmengen des Universums U :

• Reprasentation jedes Zustandes s ∈ U zunachst als Bitvektor v der Langen = dlog2 |U|e und dann als Konjunktion s′ von Literalen der Form vioder ¬vi(1 ≤ i ≤ n)

• Festlegung einer linearen Ordnung < auf v1, . . . , vn• Reprasentation jeder Teilmenge S von U als OBDD der Formel

∨s∈S s

′

bzgl. der Variablenordnung <

Reprasentation der Transitionsrelation ≺ der Kripke-Struktur:

• Betrachtung der charakteristischen Funktion C : U × U −→ 0, 1 derTransitionsrelation ≺• Dann kann jedes Element in C reprasentiert werden als ein Bitvektor v

der Lange 2n, damit als Konjunktion s′ von Literalen der Form vi oder¬vi(1 ≤ i ≤ 2n); schliesslich Reprasentation von C analog S

167

143Symbolisches Model Checking fur CTL

• Anstatt auf einzelnen Zustanden und Transitionen mussen Operationenauf Mengen arbeiten.

• Besonders geeignet dafur: eine Fixpunkt-Charakterisierung der Operato-ren der temporalen Logik

• Eine Teilmenge S′ einer Menge S heißt Fixpunkt einer Funktion f :2S −→ 2S (2S Potenzmenge von S), falls f(S′) = S′.

• Die Menge der Zustande in einer Kripke-Struktur, in denen eine CTL-Formel gilt, kann durch den kleinsten bzw. großten Fixpunkt einer be-stimmten Funktion charakterisiert werden.

168

144Fixpunkt-Reprasentationen

• Sei im folgenden I = 〈U ,≺, ι〉 eine beliebige Kripke-Struktur.

• Wir betrachten Operationen auf der Potenzmenge 2U von U ; fur diepartielle Ordnung ⊆ bildet 2U einen Verband.

• Jede Teilmenge S von U kann auch als Pradikat angesehen werden, daswahr ist fur genau die Zustande in S.

Eine Funktion f : 2U −→ 2U heißt Pradikat-Transformation fur U .

• f ist monoton gdw f(P ) ⊆ f(Q), falls P ⊆ Q.

• f ist ∪-stetig gdw aus P1 ⊆ P2 ⊆ · · · folgt, dass f(⋃Pi) =

⋃f(Pi).

• f ist ∩-stetig gdw aus P1 ⊇ P2 ⊇ · · · folgt, dass f(⋂Pi) =

⋂f(Pi).

• f(f(· · · (︸︷︷︸n-mal

S) · · ·) kurzen wir ab durch fn(S).

169

145Eigenschaften von Fixpunkt-Reprasentationen

Satz: Jede monotone Pradikat-Transformation f fur U hat einen kleinstenFixpunkt (geschrieben µf bzw. falls f explizit angegeben: µZ.f(Z)) undeinen großten Fixpunkt (geschrieben νf bzw. νZ.f(Z)).

Satz: Sei f monoton.

• Dann ist µf =⋂S ⊆ U : f(S) ⊆ S und νf =

⋃S ⊆ U : f(S) ⊇ S.

• Dann gilt fur alle i ∈ N0 : f i(∅) ⊆ f i+1(∅) und f i(U) ⊇ f i+1(U).

• Wenn f ∪-stetig ist, dann ist µf =⋃f i(∅) : i ∈ N0.

• Wenn f ∩-stetig ist, dann ist νf =⋂f i(U) : i ∈ N0.

Satz: Sei f monoton und U endlich.

• Dann ist f ∪-stetig und ∩-stetig.

• Dann gibt es naturliche Zahlen k und l mit µf = fk(∅) und νf = f l(U).

170

146Berechnung der Fixpunkte

Sei f eine Pradikat-Transformation fur eine Menge U und P ein Pradikat,d.h. eine Teilmenge von U .

Prozedur fp(f, P ) : (Pradikat-Transformation,Pradikat) Q := P ;Q′ := f(Q) ;while Q 6= Q′

Q := Q′ ;Q′ := f(Q′)

return Q

Satz: Wenn f monoton und U endlich ist, dann terminiert fp(f, P ) furP = ∅ oder P = U nach ≤ |U| Schritten; fp(f, ∅) liefert den kleinsten undfp(f,U) den großten Fixpunkt von f .

171

147Fixpunkte von Pradikat-Transformationen und CTL

• Gegeben eine Kripke-Struktur I = 〈U ,≺, ι〉 und eine CTL-Formel A.

• Die Menge AI = s ∈ U : Is |= A ist ein Pradikat (von U).

• Im folgenden sei I fest und wir identifizieren jede CTL-Formel A mit derMenge AI, d.h. s ∈ A bedeutet Is |= A.

• Jeder CTL-Operator kann als Fixpunkt einer entsprechenden Pradikat-Transformation dargestellt werden wie folgt:

– AF∗A = µZ.(A ∨ AXZ)– EF∗A = µZ.(A ∨ EXZ)

– AG∗A = νZ.(A ∧ AXZ)– EG∗A = νZ.(A ∧ EXZ)

– A(AU∗B) = µZ.(B ∨ (A ∧ AXZ))– E(AU∗B) = µZ.(B ∨ (A ∧ EXZ))

• EXZ charakterisiert die Zustandsmenge s : es gibt ein s′ s : s′ ∈ ZI• AXZ charakterisiert s : es gibt ein s′ s und fur alle s′′ s : s′′ ∈ ZI

172

148Fixpunkt-Charakterisierungen fur CTL

Basis-Operatoren

Da der Operator EX Grundlage der Fixpunkt-Charakterisierungen ist, be-trachten wir eine Variante der CTL mit den drei Basis-Operatoren EX,EU∗ und EG∗, die ausreichen um jede CTL-Formel auszudrucken.

Die BDD-basierten Model Checking-Verfahren stutzen sich auf die Gultigkeitder beiden folgenden Gleichungen:

– EG∗A = νZ.(A ∧ EXZ)

– E(AU∗B) = µZ.(B ∨ (A ∧ EXZ))

Sei im folgenden I = 〈U ,≺, ι〉 eine endliche Kripke-Struktur und A und Bbeliebige CTL-Formeln (bzw. die Zustandsmengen AI und BI).

173

149Korrektheit der Fixpunkt-Charakterisierung fur EG∗

Beweis fur EG∗A = νZ.(A ∧ EXZ):

• Zeige, dass die Funktion f = λZ.(A ∨ AXZ) monoton ist:Ang. P1 ⊆ P2. Sei s ∈ f(P1) = (A∨AXP1)⇒ Is |= P1 und Is |= EXP1,

d.h. ∃s′ s: Is′ |= P1⇒ nach Ann. s′ ∈ P2⇒ s ∈ (A∨AXP2) = f(P2).

• Da U endlich ⇒ f ist ∩-stetig, νf existiert und ∃l : f l(U) = νf .

• Zeige: Fur alle s ∈ νf : s ∈ AI und ∃s′ s : s ∈ νf :Sei s ∈ f l(U) ⇒ s ∈ f(f l(U)) ⇒ Is |= A und ∃s′ s : s′ ∈ f l(U).

• Zeige: EG∗A ist ein Fixpunkt von f , d.h. EG∗A = (A ∨ AXEG∗A):

”⊆“: Is1 |= EG

∗A ⇒ es gibt maximalen s1-Pfad P in I: ∀si in P :Isi |= EG

∗A⇒ Is1 |= A und Is2 |= EG∗A, d.h. Is1 |= (A∨EXEG∗A).

• Zeige durch Induktion uber i, dass EG∗A =⋂f i(U) : i ∈ N0 = νf .

”⊆“: i = 0 trivial. i→ i+1: Ind.-ann. EG∗A ⊆ f i(U). Da f monoton⇒f(EG∗A) ⊆ f i+1(U). Da EG∗A Fixpunkt von f ⇒ f(EG∗A) = EG

∗A.

Beweis fur E(AU∗B) = µZ.(B ∨ (A ∧ EXZ)) ist ahnlich

174

150Quantifizierte Boolesche Formeln

• Zur Darstellung der symbolischen Model-Checking-Verfahren gibt es einekompaktere Sprache fur komplexe Operationen auf Booleschen Formeln


• Die (Formeln der) Quantifizierten Boolesche Logik fur P sei(en) definiertdurch:

QBF (P) := P | ⊥ | (QBF → QBF ) | ∃P QBF

• dazu ubliche weitere Junktoren und den Quantor ∀ := ¬∃¬• Erweiterung der aussagenlogischen Semantik:

– I |= ∃pA gdw I |= (A[p/>] ∨A[p/⊥])• Zu jeder QBF-Formel gibt es eine aquivalente aussagenlogische Formel,

aber QBF-Formeln sind i.A. kurzer

• Allgemeingultigkeit einer QBF-Formel ist PSPACE-vollstandig

• Gegeben ∃v1 · · · ∃vnA, sei V = v1, . . . , vn und k die Grosse desBDDs von A. Es gibt ein in k lineares Verfahren, das entsprechendQBF-Semantik einen aquivalenten BDD ohne die Variablen V erzeugt.

175

151BDDs fur Quantifizierte Boolesche Formeln

Elimination existentieller BDD-Variablen:

Prozedur BDD-exists(V, δ) : (Variablenindex-Menge,BDD)

if δ ∈ 0 , 1 then return δ

else 〈i, k, δ0, δ1〉 := δ ;δ′0:= BDD-exists(V, δ0)) ;δ′1:= BDD-exists(V, δ1)) ;if k ∈ V then return BDD-apply(∨, δ′0, δ′1) else return new-node(k, δ′0, δ

′1)

Prozedur new-node(k, δ0, δ1) : (nat,BDD,BDD)if ∃δ ∈ struct : ( var(δ) = k and 0-succ(δ) = δ0 and 1-succ(δ) = δ1 )

then return δ else δ := 〈|struct|+ 1, k, δ0, δ1〉 ; struct := struct ∪ δ ;

return δ

176


Basis-Operatoren

Wir betrachten eine Variante der CTL mit den drei Basis-Operatoren EX,EU∗ und EG∗, die ausreichen um jede CTL-Formel auszudrucken.

Symbolisches universelles bottom-up Model Checking fur CTL

Gegeben eine Kripke-Struktur I = 〈U ,≺, ι〉 und eine Festlegung der Re-prasentation von Teilmengen von U und ≺ als OBDDs.Fur alle Teilformeln F von A berechne check(F ) ein OBDD, das alleZustande F I reprasentiert.

• Falls F = B C fur einen Junktor ,check(F ) = BDD-apply(,check(B),check(C))

• Falls F = EXB, check(F ) = checkEX(check(B))

• Falls F = E(BU∗C), check(F ) = checkEU∗(check(B),check(C))

• Falls F = EG∗(B), check(F ) = checkEG∗(check(B))

177


Die Prozedur checkEX

• checkEX(BDD(BI)) soll den BDD der Menge s ≺ s′ : s′ ∈ BIerzeugen, aber wie?

• Sei n = dlog2 |U|e. Man reprasentiere die Menge aller Zustande miteinem Nachfolger in BI als BDD der quantifizierten Booleschen Formel

∃w1 · · · ∃wn(F (w1, . . . , wn) ∧R(v1, . . . , vn, w1, . . . , wn))

wobei F (w1, . . . , wn) die Menge BI und R(v1, . . . , vn, w1, . . . , wn) dieTransitionsrelation ≺ als BDDs reprasentieren sollen.

178


Die Prozedur checkEU∗:

• Die Berechnung von checkEU∗(BDD(B),BDD(C)) basiert auf der Fix-punktcharakterisierung:

E(AU∗B) = µZ.(B ∨ (A ∧ EXZ))

• Damit kann E(AU∗B)I berechnet werden durch Aufruf der Fixpunkt-Prozedur lp wie folgt:

lp(µZ.(B ∨ (A ∧ EXZ)), ∅)

• Wie implementiert man die Funktion r = λZ.(B ∨ (A ∧ EXZ))?

• Fur eine gegebene Kripke-Struktur I soll r(Z) die folgende Mengeberechnen:

s : es gibt s′ s und s′ ∈ (BI ∪ (AI ∩ Z))

• Das entspricht dem Schema: s : ∃s′(φ(s′) ∧ ψ(s, s′))

179


BDD-Berechnung eines relationalen Produkts ∃~w(φ(~v) ∧ ψ(~v, ~w):Gegeben ein OBBD δ1 fur das Pradikat φ mit Variablen v1, . . . , vn und einOBBD δ2 fur ψ mit Variablen v1, . . . , vn, w1, . . . , wn

1. Umbenennung aller Variablen vi in δ1 in wi ergibt δ′12. Schnitt von δ′1 mit δ2: δ3 = BDD-apply(∧, δ′1, δ2)3.

”Loschung“ aller Variablen V = w1, . . . , wn aus δ3: δ = BDD-

exists(V, δ3)

Es gibt Verfahren BDD-relprod(BDD(φ),BDD(ψ)) mit linearer Komplexitat

Die Prozedur checkEG∗:

• Die Berechnung von checkEG∗(check(B)) basiert auf

E(AU∗B) = µZ.(B ∨ (A ∧ EXZ))

und kann durch folgenden Aufruf von lp berechnet werden:

lp(µZ.(B ∨ (A ∧ EXZ)),U)

180

156BDD-Reprasentation reaktiver Systeme

• Gegeben eine Beschreibung eines reaktiven Systems bestehend aus Kom-ponenten

• Problem der Zustandsexplosion bei expliziter Reprasentation der globalenSystemzustande und -transitionen als Kripke-Struktur

• Explizite Kripke-Struktur ist zu groß und kann nicht erzeugt werden

• ⇒ BDD-Reprasentation des Systems aus Kripke-Struktur funktioniertnicht

• ⇒ BDD-Reprasentation der Kripke-Struktur muss direkt aus einer kom-pakteren Reprasentation des Systems erzeugt werden

• Ansatz: Arbeiten auf”Transitions-logischer“ Reprasentation des reaktiven

Systems

181


Synchrone oder asynchrone Modellierung

• Gegeben ein System interagierender Komponenten

• Jede Komponente i hat Zustandsvariablen Vi, die o.B.d.A. BoolescheWerte annehmen konnen

• Zwei Modelle zur diskreten Modellierung des Verhaltens des Gesamtsy-stems:

– Der Wechsel der Werte der Zustandsvariablen wird durch einen Taktsynchronisiert, d.h. alle Komponenten andern die Werte ihrer Zu-standsvariablen simultan

– In jedem Schritt andern sich die Werte lediglich einer Komponente(Interleaving-Semantik)

• Verschiedene Modelle der Interaktion/Kommunikation:

– Uber gemeinsame Variablen– Durch Austausch von Nachrichten (mittels Warteschlangen oder Pro-

tokollen)

182

158Synchrone Modellierung reaktiver Systeme

Am Beispiel digitaler Schaltungen

• Beispiel: Synchroner Modulo-8-Zahler

• Das System hat drei Eingabeeinheiten, deren Werte sich in jedem Schrittandern, und die Schaltung stabilisiert sich. Dann erfolgt ein Taktpuls unddie Einheiten andern ihre Werte.

• Die Modellierung des System erfolgt mittels dreier Boolescher Zustands-variablen: V = v1, v2, v3• Die Systemubergange konnen beschrieben werden durch Verwendung

einer Menge V ′ = v′1, v′2, v′3 von Output-Variablen, fur die gilt:

v′1 = ¬v1

v′2 = v1 ⊕ v2

v′3 = (v1 ∧ v2)⊕ v3

wobei p⊕ q (exklusives oder) := p↔ ¬q

183

159Asynchrone Modellierung reaktiver Systeme

Am Beispiel asynchroner Schaltungen

• Sei vereinfachend angenommen, dass Komponenten genau einen Ausga-bewert und keine

”internen“ Zustandsvariablen haben

• ⇒ jede Komponente i kann durch eine Funktion fi(V ) beschriebenwerden

• Grundannahme der Interleaving-Semantik ist, dass sich in jedem Schrittgenau eine Komponente andert

• Damit ergibt sich die Transitionsrelation des Gesamtsystems als Disjunk-tion der individuellen Transitionsrelationen:

R(V, V ′) = R1(V, V ′) ∨ · · · ∨Rn(V, V ′)

wobei Ri(V, V ′) ≡ (v′i ↔ fi(V )) ∧∧j 6= i(v′j ↔ vj)

184

160Synchrones vs. asynchrones Verhalten

Am Beispiel digitaler Schaltungen

• Sei eine Schaltung gegeben mit einer Menge von ZustandsvariablenV = v1, v2 und gleichen Ubergangsfunktionen f1 und f2, d.h.

v′1 ≡ f1(V ) = v1 ⊕ v2

v′2 ≡ f2(V ) = v1 ⊕ v2

• Sei s ein Zustand mit v1 = 1 und v2 = 1

• Im synchronen Modell hat s genau einen Folgezustand s′, wobei

v1 = 0 und v2 = 0

• Im asynchronen Modell hat s zwei Folgezustande s1 und s2, wobei

in s1 : v1 = 0 und v2 = 1in s2 : v1 = 1 und v2 = 0

185

161Fairness in asynchronen Systemen

• In Interleaving-Modell ist es prinzipiell moglich, dass sich bestimmteKomponenten niemals andern. Um diese unwahrscheinlichen oder un-erwunschten Systemablaufe auszuschließen, ist es ublich zusatzliche sog.Fairness-Bedingungen zu verlangen.

• Solche Fairness-Bedingungen konnen direkt in CTL∗, aber nicht in CTLformuliert werden.

• Um Fairness in CTL einzubetten ohne die komplexitatstheoretischenVorteile zu verlieren, andert man die Semantik von CTL.

• Eine Fairness-Bedingung ist eine Menge von Zustanden. Eine faire Kripke-Struktur ist ein Quadrupel 〈U ,≺, ι,F〉, wobei 〈U ,≺, ι〉 eine Kripke-Struktur ist und F ⊆ 2U .

• Ein maximaler Berechnungspfad P ist fair bzgl. einer Menge F vonFairness-Bedingungen, wenn P entweder endlich ist oder jedes Fi ∈ Feinen Zustand enthalt, der unendlich oft in P vorkommt.

• Die Model Checking-Verfahren fur CTL lassen sich an die faire Semantikanpassen bei gleicher Effizienz.

186

162Model Checking und Automatentheorie

Probleme des Model Checking konnen automatentheoretisch refor-muliert und gelost werden

• Sowohl Kripke-Modelle als auch temporallogische Formeln konnen inbestimmte endliche Automaten ubersetzt werden unter Beibehaltungfolgender Eigenschaft:

– Ein Kripke-Modell erfullt eine Formel gdw jedes Wort, das vom Modell-Automaten akzeptiert wird, vom Formel-Automaten akzeptiert wird

• Das Model Checking-Problem reduziert sich dann auf die Uberprufung,ob die Sprache des Modell-Automaten eine Teilmenge der Sprache desFormel-Automaten ist

• Vorteile:

– Uniformer Ansatz– Ermoglicht Anwendung effizienter automatentheoretischer Methoden

und -algorithmen– Modell-Automat kann inkrementell generiert werden

187

163Endliche Automaten

• Endlicher Automat: 〈Σ, S,≺, S0, Sa〉 wobei

– Σ eine endliche Menge, das Alphabet– S eine endliche Menge, die Zustande– ≺⊆ S × Σ× S, die Transitionsrelation– S0 ⊆ S, die Menge der Anfangszustande– Sa ⊆ S, die Menge der akzeptierenden Zustande

• Lauf eines endlichen Automaten angesetzt auf ein endliches Wort w ∈ Σ∗,Akzeptanz eines Wortes, Sprache eines endlichen Automaten, etc. wieublich definiert

• Sprache eines endlichen Automaten durch regulare Ausdrucke beschreib-bar und umgekehrt

• Sprache der regularen Ausdrucke

A := ε | a | (A.A) | (A+A) | A∗

wobei ε leeres Wort und a ∈ Σ

188

164Automaten auf unendlichen Wortern

• Zur Erfassung beliebiger maximaler Pfade Erweiterung auf sog. ω-Automaten, die auf unendlichen Wortern w ∈ Σω arbeiten

• Im folgenden ausschließliche Beschrankung auf unendliche Worter (Si-mulation beliebiger, auch endlicher maximaler Pfade durch Einfuhrungspezieller Zustandsschleifen moglich)

• Buchi-Automat: wie endlicher Automat, aber Akzeptanzbedingung wiefolgt definiert:

Ein Buchi-Automat akzeptiert ein ω-Wort w gdw es einen Lauf desAutomaten angesetzt auf w gibt, in dem ein Zustand s ∈ Sa unendlichoft vorkommt

• Sprache eines Buchi-Automaten durch sog. ω-regulare Ausdrucke be-schreibbar und umgekehrt

• Sprache der ω-regularen Ausdrucke

ωA := ε | a | (A.A) | (A+A) | A∗ | Aω

189

165Beipiele fur Automaten und ihre akzeptierten Worter

• Gegeben der Automat mit

– Σ = a, b– S = q1, q2– ≺ = 〈q1, a, q1〉, 〈q1, b, q2〉, 〈q2, a, q1〉, 〈q2, b, q2〉– S0 = q1– Sa = q1

• Sprache des Automaten als endlicher Automat:

(ε+ ((a+ b)∗.a))

• Sprache des Automaten als Buchi-Automat:

(b∗.a)ω

190

166Eigenschaften von Buchi-Automaten

• Die Klasse der Buchi-Automaten (der akzeptierten Sprachen) ist ab-geschlossen unter Vereinigung, Schnitt, Projektion und Komplementbil-dung.

– Schnitt: Bildung des Produktes der Automaten– Vereinigung und Projektion ebenfalls einfach– Komplementbildung: Im worst-case exponentielles Anwachsen der Zu-

standsmenge (Ω(2n logn))

• Deterministische Buchi-Automaten: ≺ : S × Σ → S; haben geringereAusdrucksstarke als nichtdeterministische (Gegenbeispiel: Sprache allerω-Worter uber Σ = a, b, die nur endlich oft a enthalten)

• Leerheit der Sprache leicht zu entscheiden:

– Prufe, ob ≺ eine stark konnektierten Komponente hat, die vom An-fangszustand aus erreichbar ist und einen akzeptierenden Zustandenthalt

– Komplexitat: in linearer Zeit entscheidbar, sogar auf nichtdeterministi-schem logarithmischem Platz (NLOGSPACE)

191

167Von LTL-Formeln zu Buchi-Automaten

• Gegeben eine LTL(P)-Formel φ

• In der Folgensemantik kann φ aufgefasst werden als die Menge M derunendlichen naturlichen Modelle (unendlichen Pfade) Is, die φ erfullen,d.h. fur die gilt: Is |= φ

• Jedes Element in M kann als ω-Wort uber dem Alphabet Σ = 2P

interpretiert werden

• Dann gibt es einen Buchi-Automaten B, dessen Sprache L(B) die Mengeder M entsprechenden ω-Worter ist.

• Umgekehrt gibt es nicht zu jedem Buchi-Automaten eine entsprechendeFormel in der Temporallogik LTL

• Buchi-Automaten entsprechen den ausdrucksstarkeren TemporallogikenµTL, qTL und der monadischen Logik zweiter Stufe, die alle beschrankteFormen der Quantifikation erlauben

192

168Von LTL-Formeln zu Buchi-Automaten

• Jede aussagenlogische Formel F uber einer Menge von Variablen Plasst sich in einen ω-regularen Ausdruck der Form α1 + · · · + αn mitαi ∈ Σ = 2P ubersetzen und umgekehrt, wobei die αi genau dieBelegungen kodieren, die F erfullen.

• Beispiele (sei P = p, q und damit Σ = ∅, p, q, p, q):

– ¬p ∨ q = ∅+ q+ p, q– ¬p ∧ q = q– > = ∅+ p+ q+ p, q– ⊥ = ε

• Damit lassen sich logische Formeln als Abkurzungen fur ω-regulareAusdrucke der Form α1 + · · ·+ αn mit αi ∈ Σ = 2P verwenden

• Die Ubersetzung lasst sich auf LTL-Operatoren ausdehnen

• Die LTL-Formel G∗(¬p ∧ X>) ∨ G∗F+q entspricht dem ω-regularenAusdruck (¬p)ω + (>.>∗.q)ω

193

169Model Checking und Automaten

Modellierung reaktiver Systeme durch Automaten

• Zustande des modellierten Systems konnen durch das Alphabet oder dieinternen Zustande eines Automaten modelliert werden

• Vorteile des Ansatzes: Modelliertes System und Systemeigenschaft (tem-porale Formel) konnen in derselben Weise modelliert werden

• Gegeben ein Kripke-ModellM = 〈U ,≺M, ι, s0〉 fur eine aussagenlogischeSprache P• Abbildung in einen Buchi-Automaten BM z.B. wie folgt:

– Σ = 2P

– S = U– 〈s, α, s′〉 ∈ ≺ gdw s ≺M s′ und α = p ∈ P : s′ ∈ ι(p)– S0 = s0– Sa = S

194

170Model Checking und Automaten

Model Checking mittels Automaten

• Gegeben Spezifikation eines Kripke-Modells M als Buchi-Automat BMund eine LTL-Formel φ

• Spezifikation der intendierten temporallogischen Eigenschaft φ als weite-rer Buchi-Automat Bφ uber demselben Alphabet

• Es gilt: M |=s φ gdw L(BM) ⊆ L(Bφ)

• Prufe ob L(BM) ⊆ L(Bφ)

• Indirekter Ansatz:

– Erzeugung des Buchi-Automaten B¬φ– Bildung des Produktautomaten BP = BM · B¬φ– Es gilt: M |=s φ gdw L(BP ) = ∅– Prufe ob L(BP ) = ∅

195

171Reduktion durch partielle Ordnungen

• Explosion des Zustandsraumes wird zum Teil verursacht durch nebenlaufi-ges Verhalten der Komponenten des reaktiven Systems

• Asynchrones Verhalten wird typischerweise durch Interleaving modelliert(in jedem Schritt andert sich genau eine Komponente)

• Unabhangige Ablaufe konnen viele verschiedene Interleavings haben

• In vielen Fallen ist es nicht notig, alle Interleavings zu betrachten

• Ansatz der Methoden partieller Ordnungen: Betrachtung einer reprasen-tativen Interleaving-Folge fur die gerade betrachtete Temporalformel

• D.h. echte Nebenlaufigkeit wird nicht modelliert und die Logik wird nichterweitert um partielle Ordnungen zu erfassen, sondern die Effizienz desModel Checking wird verbessert fur die erfassbaren Anwendungsfalle

• Wichtige Voraussetzung: Invarianz unter sog. Stottern (gilt fur LTLohne X)

196

172Weitere Techniken

• Beschranktes Model Checking:

Ubersetzung des Model Checking-Problems in eine Folge rein aussagen-logischer Probleme (fur jede zu untersuchende Pfadlange)

• Abstraktionen

• Symmetrien

• Kombination von Model Checking und Theorembeweisen

197

Was ist Model Checking? 1 - LMU, Informatik, TCS · Model checking is an automatic technique for...

Documents

Transcript of Was ist Model Checking? 1 - LMU, Informatik, TCS · Model checking is an automatic technique for...