1

Computergestützte Verifikation

26.4.2002

2

CTL*

CTL*

LTL CTL

nur Pfad-formeln

Nur Zust.-formeln

X, F, G, U X, F, G, U,A, E

EX, AX,EF, AF,EG, AG,E( . U . )A( . U . )

3

Lösung: Fairnessannahmen

Eine Fairnessannahme ist eine Pfadeigenschaft undBestandteil der Systembeschreibung.

Gültigkeit unter Fairness:A = für jeden Pfad, der alle Fairnessannahmen erfüllt, gilt....E = es gibt einen Pfad, der alle Fairnessannahmen erfüllt und ...

Fairness

aktionsbasiert zustandsbasiert

4

Wie geht es weiter?

System Abstraktion

Spezifikation

Simulation

Formalisierung

Model Checker

Gegenbeispiel

Modell

log. Formel

+

-

VerfeinerungFehler-beseitigung

Präzisierung

Überlauf

A) Finite state systems B) Infinite state systems

5

Model Checking für finite state systems

explizit: symbolisch:

3.1: Tiefensuche

3.2: LTL-Model Checking

3.3: CTL-Model Checking

3.5: Reduktion durch Symmetrie3.6: Partial Order Reduction

3.7: Tools

4.1: BDD-basiertes CTL-Model Checking

4.2: SAT-basiertes Model Checking

4.3: Tools

3.4: Fairness

Kapitel 3 Kapitel 4

6

Kriterium für Startknoten von SZK

0

3

26

1

5

4v.lowlink = MIN(v’.dfs | v’ von v erreichbar über beliebig vieleBaumkanten, gefolgt von max. eineranderen Kante [v,v’] mit v ~ v’)

0

1

1

3

4

44

Satz: v ist genau dann Startknoten einerSZK wenn v.lowlink = v.dfs

0

6

52

4

1

3

0

1 1

1

6

4

4

7

Tarjans AlgorithmusVAR Tarj: Stack von Knoten, maxdfs: Nat, weiss: Knotenmengeweiss := V, maxdfs = 0; Tarj := empty stackdfs(v0);

dfs(v): v.dfs = v.lowlink = maxdfs; maxdfs += 1;push(v,Tarj);weiss := weiss \ {v}FOR ALL v’ ([v,v’] in E) DO

IF v’ in weiss THENdfs(v’)v.lowlink = MIN(v.lowlink,v’.lowlink)

ELSEIF v’ on Tarj THEN

v.lowlink = MIN(v.lowlink,v’.dfs)END

ENDENDIF v.lowlink = v.dfs THEN

REPEATv* = pop(Tarj)

UNTIL v = v*END

eine SZK

Baumkante

andere Kante

8

3.2 LTL Model Checking

9

Grundidee

LTL-Eigenschaft Menge derjenigen Pfade, die erfüllen L

Transitionssystem Menge derjenigen Pfade, die in TS realisiert werden können

LTS

TS erfüllt genau dann, wenn jeder Pfad in TS erfüllt, d.h.

LTS L

10

Wie kann man Inklusion entscheiden?

LTS L

LTS L

LTS L¬

Agenda: 1. Automaten, die LTSund L¬

akzeptieren 2. Konstruktion eines Schnittautomaten 3. Entscheidung, ob Automat die leere Sprache akzeptiert

Problem: Wir reden über unendliche Sequenzen!

11

Büchi-Automaten

= endliche Automaten mit einem für unendliche Sequenzengeeigneten Akzeptierungskriterium

B = [X, Z, Z0, , F]

X – Alphabet Z – ZustandsmengeZ0 – Anfangszustandsmenge : Z x X 2Z

F = {F1,...,Fn}, Fi Z Akzeptierungsmengen

unendliche Sequenz in X

B akzeptiert: es ex. unendliche Sequenz = z0 z1 z2 ....- z0 Z0, zi+1 d(zi,xi), - Für jedes Fi F: enthält unendlich oft Elemente aus Fi

LB

12

Beispiele

X = {a,b,c}

A

C

B

a

a

a b

bb

cc

cZ0 = ZF1 = {A,B}F2 = {A,C}

LB = {| in unendlich oft a oder unendlich of b und c}

1

LB = {| nach jedem a in kommt irgendwann b}

2ab

b,c a,c

Z0 = {1}F1 = {1}

13

Transitionssystem und Büchi-Automat

Eine Menge Lvon unendlichen Sequenzen heißt regulär,wenn es einen endlichen Büchi-Automaten gibt, der L

akzeptiert.

Beobachtung: Jede Menge von Systemabläufen einesfinite state Transitionssystems ist regulär.

Z = S, Z0 = I, (z,x) =

, sonst

{z’ | [z,z’] E}, falls x den Wahrheitswerten der Aussagen in z entspricht

X = Vektoren von booleschen Werten, die als Wahrheits-werte der elementaren Aussagen interpretiert werden

F1 = Z, F = {F1}

14

Beispiele

(i,i,1)

(r,i,1) (i,r,1)

(r,r,1)(c,i,0) (i,c,0)

(c,r,0) (r,c,0)

g2

g1 g1’

g2’g1

g1

g1’

g1’

g3 g3’

g3’g3

g2’g2

g0,g0’

g0

g0

g0’

g0’

S: G (pc1 “critical” pc2 “critical” )

G (pc2 = “request” F pc2 = “critical”)

L: G (pc1 = “request” F pc1 = “critical”)

1.pc1 = crit2. pc2 = crit3. pc1 = req4. pc2 = req

15

Beispiele

(i,i,1)

(r,i,1) (i,r,1)

(r,r,1)(c,i,0) (i,c,0)

(c,r,0) (r,c,0)

FFWF

FFFF FFFF

FFFWFFFW

FWFF

FFWF

WFFF

WFFF FWFF

FWWFWFFW

FFWWFFWW

FFFF

FFFW

FWFF

FFWF

WFFF

1.pc1 = crit2. pc2 = crit3. pc1 = req4. pc2 = req

16

Büchi-Automaten und LTL

Satz: Zu jeder LTL-Formel gibt es einen Büchi-Automatenmit max 2Zuständen, der genau die unendlichenSequenzen akzeptiert, die erfüllen.

Beispiele:

X a2

0 12

3

*?W*

?F*

*

*Z0 = {0},F = { {2} }

F a2

0* 1

*

?W*

Z0 = {0},F = { {1} }

G a2

0?W*1

*

?F*

Z0 = {0},F = { {0} }

0 1

2

?W*

??W**

*

*

Z0 = {0},F = { {1} }

a2 U a3

17

Automaten für komplexe Formeln (Bsp)

0 11

0

2

?F*

?W*

??W*

*

G(a2 F a3)

Z0 = {0}F = {{0}}

*

*

?F*

??W**

(G F a2) (G F a3)

Z0 = {0}F = { {1,2} }

18

Zwischenfazit

Haben:-Büchi-Automat für LTS

-Büchi-Automat für L¬

Ziel: LTS L¬

nächster Schritt: geg: B1,B2

ges: B*: LB* = LB1 LB2

19

Produktautomat

B1 = [X,Z1,Z01,1,F1] B2 = [X,Z2,Z0

2,2,F2]

B* = [X,Z*,Z0*,*,F*]

Z* = Z1 x Z2 Z0* = Z01 x Z0

2

*([z,z’],x) = 1(z,x) x 2(z’,x)

F* = { F x Z2 | F F1} { Z1 x F | F F2}

Satz: LB* = LB1 LB2

Idee: beide Automaten arbeiten parallel, Akzeptierungs-mengen werden nebeneinandergestellt

20

BeispielB1:

0 1cba

W,F

W,F FW F

F

(a,0) (a,1)

(b,0) (b,1)

(c,0) (c,1)

WW

F F

F FF

F

B2:

Z0 = {0}F = { {1} }

Z0 = {a}

F = { {a,b,c} }

Z0 = {(a,0)} F = { Z, {(a,1),(b,1),(c,1)} }

B* :

21

Emptinessgeg.: Büchi-Automat B Frage LB = ?

“”: Sei Sequenz, die von B akzeptiert wird.Z* sei Menge der Zustände, die im akzeptierenden Laufunendlich oft durchlaufen werden. Z* ist stark zusammen-hängend, und enthält Elemente aus jeder Akzeptierungsmenge

“”: Konstruiere zur SZK eine Sequenz, die vom Initialzustandzur SZK gelangt, und dort zyklisch alle Zst. durchläuft. DieseSequenz ist offenbar in LB

Lösung: LB gdw. es gibt eine nichttriv. SZK in B (von einemInitialzustand erreichbar), die aus jeder AkzeptierungsmengeElemente enthält.

nichttriv. = mehrere Zst. oder 1 Zustand mit Schleife

22

LTL Model Checking

Geg.: TS (implizit), .

1. Konstruiere B¬

2. Konstruiere Produktautomat B* aus TS und B¬

3. Suche in B* nach SZK, die aus jeder Akzeptierungsmenge ein Element enthalten

4. gefunden “nein”, bilde Gegenbeispiel aus gefundener SZK

5. nicht gefunden “ja”

1 Schritt!

O(2|| |TS|)

23

BeispielG F a (negiert: F G ¬a)

cba W F

F

TS:

0 1W,F

W,F F

Z0 = {0}F = { {1} }

Z0 = {a}

F = { {a,b,c} }

(a,0) (a,1)

(b,0) (b,1)

(c,0) (c,1)

WW

F

F

F

FF

F

Z0 = {(a,0)} F = { Z, {(a,1),(b,1),(c,1)} }

B* : nur triv. SZK akzeptieren

also: Formel wahr

24

BeispielG F a (negiert: F G ¬a)

0 1cba

W,F

W,F FW F

F

(a,0) (a,1)

(b,0) (b,1)

(c,0) (c,1)

WW

F

F

F

FF

F

TS:

Z0 = {0}F = { {1} }

Z0 = {a}

F = { {a,b,c} }

Z0 = {(a,0)} F = { Z, {(a,1),(b,1),(c,1)} }

B* : nichttriv. SZK,

Formel falsch,

Gbsp: a (b c)*F F

F

F

25

On-The-Fly Verifikation

LTL-Formel wahr kompletter Produktautomat wird konstruiert

LTL-Formel falsch Konstruktion des Produktautomaten kann vorzeitig abgebrochen werden

weniger Speicherverbrauch

26

3.3 CTL Model Checking

Spezifisch für LTL: alle Formeln betreffen Pfade

Spezifisch für CTL: alle (Teil-)Formeln betreffen Zustände

Idee: - Jeder Zustand hat Liste mit Wahrheitswerten allerTeilformeln ( {W,F,?} ) L(s,)-Für die Wertberechnung werden Teilformeln jeweils alsatomar angesehen- Werte von Teilformeln werden bei Bedarf berechnet

27

RahmenprozedurCTL(s,)IF L(s,? THEN RETURN ENDCASE AP: berechne L(s,) END: CTL(s,) IF L(s,) THEN CTL(s,); L(s,) = L(s,); ELSE L(s,) = F END¬analogAX : FOR ALL s’: [s,s’] E DO

CTL(s’,); IF L(s’,) = F THEN L(s,) = F; RETURN; END END L(s,) = WEX : analog/* Fortsetzung folgt */

28

Rahmenprozedur (Fortsetzung)

(... CASE )

E( U ) : CheckEU(s,,);A( U ) : CheckAU(s,,);EF , AF ,EG ,AG : /* über Tautologien */

Also bleiben: CheckAU, CheckEU

29

CheckAU

s

CheckAU(s,,): Suche Gegenbeispiel

L(s’,) = W

L(s’,) = F

L(s’,A( U )) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,A( U ) = W

L(s’,A( U ) = F

30

CheckAU

s

CheckAU(s,,): Suche Gegenbeispiel

L(s’,) = W

L(s’,) = F

L(s’,A( U ) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,A( U )) = W

L(s’,A( U ) = Fs’

Keine Fortsetzung des Pfades kann Gegenbeispiel sein Backtracking von s’

31

CheckAU

s

CheckAU(s,,): Suche Gegenbeispiel

L(s’,) = W

L(s’,) = F

L(s’,A( U ) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,A( U )) = W

L(s’,A( U )) = F

s’

Gegenbeispiel gefunden L(s,A( U )) := F, RETURN

32

CheckAU

s

CheckAU(s,,): Suche Gegenbeispiel

L(s’,) = W

L(s’,) = F

L(s’,A( U ) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,A( U ) = W

L(s’,A( U ) = F

s’

Da jede Fortsetzung bei s’ U erfüllt, kann keine FortsetzungGegenbeispiel liefern Backtracking

33

CheckAU

s

CheckAU(s,,): Suche Gegenbeispiel

L(s’,) = W

L(s’,) = F

L(s’,A( U ) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,A( U ) = W

L(s’,A( U ) = F

s’

Gegenbeispiel gefunden ( = s....s’ + Gegenbeispiel bei s’) L(s,A( U )) = F, RETURN

34

CheckAU

s

CheckAU(s,,): Suche Gegenbeispiel

L(s’,) = W

L(s’,) = F

L(s’,A( U ) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,A( U ) = W

L(s’,A( U )) = F

Gegenbeispiel L(s, A( U ) = F, RETURN

35

CheckAU

s

CheckAU(s,,): Suche Gegenbeispiel

L(s’,) = W

L(s’,) = F

L(s’,A( U )) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,A( U ) = W

L(s’,A( U ) = F

Suchraum komplett durchsucht, ohne Gegenbeispiel L(s,A( U )) = W

36

CheckEU

s

CheckEU(s,,): Suche Zeugenpfad

L(s’,) = W

L(s’,) = F

L(s’,E( U )) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,E( U ) = W

L(s’,E( U ) = F

37

CheckEU

s

CheckEU(s,,): Suche Zeugenpfad

L(s’,) = W

L(s’,) = F

L(s’,E( U )) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,E( U ) = W

L(s’,E( U ) = Fs’

Zeuge gefunden L(s’,E( U )) = W, RETURN

38

CheckEU

s

CheckEU(s,,): Suche Zeugenpfad

L(s’,) = W

L(s’,) = F

L(s’,E( U )) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,E( U ) = W

L(s’,E( U ) = F

s’

keine Fortsetzung kann Zeuge sein Backtracking

39

CheckEU

s

CheckEU(s,,): Suche Zeugenpfad

L(s’,) = W

L(s’,) = F

L(s’,E( U )) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,E( U ) = W

L(s’,E( U ) = F

s’

Zeuge (= s....s’ + Zeuge bei s’) L(s’,E( U )) = W, RETURN

40

CheckEU

s

CheckEU(s,,): Suche Zeugenpfad

L(s’,) = W

L(s’,) = F

L(s’,E( U )) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,E( U ) = W

L(s’,E( U ) = F

s’

Keine Fortzsetung kann Zeuge sei Backtracking

41

CheckEU

s

CheckEU(s,,): Suche Zeugenpfad

L(s’,) = W

L(s’,) = F

L(s’,E( U )) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,E( U ) = W

L(s’,E( U ) = F

Suche komplett ohne Zeuge L(s’,E( U )) = F

42

Zwischenfazit CheckAU und CheckEU

L(s,A/E( U )) kann durch einfache Tiefensuche ermittelt werden

Das würde Laufzeit von O( || |TS| |TS| ) = O(|| |TS|2)liefern: Für jede Teilformel und jeden Zustand eineTiefensuche

Ziel : O((|| |TS|)

43

Lineare Gesamtlaufzeit - Idee

s

L(s’,) = W

L(s’,) = F

L(s’,A/E( U )) = ?

L(s’,) = W

L(s’,) = FL(s’,) = F

L(s’,A/E( U ) = W

L(s’,A/E( U ) = F

Bestimme durch eine einzige Tiefensuche nicht nur L(s,A/E( U )) , sondern ....

... auch L(s’,A/E( U )) für alle während der Suche betretenenZustände!

44

Was hilft das?

s0

S

S1

S2 Sn

....

|| ( O(|S1|) +

.... + O(|Sn|))

O( |S2|) +

= O(||(|S1| +|S2|+...+ |Sn|))

= O((|| |TS|)

L(s,A/E( U )) ?

45

Übung 1

Konstruiere einen Büchi-Automat, der genau die Sequenzen akzeptiert, die (G a) (F G b) erfüllen

46

Übung 2

Konstruiere den Produktautomat, der entsteht, wenndie Formel F a G F b auf folgendem Transitionssystemverifiziert wird:

ba

(Der untere Zustand ist einziger Initialzustand)

47

Übung 3

Finde das kleinstmögliche Transitionssystem, dasfolgende LTL-Formeln erfüllt....

G F b F G a a U b

... und folgende LTL-Formeln nicht erfüllt:

G b G a a X a