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
GPS: Baumzeit-Temporallogik — Syntax und Semantik von CTL 237
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
GPS: Baumzeit-Temporallogik — Syntax und Semantik von CTL 238
Semantik von CTL
Def. 7
Sei T = (S ,−→, I , L) totales LTS.
T , s |= q gdw. q ∈ L(s)
T , s |= ϕ ∧ ψ gdw. T , s |= ϕ und T , s |= ψ
T , s |= ¬ϕ gdw. T , s �|= ϕ
T , s |= EXϕ gdw. es gibt t ∈ S mit s −→ t und T , t |= ϕ
T , s |= E(ϕ Uψ) gdw. es gibt Pfad s0s1 . . . mit s0 = s
und es gibt k ∈ N mit T , sk |= ψ
und fur alle j < k : T , sj |= ϕ
T , s |= EGϕ gdw. es gibt Pfad s0s1 . . . mit s0 = s
und fur alle k ∈ N : T , sk |= ϕ
T |= ϕ gdw. fur alle s ∈ I : T , s |= ϕ
GPS: Baumzeit-Temporallogik — Syntax und Semantik von CTL 239
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 |= ϕ
GPS: Baumzeit-Temporallogik — CTL und Bisimilaritat 241
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 �|= ϕ. �
GPS: Baumzeit-Temporallogik — CTL und Bisimilaritat 242
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?
GPS: Baumzeit-Temporallogik — CTL und Bisimilaritat 243
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 )
GPS: Baumzeit-Temporallogik — Model Checking 245
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
GPS: Baumzeit-Temporallogik — Model Checking 246
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ψ)]]
GPS: Baumzeit-Temporallogik — Model Checking 247
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ψ).
GPS: Baumzeit-Temporallogik — Model Checking 248
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. �
GPS: Baumzeit-Temporallogik — Model Checking 249
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
GPS: Baumzeit-Temporallogik — Model Checking 250
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|ϕ|)
GPS: Baumzeit-Temporallogik — Model Checking 251
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.
GPS: Baumzeit-Temporallogik — Model Checking 252
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
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 254
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
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 255
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
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 256
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.
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 257
BDDs: Beispiel
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 258
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)
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 259
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. �
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 260
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
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 261
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)
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 262
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.
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 263
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.
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 264
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
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 265
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)
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 266
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
GPS: Baumzeit-Temporallogik — Symbolisches Model Checking 267
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 )
Top Related