IV113 Validace a verifikace
Převod LTL formule na Büchi automat
Jiří Barnat
Připomenutí
Problém
Kripkeho struktura M
LTL formule ϕ
M |= ϕ ?
Řešení pomocí Büchi automatů
Asys – automat akceptující běhy modelu
A¬ϕ – automat akceptující běhy porušující vlastnost ϕ
L(Asys) ∩ L(A¬ϕ) = L(Asys × A¬ϕ)
L(Asys × A¬ϕ) = ∅ ⇐⇒ model má běh porušující ϕ
M |= ϕ ⇐⇒ Asys × A¬ϕ nemá akceptující cyklus
IV113 úvod do validace a verifikace: LTL → BA str. 2/26
Grafické znázornění sémantiky temporálních operátorů
X ϕ : •−→
ϕ
•−→•−→•−→•−→• · · ·
ϕ U ψ :
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ψ
•−→• · · ·
F ϕ : •−→•−→•−→•−→
ϕ
•−→• · · ·
G ϕ :
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
• · · ·
ϕ R ψ :
ψ
•−→
ψ
•−→
ψ
•−→
ψ
•−→
ϕ∧ψ
• −→• · · · or
ψ
•−→
ψ
•−→
ψ
•−→
ψ
•−→
ψ
•−→
ψ
• · · ·
ϕ W ψ :
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ψ
•−→• · · · or
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
•−→
ϕ
• · · ·
IV113 úvod do validace a verifikace: LTL → BA str. 3/26
Příklad
Nechť Σ = {a, b, c}, najděte Büchi automat, který akceptuje
ω-regulární jazyk definovaný následující LTL formulí.
a) a U b
b) a U (X b)
c) ¬(a U (X b))
d) a U (b U c)
e) ¬(a U (b U c))
IV113 úvod do validace a verifikace: LTL → BA str. 4/26
Sekce
Algoritmus převodu
LTL formule na Büchi automat
IV113 úvod do validace a verifikace: LTL → BA str. 5/26
Postup převodu
Vstup: Množina atomických propozic AP, LTL formule ϕ.
Výstup: Büchi automat A takový, že L(A) = Lϕ.
Postup:
Formule ϕ se převede do normální formy.
Vypočítá se přechodový graf budoucího automatu.
Graf se doplní na zobecněný Büchi automat.
Zobecněný BA se převede na standardní Büchi automat.
IV113 úvod do validace a verifikace: LTL → BA str. 6/26
Normální forma LTL formule
Řekneme, že LTL formule je v normální formě, pokud
neobsahuje operátory F a G, a všechny operátory unární
negace jsou aplikovány na podformule tvořené pouze
atomickou propozicí.
Syntax
ϕ ::= p | ¬p | ϕ ∨ ϕ | ϕ ∧ ϕ | X ϕ | ϕ U ϕ | ϕ R ϕ
Pravidla pro převod do normální formy
¬(ϕ ∨ ψ) ≡ (¬ϕ) ∧ (¬ψ)
¬(ϕ ∧ ψ) ≡ (¬ϕ) ∨ (¬ψ)
¬Xϕ ≡ X(¬ϕ)
¬(ϕ U ψ) ≡ (¬ϕ R ¬ψ)
¬(ϕ R ψ) ≡ (¬ϕ U ¬ψ)
IV113 úvod do validace a verifikace: LTL → BA str. 7/26
Příklad
Nechť AP = {a, b}. Převeďte následující LTL formule do
normální formy
a) G(F(a))
b) F(G(a))
c) ¬(G(F(a))
d) G(a =⇒ F(b))
e) ¬(a U (G b))
IV113 úvod do validace a verifikace: LTL → BA str. 8/26
Zobecněné Büchi automaty
Büchi automaty
A = (Σ, S, s, δ, F)
F ⊆ S je množina koncových stavů.
Běh ρ je akceptující, pokud inf (ρ) ∩ F = ∅.
Zobecněné Büchi automaty
A = (Σ, S, s, δ, F)
F ⊆ 2S
je systém množin koncových stavů.
Běh ρ je akceptující, pokud ∀Fi ∈ F platí inf (ρ) ∩ Fi = ∅.
IV113 úvod do validace a verifikace: LTL → BA str. 9/26
Příklad
Nechť Σ = {a, b} a L = {w ∈ Σω
| inf (w) = {a, b}}.
Najděte zobecněný BA A takový, že L(A) = L.
IV113 úvod do validace a verifikace: LTL → BA str. 10/26
Zobecněné Büchi automaty
Tvrzení
Ke každému zobecněnému Büchi automatu A existuje
(normální) Büchi automat B takový, že L(A) = L(B).
Konstrukce
Nechť A = (Σ, S, s, δ, {F1, . . . , Fn}).
B = (Σ, S × {0, . . . , n}, (s, 0), δ , S × {n}), kde
(q, y) ∈ δ ((p, x), a) pokud q ∈ δ(p, a) a pro x a y platí
jestliže q ∈ Fi a x = i − 1, tak y = i
jestliže x = n, tak y = 0
jinak x = y.
IV113 úvod do validace a verifikace: LTL → BA str. 11/26
Příklad ZBA → BA
ZBA: F = {F1 = {p}, F2 = {q}}
a b
→ p p q
q p q
BA: F = {(p, 2), (q, 2)}
a b
→ (p,0) (p,1) (q,0)
(q,0) (p,1) (q,0)
(p,1) (p,1) (q,2)
(q,1) (p,1) (q,2)
← (p,2) (p,0) (q,0)
← (q,2) (p,0) (q,0)
IV113 úvod do validace a verifikace: LTL → BA str. 12/26
Sekce
Výpočet přechodového grafu
IV113 úvod do validace a verifikace: LTL → BA str. 13/26
Přechodový graf intuitivně
Pozorování
Přechod v Büchi automatu stráží jeden stav běhu.
Pro definici přechodu, je třeba vědět, co platí v aktuálním
stavu, a co má platit v následujícím stavu běhu.
Rozbalené definice modálních operátorů
X a ≡ tt ∧ X( a )
a U b ≡ a ∧ X( a U b )
∨ b ∧ X( tt )
a R b ≡ b ∧ X( a R b )
∨ a ∧ b ∧ X( tt )
IV113 úvod do validace a verifikace: LTL → BA str. 14/26
Přechodový graf intuitivně
Pozorování
Přechod v Büchi automatu stráží jeden stav běhu.
Pro definici přechodu, je třeba vědět, co platí v aktuálním
stavu, a co má platit v následujícím stavu běhu.
Rozbalené definice modálních operátorů
New Now Next
X a ≡ a
a U b ≡ a a U b
∨ b
a R b ≡ b a R b
∨ a ∧ b
IV113 úvod do validace a verifikace: LTL → BA str. 14/26
Přechodový graf LTL formule
Uzel je uspořádaná pětice
Id – Číslo
Unikátní označení uzlu.
Incoming – Množina označení uzlů.
Množina přímých předchůdců vrcholu ve výsledném grafu.
Kóduje hrany grafu.
Now – Množina LTL formulí.
Seznam podformulí, které platí v daném uzlu.
New – Množina LTL formulí.
Množina ještě nezpracovaných formulí, které musí být splněny
v tomto uzlu.
Next – Množina LTL formulí.
Seznam formulí, které musí být splněny v následujícím uzlu.
IV113 úvod do validace a verifikace: LTL → BA str. 15/26
Graf LTL formule
Vytvoření grafu (výpočet množiny uzlů)
proc create_graph(ϕ)
N = (new_ID(), {init}, ∅, {ϕ}, ∅)
return expand(N, ∅)
end
Pomocné funkce
expand(n, Nodes)
Funkce volaná pro uzel n a dosud známe uzly Nodes.
Vrací množinu uzlů (po zpracování uzlu n).
new_ID()
Každé volání této funkce vrátí dosud nevrácené číslo.
Neg(_)
Neg(A) = ¬A pro všechny A ∈ AP.
Neg(True) = False
Neg(False) = True
¬¬A = A
IV113 úvod do validace a verifikace: LTL → BA str. 16/26
Graf LTL formule – funkce expand
proc expand(q, Nodes)
if New(q) == ∅
then if (∃r ∈ Nodes takový, že Now(r) == Now(q) ∧ Next(r) == Next(q))
then Incoming(r) = Incoming(r) ∪ Incoming(q)
return Nodes
else N = (new_ID(), {ID(q)}, ∅, Next(q), ∅)
return expand(N, Nodes ∪ {q}) /∗ q je nový uzel ∗/
fi
else let η ∈ New(q)
New(q) = New(q) {η}
if η ∈ Now(q) /∗ η již byla zpracována ∗/
then return expand(q, Nodes)
fi
switch (η) /∗ pokračuj podle typu nejvnějšnějšího operátoru η ∗/
. . .
end
fi
end
IV113 úvod do validace a verifikace: LTL → BA str. 17/26
Graf LTL formule – funkce expand (switch)
switch (η) /∗ pokračuj podle typu nejvnějšnějšího operátoru η ∗/
case (η ∈ (AP ∪ Neg(AP) ∪ {True, False}))
if (η == False ∨ Neg(η) ∈ Now(q))
then return Nodes
else N = (new_ID(), Incoming(q), Now(q) ∪ {η}, New(q), Next(q))
return expand(N, Nodes)
fi
end
case (η ≡ ϕ U ψ)
N1 = (new_ID(), Incoming(q),
Now(q) ∪ {η}, New(q) ∪ {ϕ}, Next(q) ∪ {ϕ U ψ})
N2 = (new_ID(), Incoming(q),
Now(q) ∪ {η}, New(q) ∪ {ψ}, Next(q))
return expand(N2, expand(N1, Nodes))
end
. . .
IV113 úvod do validace a verifikace: LTL → BA str. 18/26
Graf LTL formule – funkce expand (switch)
case (η ≡ ϕ R ψ)
N1 = (new_ID(), Incoming(q),
Now(q) ∪ {η}, New(q) ∪ {ϕ, ψ}, Next(q))
N2 = (new_ID(), Incoming(q),
Now(q) ∪ {η}, New(q) ∪ {ψ}, Next(q) ∪ {ϕ R ψ})
return expand(N2, expand(N1, Nodes))
end
case (η ≡ ϕ ∨ ψ)
N1 = (new_ID(), Incoming(q),
Now(q) ∪ {η}, New(q) ∪ {ϕ}, Next(q))
N2 = (new_ID(), Incoming(q),
Now(q) ∪ {η}, New(q) ∪ {ψ}, Next(q))
return expand(N2, expand(N1, Nodes))
end
. . .
IV113 úvod do validace a verifikace: LTL → BA str. 19/26
Graf LTL formule – funkce expand (switch)
case (η ≡ ϕ ∧ ψ)
N = (new_ID(), Incoming(q),
Now(q) ∪ {η}, New(q) ∪ {ϕ, ψ}, Next(q))
return expand(N, Nodes)
end
case (η ≡ X ϕ)
N = (new_ID(), Incoming(q),
Now(q) ∪ {η}, New(q), Next(q) ∪ {ϕ})
return expand(N, Nodes)
end
end /∗ end of switch ∗/
IV113 úvod do validace a verifikace: LTL → BA str. 20/26
Příklad výpočet grafu pro formuli X(a)
Vypočtené uzly
Id: 2
Incoming: init
Now: X(a)
New: ∅
Next: a
Id: 4
Incoming: 2
Now: a
New: ∅
Next: ∅
Id: 5
Incoming: 4,5
Now: ∅
New: ∅
Next: ∅
Výpočet
Id Incoming Now New Next
1 init ∅ {X(a)} ∅
2 init {X(a)} ∅ {a}
Uzel 2 je nově vypočtený uzel.
3 2 ∅ {a} ∅
4 2 {a} ∅ ∅
Uzel 4 je nově vypočtený uzel.
5 4 ∅ ∅ ∅
Uzel 5 je nově vypočtený uzel.
6 5 ∅ ∅ ∅
Uzel 6 je shodný s uzlem 5.
Incoming(5) = Incoming(5)∪{5}
IV113 úvod do validace a verifikace: LTL → BA str. 21/26
Příklad a U (b U c)
01| in, ∅, {aU(bUc)}, ∅
02| in, {aU(bUc)}, {a}, {aU(bUc)} 03| in, {aU(bUc)}, {bUc}, ∅
04| in, {aU(bUc),a}, ∅, {aU(bUc)}
Uzel 04 je nově vypočtený uzel.
05| 04, ∅, {aU(bUc)}, ∅
06| 04, {aU(bUc)}, {a}, {aU(bUc)} 07| 04, {aU(bUc)}, {bUc}, ∅
08| 04, {aU(bUc),a}, ∅, {aU(bUc)}
Uzlu 04 je přidán předchůdce 04.
07| 04, {aU(bUc)}, {bUc}, ∅
09| 04, {aU(bUc),bUc}, {b}, {bUc} 10| 04, {aU(bUc),bUc}, {c}, ∅
11| 04, {aU(bUc),bUc,b}, ∅, {bUc}
Uzel 11 je nově vypočtený uzel.
12| 11, ∅, {bUc}, ∅
13| 11, {bUc}, {b}, {bUc} 14| 11, {bUc}, {c}, ∅
15| 11, {bUc,b}, ∅, {bUc}
Uzel 15 je nově vypočtený uzel.
16| 15, ∅ {bUc}, ∅
17| 15, {bUc}, {b}, {bUc} 18| 15, {bUc}, {c}, ∅
19| 15, {bUc,b}, ∅, {bUc}
Uzlu 15 je přidán předchůdce 15.
IV113 úvod do validace a verifikace: LTL → BA str. 22/26
Příklad a U (b U c) – pokračování
18| 15, {bUc}, {c}, ∅
20| 15, {bUc,c}, ∅, ∅
Uzel 20 je nově vypočtený uzel.
21| 20, ∅, ∅, ∅
Uzel 21 je nově vypočtený uzel.
22| 21, ∅, ∅, ∅
Uzlu 21 je přidán předchůdce 21.
14| 11, {bUc}, {c}, ∅
23| 11, {bUc,c}, ∅, ∅
Uzlu 20 je přidán předchůdce 11.
10| 04, {aU(bUc),bUc}, {c}, ∅
24| 04, {aU(bUc),bUc,c}, ∅, ∅
Uzel 24 je nově vypočtený uzel.
25| 24, ∅, ∅, ∅
Uzlu 21 je přidán předchůdce 24.
IV113 úvod do validace a verifikace: LTL → BA str. 23/26
Příklad a U (b U c) – pokračování
03| in, {aU(bUc)}, {bUc}, ∅
26| in, {aU(bUc),bUc}, {b}, {bUc} 27| in, {aU(bUc),bUc}, {c}, ∅
28| in, {aU(bUc),bUc,b}, ∅, {bUc}
Uzlu 11 je přidán předchůdce in.
27| in, {aU(bUc),bUc}, {c}, ∅
29| in, {aU(bUc),bUc,c}, ∅, ∅
Uzlu 24 je přidán předchůdce in.
IV113 úvod do validace a verifikace: LTL → BA str. 24/26
Převedení grafu na zobecněný Büchi automat
Předpoklady
Dána množina AP.
Nodes je množina vrcholů grafu LTL formule.
Zobecněný Büchi automat A = (S, Σ, δ, init, F)
S = Nodes ∪ {init}
Σ = 2AP
r ∈ δ(r, α) pokud
r ∈ Incoming(r ), α ∈ Σ
α splňuje omezení dané množinou ((AP ∪ ¬AP) ∩ Now(r ))
F = {F1, . . . , Fn}
Pro každou podformuli ve tvaru ϕ U ψ definujeme Fi .
Fi = {r ∈ Nodes | ψ ∈ Now(r) ∨ ϕUψ ∈ Now(r)}.
IV113 úvod do validace a verifikace: LTL → BA str. 25/26
Příklad a U (b U c) – Zobecněný Büchi automat
Přechodová funkce (stráže)
a b c tt
→ init 04 11 24
04 04 11 24
11 15 20
15 15 20
20 21
21 21
24 21
F – akceptující množiny
FaU(bUc) — {11,15,20,21,24}
FbUc — {04,20,21,24}
IV113 úvod do validace a verifikace: LTL → BA str. 26/26