Post on 24-Aug-2019
Formale Grundlagen der Informatik II Kap 1: Transitionssysteme und Verifikation (Teil 2) Seite 1
1 Transitionssysteme und Verifikation 3
1.1 Transitionssysteme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.2 Produkte von Transitionssystemen . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.3 Automaten und regulare Sprachen . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.4 Kripkestrukturen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.4.1 Verifikation und Model-Checking . . . . . . . . . . . . . . . . . . . . . . 19
1.4.2 Transitionssysteme in Form von Kripke-Strukturen . . . . . . . . . . . . 21
1.4.3 Kripke-Strukturen von Programmen . . . . . . . . . . . . . . . . . . . . 25
1.4.4 Wechselseitiger Ausschluss . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1.5 Temporale Logik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1.5.1 Syntax und Semantik von LTL-Formeln . . . . . . . . . . . . . . . . . . 34
1.5.2 Syntax und Semantik von CTL- und CTL∗-Formeln . . . . . . . . . . . 37
1.5.3 Faire Kripke-Struktur . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
1.5.4 CTL-Model-Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
Formale Grundlagen der Informatik II Kap 1: Transitionssysteme und Verifikation (Teil 2) Seite
Das bedeutet: ∀s ∈ S ∃s� ∈ S : (s, s�) ∈ R
2
Definition 5.44 (Kripke-Struktur 2)
Eine Kripke-Struktur M := (S, S0, R, ES) besteht aus
a) einer endlichen Zustandsmenge S,
b) einer Menge S0 ⊆ S von Anfangszustanden,
c) einer linkstotalen (Transitions-)Relation R ⊆ S × S und
d) einer Zustandsetikettenfunktion ES : S → P(AP ), die jedem Zu-stand s eine Menge ES(s) ⊆ AP von aussagenlogischen atomarenFormeln zuordnet (die in diesem Zustand gelten).
238 Kapitel 5: Verifikation
Satz 5.40 Das Erreichbarkeitsproblem fur endliche P/T-Netze ist ent-scheidbar,benotigt jedoch mindestens exponentiell viel Platz.
Eine untere Schranke NSpace(2O(n)) wurde von Lipton 1976 bewiesen.Einen guten Uberblick uber weitere Komplexitatsresultate zu Algorith-men und Problemen bei Petrinetzen ist bei Esparza und Nielsen (1994)zu finden.
5.6 Kripke-Strukturen
Wir kommen nun zu Analyseverfahren, die auf Transitionssystemen vonbeliebigen Systemen anwendbar sind, also nicht speziell nur fur Petri-netze. Wegen ihrer Wurzeln in der Logik heißen sie Kripke-Strukturen.Dabei werden weniger die Aktionsfolgen als vielmehr die Eigenschaftender Zustande betrachtet. Solche Eigenschaften werden durch atomareAussagen in den Zustanden beschrieben. Im Gegensatz zu der in Ka-pitel 1 betrachteten Transitionsetikettenfunktion haben wir hier eineZustandsetikettenfunktion.
Definition 5.41 Sei TS = (S, A, tr, S0, SF ) ein Transitionssystem. Ei-ne Zustandsetikettenfunktion ist eine Abbildung ES : S → P(AP ), wo-bei AP eine Menge von atomaren Aussagen ist.
s0
s1
s2 s3
s4s5
1!
Tee Kaffee
" "
Tee_einfüllen Kaffee_einfüllen
{α1,α2} {α1,α3}
{α1}
∅
∅ ∅
Abbildung 5.20: Getrankeautomat als Transitionssystem mit Zustand-setikettenfunktion
Beispiel 5.42 Durch eine Zustandsetikettenfunktion konnen denZustanden Mengen von atomaren Aussagen zugeordned werden, die in
FGI-2/WiSe 2008/09
1.23
Formale Grundlagen der Informatik II Kap 1: Transitionssysteme und Verifikation (Teil 2) Seite 3
Zuweisung:C(l, v ! e, l!) "! pc = l"pc! = l!"v! = e"same(V \{v})
C(l!!, P2, l!)g:C(l, P1,
Hintereinanderausfuhrung:C(l, (P1; l!! : P2)7, l!) ! C(l, P1, l!!) " C(l!!, P2, l!)
?
ur die Zuweisungsfolge l1 : x := 2 · y;und dem Anfangswert = 1 = 2.
·und dem Anfangswert x = 1, y = 2.
; l2 : y :=
1; l3 mit
y − 1;Anfangszustand: S0 ≡ (x = 1 ∧ y = 2 ∧ pc = l1)
Beispiel 1.28 auf Seite 28
Formale Grundlagen der Informatik II Kap 1: Transitionssysteme und Verifikation (Teil 2) Seite 4
Schleifen-Anweisung:C(l, while b do l1 : P1 endwhile, l!) !(pc = l " pc! = l1 " b " same(V ))#(pc = l " pc! = l! " ¬b " same(V ))#C(l1, P1, l)
o l1 : P1
C(l,! b
! ¬b
le, l!)
Formale Grundlagen der Informatik II Kap 1: Transitionssysteme und Verifikation (Teil 2) Seite 5
Skip:C(l, skip, l!) ! pc = l " pc! = l! " same(V )
C(l,
o l1 : P1
se l2 : P2
! b
! ¬b
le, l!)
Bedingte Anweisung:C(l, if b then l1 : P1 else l2 : P2 endif , l!) !(pc = l " pc! = l1 " b " same(V ))#(pc = l " pc! = l2 " ¬b " same(V ))#C(l1, P1, l!) # C(l2, P2, l!)
Formale Grundlagen der Informatik II Kap 1: Transitionssysteme und Verifikation (Teil 2) Seite 6
C(l, PL, l!) !(pc = l " pc!1 = l1 " . . . " pc!n = ln " pc! =#) $Initialisierung(pc =# "pc1 = l!1". . ."pcn = l!n"pc! = l!"
!ni=1(pc!i =#)) $
Termination("n
i=1(C(li, Pi, l!i) " same(V \Vi) " same(PC\{pci})))Transition von Pi
PL = cobegin l1 : PL1 l!1! . . . !ln : PL
n l!n; coend
Formale Grundlagen der Informatik II Kap 1: Transitionssysteme und Verifikation (Teil 2) Seite 7
Beispielprogramm fur wechselseitigen Ausschluss
P = m : cobegin P0! P1 coend
warte bis b gilt !await b
await-Anweisung:C(l,await(b), l�) ≡(pci = l ∧ pc�
i = l ∧ ¬b ∧ same(Vi)) “busy waiting”∨ (pci = l ∧ pc�
i = l� ∧ b ∧ same(Vi))
b = trueb = false
C(l,! ¬b
le, l!)b
Formale Grundlagen der Informatik II Kap 1: Transitionssysteme und Verifikation (Teil 2) Seite 8
Die Programme sollen dabei (fur den Fall zweier Prozesse P und Q)folgende Eigenschaften erfullen:
A) Die Befehlszahler von P und Q sind nie gleichzeitig in ihren kriti-schen Abschnitten.
B) Meldet der Prozess P oder Q den Wunsch zum Eintritt in denkritischen Abschnitt an (wantP = True oder wantQ = True), sokann er nach einer gewissen endlichen Zeit tatsachlich in seinenkritischen Abschnitt eintreten.
=========================Parallele Programme oder Prozesse konnen zum konsistenten Schreibenauf gemeinsame Daten einen ”kritischen Abschnitt“ enthalten, der nichtuberlappend ausgefuhrt werden darf. Dies kommt im ”nicht-kritischenAbschnitt“ nicht vor.
Markierungs-Invarianz
Lebendigkeits-Invarianz
safety property
liveness property
Es gilt immer ....
Es gilt später einmal ....
Formale Grundlagen der Informatik II Kap 1: Transitionssysteme und Verifikation (Teil 2) Seite 9
P: Initialisierungm : cobegin P�Q coendwobei
P : l0 : while True do Q: l1 : while True dopi : non-critical section; qi : non-critical section;Eintrittsprotokoll Eintrittsprotokollpj : critical section; qj : critical section;Austrittsprotokoll : Austrittsprotokoll
endwhile l�0 endwhile l�1
a'gemeines Programm-Schema
Formale Grundlagen der Informatik II Kap 1: Transitionssysteme und Verifikation (Teil 2) Seite 10
11
1
FF
s0
21
1
TF
s2 12
1
FT
s4
31
1
TF
s6 22
1
TT
s7
13
2
FT
s9
51
1
TF
s10 32
1
TTs11
23
2
TTs12
15
2
FT
s13
33
2
TT
s15
53
2
TT
s18
33
1
TT
s16
35
1
TT
s19
11
2
FF
21
2
TF
12
2
FT
22
2
TT
52
1
TT25
2
TT
p1 p
1
p1
p1
p1
p2
p2
p2
p2
p3
p5
p1
p2
q1
q1
q1
q2
q2
q2
q2
q2
q2
p2
q3
p3
q3
p3
q3
p3
p3
q3
q5 p
5
q3
q5
25
2
TT
q5
p5
s8
s3
s5
s14
s17
q1 q
1
s1
(pi, qj ,
Zustand diej , last =
n, wantP
, wantQ =
) lautet.
wantP = wantQ = False : boolean,last = 1 ∨ last = 2 : integer,m : cobegin P�Q coendwobei
P : l0 : while True do[ p0 : non-critical section; ]
p1 : wantP := True;p2 : last := 1;p3 : wait(wantQ = False
∨ last = 2);[ p4 : critical section; ]
p5 : wantP := False;endwhile l�0
await
Formale Grundlagen der Informatik II Kap 1: Transitionssysteme und Verifikation (Teil 2) Seite 11