6) Baumzeit-Temporallogik · GPS: Baumzeit-Temporallogik — CTL und Bisimilarit¨at 241 CTL ist...

6) Baumzeit-Temporallogik

GPS: Baumzeit-Temporallogik — Syntax und Semantik von CTL 236

Motivation

zur Erinnerung: Linearzeit-Eigenschaften konnen trace-aquivalenteModelle nicht unterscheiden

Trace-Aquivalenz schwacher als “Verhaltens-Aquivalenz”(Bisimulation)

in Baumzeit-Logiken:

• Zukunft nicht ein fur alle Male determiniert, sondern ergibtsich in jedem Schritt neu

• Aussagen uber Existenz von Momenten in der Zukunftmoglich

Primitive sind Zustande statt Traces


Computation Tree Logic CTL

Def. 6Syntax von CTL:

ϕ := q | ϕ ∧ ϕ | ¬ϕ | EXϕ | E(ϕ Uϕ) | EGϕ

wobei q ∈ AP.

temporale Operatoren X, U, G wie in LTL (X statt �)

jeweils zusammen mit Pfadquantor E, A


Beispiele

nutzliche Abkurzungen:

• EFϕ := E(true Uϕ) “irgendwo”

• AXϕ := ¬EX¬ϕ “auf allen Nachfolgern”

• A(ϕ Uψ) := ¬EG¬ψ ∧ ¬E�(¬ψ) U (¬ϕ ∧ ¬ψ)

�

• AGϕ := ¬EF¬ϕ “uberall”

Beispiele:

• AGAFq “auf allen Pfaden unendlich oft q”

• EGEFq nicht: “unendlich oft q auf einem Pfad”!

• AG(request → AFserve)

• . . .

GPS: Baumzeit-Temporallogik — CTL und Bisimilaritat 240

CTL und Trace-Aquivalenz

zur Erinnerung: zwei verschiedene Getranke-Automaten T1, T2

betrachte ϕ := EX�EXspezi ∧ EXmezzomix

�

es gilt:

• T1 |= ϕ

• T2 �|= ϕ

zur Erinnerung:

T1 ≡tr T2 gdw. fur alle ϕ ∈ LTL : T1 |= ϕ ⇔ T2 |= ϕ


CTL ist nicht weniger als LTL

aus obigem folgt sofort:

Thm. 8Es gibt CTL-definierbare Eigenschaften, die nicht LTL-definierbarsind.

Beweis: Betrachte obige Formel ϕ. Angenommen, es gabeLTL-Formel ψ mit ψ ≡ ϕ.

Betrachte ebenfalls Getranke-Automaten T1 und T2. Es giltT1 ≡tr T2 und somit

T1 |= ψ gdw. T2 |= ψ

Andererseits gilt aber T1 |= ϕ und T2 �|= ϕ. �


Induzierte Aquivalenz

Def. 8Sei L eine Logik fur LTS. Diese induziert Relation ≡L auf LTS wiefolgt.

T1 ≡L T2 gdw. ∀ϕ ∈ L : T1 |= ϕ ⇔ T2 |= ϕ

Lemma: ≡L ist Aquivalenzrelation

es gilt: ≡tr = ≡LTL

gilt vielleicht auch ∼ = ≡CTL?


CTL und Bisimilaritat

Def. T = (S ,−→, I , L) endlich-verzweigend, falls∀s ∈ S : |Post(s)| < ∞

Thm. 9Fur alle T1, T2 gilt:

a) wenn T1 ∼ T2, dann T1 ≡CTL T2b) wenn T1 ≡CTL T2 und T1, T2 endlich-verzweigend, dann

T1 ∼ T2

Beweis: (a) Ubung.

(b) Betrachte die RelationR = {(s, t) | ∀ϕ ∈ CTL : s |= ϕ ⇔ t |= ϕ}. Man uberprufe, dasses sich dabei um eine Bisimulation handelt, solange diese Zustandejeweils nur endlich viele Nachfolger haben. �

GPS: Baumzeit-Temporallogik — Model Checking 244

Model-Checking fur CTL

sei T = (S ,−→, I , L) totales LTS

MC(ϕ) =case ϕ of

q : {s ∈ S | q ∈ L(s)}ψ1 ∧ ψ2 : MC(ψ1) ∩ MC(ψ2)

¬ψ : S\ MC(ψ)

EXψ : let T = MC(ψ) in Pre(T )

E(ψ1 Uψ2) : let T1 = MC(ψ1) in

let T2 = MC(ψ2) in MCEU(T1,T2)

EGψ : let T = MC(ψ) in MCEG(T )


Model-Checking fur Until-Formeln

Abwicklung einer CTL-Until-Formel ahnlich wie bei LTL, jedochPfadquantifizierung beachten!

E(ϕ Uψ) ≡ ψ ∨ (ϕ ∧ EXE(ϕ Uψ))

wieder: keine unendlichen Abwicklungen erlaubt!

MCEU(T1,T2) =T := T2

T � := ∅while T � �= T do

T � := TT := T ∪ (T1 ∩ Pre(T ))

return T


Korrektheit der EU-Berechnung

Def.: schreibe [[ϕ]] fur {s | T , s |= ϕ} wenn zugrundeliegendes LTST bekannt ist

Lemma 10

Sei T = (S ,−→, I , L) LTS, ϕ,ψ ∈ CTL, Tϕ,Tψ ⊆ S mit Tx = [[x ]]fur x ∈ {ϕ,ψ}. Dann gilt:

MCEU(Tϕ,Tψ) = [[E(ϕ Uψ)]]


MCEU ist korrekt

Beweis: “⊆” Sei s ∈ MCEU(Tϕ,Tψ). Wir zeigen s |= E(ϕ Uψ) perInduktion uber Anzahl k der (angefangenen) Durchlaufe derwhile-Schleife, bevor s ∈ T gilt. Beachte Monotonie in T !

Fall k = 0. Dann gilt s ∈ Tψ, also s |= ψ und somit auchs |= E(ϕ Uψ).

Fall k > 0. Dann wird s zu T hinzugefugt, weil gilt:

1 s ∈ Tϕ und somit s |= ϕ, und

2 es gibt t ∈ T mit s ∈ Pre(T ).

Beachte: Hypothese kann auf t angewandt werden und liefertt |= E(ϕ Uψ). Dann gilt aber auch s |= E(ϕ Uψ).


MCEU ist vollstandig

“⊇” Angenommen s |= E(ϕ Uψ). Dann existieren s0, s1, . . . undk ∈ N mit

1 s0 = s,

2 si ∈ Pre(si+1) fur alle i ∈ N,3 sk ∈ Tψ,

4 si ∈ Tϕ fur i = 0, . . . , k − 1,

5 si �= sj fur 0 ≤ i < j ≤ k .

Dann gilt fur i = 0, . . . , k : nach i Iterationen der while-Schleifeenthalt T den Zustand sk−i . Bedingung (5) sorgt dafur, dassMCEU mindestens k Schleifendurchlaufe ausfuhrt. �


Model Checking fur Generally-Formeln

Abwicklung: EGϕ ≡ ϕ ∧ EXEGϕ

hier aber großte Losung! (kleinste Losung ist false)

soll heißen: unendliches Abwickeln ok (sogar notwendig) umErfulltheit zu zeigen

MCEG(T1) =T := T1

T � := Swhile T � �= T do

T � := TT := T ∩ Pre(T )

return T

beachte: Variable T enthalt, vor i-ter Iteration, alle Zustande, vondenen Pfad der Lange i durch T1 ausgeht


Die Komplexitat des Model-Checking fur CTL

Prop. 11

Sei T totales, endliches LTS mit n Transitionen, ϕ ∈ CTL. MC (ϕ)kann darauf in Zeit O(n · |ϕ|) berechnet werden.

Beweisskizze:

• Rekursion uber Formelaufbau

• jede Klausel im Algorithmus kann in Zeit O(|−→ |) berechnetwerden

• dynamisches Programmieren, um maximal O(|ϕ|) vieleAufrufe zu haben

zum Vergleich: LTL-Model-Checking in O(n · |ϕ| · 22|ϕ|)


CTL vs. LTL: Ausdrucksstarke

geringere Model-Checking-Komplexitat hat ihren Preis: Fairnessz.B. nicht ausdruckbar

Prop. 12

Es gibt keine CTL-Formel ϕ, so dass fur alle T : T |= ϕ gdw. eseinen Trace gibt, auf dem unendlich oft q gilt.

Kor. 13CTL und LTL sind unvergleichbar bzgl. Ausdrucksstarke.


CTL vs. LTL: Komplexitat

Crash-Kurs “Komplexitatstheorie”:

NLOGSPACE PNP

coNPPSPACE EXPTIME⊆ ⊆

⊆⊆⊆

⊆

LTL Model CheckingCTL Model Checking

LTL Erfullbarkeit

CTL Erfullbarkeit

LTL M.C. mit fester Formel

CTL M.C. mit fester Formel

alle Probleme jeweils vollstandig

GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 253

State-Space Explosion

zur Erinnerung:

• paralleles Produkt aus n Komponenten hat i.A. exp(n) vieleZustande

• Schaltkreis uber n Bits hat i.A. 2n viele Zustande

bisher vorgestellte LTL- und CTL-Model-Checking-Algorithmensind explizit: Transitionssystem muss als solches vorliegen

gibt es Moglichkeiten, den Aufbau exponentiell großerTransitionssysteme zur Verifikation zu verhindern?

• on-the-fly Model-Checking

• symbolisches Model-Checking


On-the-fly Model-Checking

auch lokales Model Checking genannt (im Gegensatz zu globalem)

Idee:

• fur Programmverifikation interessant: erfullen Initialzustandegegebene Formel?

• oben vorgestellter Model-Checker fur CTL berechnet dies aberfur alle Zustande

• Ansatz: top-down, Formel steuert Suche durch dasTransitionssystem

• Transitionssystem wird (z.B. uber Semantik-Regeln) nur nachBedarf aufgebaut

fur CTL moglich, aber nicht trivial

fur LTL einfach: Produkt aus Transitionssystem und Buchi-Automat kann wahrend der Tiefensuche aufgebaut werden


Symbolisches Model Checking

symbolisch = Transitionssysteme nicht mehr explizit reprasentiert

Was soll das heißen? Egal. Bessere Frage: Algorithmus MC arbeitetmit Zustandsmengen; welche Operationen mussen aufReprasentationsform fur solche Mengen moglich sein, damitAlgorithmus MC seine Menge entsprechend reprasentieren kann?

• Durchschnitt, Komplement, Vereinigung

• Vorganger

• Ungleichheitstest

• nochmal Durchschnitt fur Frage, ob Initialzustande gegebeneFormel erfullen

• Menge der Initialzustande und Menge aller Zustande, diebestimmtes q ∈ AP erfullen, mussen entsprechendreprasentierbar sein


Binare Entscheidungsdiagramme

im folgenden sei V immer eine total geordnete Menge boolescherVariablen

Ordnung oft einfach implizit gegeben, z.B. durch Indizierung{x1, x2, . . . , xn}

Def. 9

Ein BDD uber Variablenmenge V = {x1, . . . , xn} ist DAG mit . . . .

• zwei Endknoten 0 und 1 ohne Nachfolger,• jeder Knoten außer 0 und 1

• ist beschriftet mit einer Variablen aus V,• hat genau zwei verschiedene Nachfolger, erreichbar uber eine

0- und 1-Kante,

• jeder Pfad von beliebigem Knoten zu Endknoten respektiertdie Ordnung auf den Variablen.


BDDs: Beispiel


Die Semantik eines BDDsjedem Knoten v in einem BDD wird induktiv eine Funktionfv : V → {0, 1} zugeordnet (hier reprasentiert als boolescheFormel)

Induktionsanfang, Endknoten:

f0 := 0 f1 := 1

Induktionsschritt: Sei v Nicht-Endknoten mit

• Knotenbeschriftung x

• 0-Nachfolger w0

• 1-Nachfolger w1

nach Voraussetzung ist wi jeweils fwizugeordnet

fv := (¬x ∧ fw0) ∨ (x ∧ fw1)


Reduzierte BDDs

Def. 10Ein BDD heißt reduziert, falls fur alle Knoten v ,w gilt: wennv �= w, dann fv �= fw .

Lemma 14

Fur jede Funktion f : V → {0, 1} existiert ein reduzierter BDD mitKnoten v, so dass f = fv .

Beweis: (1) BDD fur f laßt sich mithilfe der Shannon-Expansionaufbauen.

f (x1, . . . , xn) =�¬x1 ∧ f (0, x2, . . . , xn)

�∨�x1 ∧ f (1, x2, . . . , xn)

�

Wahle Variablen sukzessive und ubersetze rechte Seite inBDD-Knoten. Beachte Variablenordnung!(2) BDD schrittweise reduzieren. �


Eindeutigkeit

Kor. 15

Seien f1, f2 : V → {0, 1} und v1, v2 Knoten in reduziertem BDDmit f1 = fv1 und f2 = fv2 . Dann gilt:

f1 = f2 gdw. v1 = v2

soll heißen: reprasentiert man mehrere Funktionen in einemeinzigen reduzierten BDD, so ist Funktionengleichheit in O(1)testbar!

ab jetzt: alle BDDs reduziert


Operationen auf BDDs

Thm. 16

Seien x = {x1, . . . , xn} und f1, f2 : x → {0, 1} durch BDDs v1, v2reprasentiert. Dann lassen sich BDDs w berechnen, so dass

a) fw (x) = ¬f1(x) (Komplement)

b) fw (x1, . . . , xi−1, xi+1, . . . , xn) = f1(x1, . . . , xi−1, c , xi+1, . . . , xn)fur i ∈ {1, . . . , n}, c ∈ {0, 1} (Projektion)

c) fw (y1, . . . , yn) = f1(x)[y1/x1, . . . , yn/xn] (Var.-Umbenennung)

d) fw (x) = f1(x) ∨ f2(x) (Disjunktion)

e) fw (x) = f1(x) ∧ f2(x) (Konjunktion)

f) fw (x1, . . . , xi−1, xi+1, . . . , xn) = 1 gdw. es c ∈ {0, 1} gibt, sodass f1(x1, . . . , xi−1, c , xi+1, . . . , xn) = 1 fur i ∈ {1, . . . , n}

(∃-Quantifikation)


Komplement, Projektion, Umbenennung

Beweis: (Komplement) Vertauschung der 0- und 1-Knotenunterhalb von v1.

(Projektion) Losche unterhalb von v1 jeden Knoten, der mit xibeschriftet ist. Eingehende Kanten werden an deren c-Nachfolgerweitergeleitet.

(Umbenennung) Durch Umbennung der Knotenbeschriftungen.


Disjunktion

(Disjunktion) Durch Induktion uber Anzahl der Variablen in denBDDs unterhalb von v1 und v2. Induktionsanfang: Einer der beidenist 0 oder 1. Klar.

Induktionsschritt. Seien {xi , . . . , xn} die noch unterhalb von v1oder v2 vorkommenden Variablen. Dann benutze zunachstShannon-Expansion.

(f1 ∨ f2)(xi , . . . , xn) =�xi ∧

�f1(1, xi+1, . . . , xn) ∨ f2(1, xi+1, . . . , xn)

��

∨�¬xi ∧

�f1(0, xi+1, . . . , xn) ∨ f2(0, xi+1, . . . , xn)

��

Somit:1 Beachte: fj(c , xi+1, . . . , xn) ist lediglich der c-Nachfolger von

vj fur c ∈ {0, 1} und j ∈ {1, 2}.2 Berechne f1(c , . . .) ∨ f2(c , . . .) rekursiv fur c ∈ {0, 1}.3 Setze diese nach ublicher Vorschrift mit neuem Knoten fur xi

zusammen.


Konjunktion, Quantifikation

(Konjunktion) Analog zur Disjunktion.

(∃-Quantifikation) Mithilfe von Projektion und Disjunktion wegen

∃xi .f1(x) = f1(x1, . . . , xi−1, 0, xi+1, . . . , xn)∨f1(x1, . . . , xi−1, 1, xi+1, . . . , xn)

�

klar: weitere Operationen (∀-Quantifikation, Implikation, etc.)ebenfalls moglich

worst-case fur alle Operationen linear in Große des entstehendenBDDs


Symbolische Reprasentationen von LTS

sei n ∈ N, T = (S ,−→, I , L) LTS uber AP mit S = {0, . . . , 2n − 1}

wahle Variablen x = (x0, . . . , xn−1) und y = (y0, . . . , yn−1)

Zustand i binar kodierbar als enc(i)

T lasst sich symbolisch reprasentieren durch |AP |+ 2 boolescheFunktionen bzw. BDDs

• 1 BDD ftr (x , y) mit

ftrans(enc(i), enc(j)) = 1 gdw. i −→ j

• 1 BDD finit(x) mit

finit(enc) = 1 gdw. i ∈ I

• je ein BDD fq fur jedes q ∈ AP mit

fq(enc(i)) = 1 gdw. q ∈ L(i)


Wahl der richtigen Variablenordnung

Große der BDD-Reprasentation hangt oft von Variablenordnung ab

Bsp.: Man konstruiere den BDD fur die Transitionsrelation in

0 1 2 2n−1. . .

jeweils fur Variablenordnung

• x0, . . . , xn−1, y0, . . . , yn−1

• y0, . . . , yn−1, x0, . . . , xn−1

• xn−1, . . . , x0, yn−1, . . . , y0

• x0, y0, . . . , xn−1, yn−1

• xn−1, yn−1, . . . , x0, y0


Symbolisches Model Checking

CTL-Model-Checking kann auf BDDs ausgefuhrt werden

MC(ϕ) berechnet BDD (uber x0, . . . , xn−1 z.B.), der {s | s |= ϕ}kodiert; MCEU und MCEG dementsprechend

MC(ϕ) =case ϕ of

q : fq

ψ1 ∧ ψ2 : MC(ψ1) ∧ MC(ψ2)

¬ψ : ¬ MC(ψ)

EXψ : ∃y0 . . . ∃yn−1.ftr ∧ MC(ψ)[y0/x0, . . . , yn−1/xn−1]

E(ψ1 Uψ2) : let f1 = MC(ψ1) in

let f2 = MC(ψ2) in MCEU(f1, f2)

EGψ : let f = MC(ψ) in MCEG(f )

6) Baumzeit-Temporallogik · GPS: Baumzeit-Temporallogik — CTL und Bisimilarit¨at 241 CTL ist...

Documents

Transcript of 6) Baumzeit-Temporallogik · GPS: Baumzeit-Temporallogik — CTL und Bisimilarit¨at 241 CTL ist...