IV113 Validace a verifikace
Ověřování modelu pro CTL
a logiky větvícího se času
Jiří Barnat
Lineární x Větvící se čas
Pnueli, 1977
Systém lze chápat jako množinu sekvencí stavů – běhů.
Vlastnosti systému lze vymezit vlastnostmi běhů.
Vlastnosti běhů lze popsat temporální logikou
lineárního času.
Clarke & Emerson, 1980
Systém lze chápat jako strom možných pokračování,
tzv. výpočetní strom. V každém okamžiku chodu
systému existuje (konečně mnoho) možných pokračování
(budoucích stavů).
Systém lze vymezit vlastnostmi výpočetního stromu.
Vlastnosti stromu lze popsat temporální logikou
větvícího se času.
IV113 Úvod do validace a verifikace: CTL Model Checking str. 2/33
Systém a výpočetní strom z iniciálního stavu
1 2
1 1 1 1
2 2 2 2
2 2 2 2
IV113 Úvod do validace a verifikace: CTL Model Checking str. 3/33
Sekce
Logika CTL
(Computation Tree Logic)
IV113 Úvod do validace a verifikace: CTL Model Checking str. 4/33
CTL neformálně
Možné výpočty
Je-li dán výpočetní strom a jeden z jeho vrcholů, pak
podstrom určený daným vrcholem udává všechny možné
běhy, které systém z daného stavu může provést.
O každém jednom takovém běhu mluvíme jako o možném
výpočtu (možné budoucnosti).
CTL formule umožňují
Specifikovat vlastnosti stavů pomocí atomických propozic.
Kvantifikovat přes možné výpočty z daného stavu.
Omezovat množinu možných výpočtů pomocí
(kvantifikovaných) LTL operátorů.
Příklad
ϕ ≡ EF(a)
Je možné provést výpočet, ve kterém jednou bude platit a.
IV113 Úvod do validace a verifikace: CTL Model Checking str. 5/33
Syntax CTL
Nechť AP je množina atomických propozic. Pak
Je-li p ∈ AP, pak p je formule.
Je-li ϕ formule, pak ¬ϕ je formule.
Jsou-li ϕ a ψ formule, pak ϕ ∨ ψ je formule.
Je-li ϕ formule, pak EX ϕ je formule.
Jsou-li ϕ a ψ formule, pak E[ϕ U ψ] je formule.
Jsou-li ϕ a ψ formule, pak A[ϕ U ψ] je formule.
Alternativní zápis (Backus-Naur form)
ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | EX ϕ | E[ϕ U ϕ] | A[ϕ U ϕ]
IV113 Úvod do validace a verifikace: CTL Model Checking str. 6/33
Syntaktické zkratky
Standardní
Klasické syntaktické zkratky výrokové logiky
Syntaktické zkratky z LTL
F ϕ ≡ true U ϕ
G ϕ ≡ ¬F ¬ϕ
Odvozené temporální operátory CTL
EF ϕ ≡ E[true U ϕ]
AF ϕ ≡ A[true U ϕ]
EG ϕ ≡ ¬AF ¬ϕ
AG ϕ ≡ ¬EF ¬ϕ
AX ϕ ≡ ¬EX ¬ϕ
IV113 Úvod do validace a verifikace: CTL Model Checking str. 7/33
Modely CTL formulí
Model CTL formule
Je dána množina atomických propozic AP.
Modelem CTL formule je stav s ∈ S Kripkeho struktury
M = (S, T, I, s0).
Připomenutí
Běh v Kripkeho struktuře je maximální cesta začínající
v daném (iniciálním) stavu.
Na konečné běhy nahlížíme jako na nekonečné, které
vzniknou opakováním posledního stavu.
Značení
Nechť s ∈ S je stav Kripkeho struktury M = (S, T, I, s0).
PM(s) = {π | π je běh začínající ve stavu s}
IV113 Úvod do validace a verifikace: CTL Model Checking str. 8/33
Sémantika CTL
Předpoklady
Je dána množina atomických propozic AP.
Je dán stav s ∈ S Kripkeho struktury M = (S, T, I, s0).
ϕ, ψ jsou syntakticky správné CTL formule.
p ∈ AP je atomická propozice.
Sémantika
s |= p iff p ∈ I(s)
s |= ¬ϕ iff ¬(s |= ϕ)
s |= ϕ ∨ ψ iff s |= ϕ or s |= ψ
s |= EX ϕ iff ∃π ∈ PM(s).π(1) |= ϕ
s |= E[ϕ U ψ] iff ∃π ∈ PM(s).(∃k ≥ 0.(π(k) |= ψ and
∀0 ≤ i < k.π(i) |= ϕ))
s |= A[ϕ U ψ] iff ∀π ∈ PM(s).(∃k ≥ 0.(π(k) |= ψ and
∀0 ≤ i < k.π(i) |= ϕ))
IV113 Úvod do validace a verifikace: CTL Model Checking str. 9/33
Příklad
Vyjádřete pomocí CTL formule
Je možné dosáhnout stav, ve kterém platí a, ale neplatí b.
Pokud systém obdrží žádost Req, pak v konečném čase
vygeneruje potvrzení Ack.
V každém možném výpočtu nekonečně mnohokrát platí b.
Vždy je možné systém restartovat (dosáhnout stavu
Restart).
IV113 Úvod do validace a verifikace: CTL Model Checking str. 10/33
Sekce
Model Checking CTL
IV113 Úvod do validace a verifikace: CTL Model Checking str. 11/33
Definice problému
Model checking CTL
Je dána Kripkeho struktura M = (S, T, I, s0).
Je dána CTL formule ϕ.
Problém: Platí, že M, s0 |= ϕ?
Alternativně
Je dána Kripkeho struktura M = (S, T, I, s0).
Je dána CTL formule ϕ.
Problém: Spočítat množinu {s | M, s |= ϕ}.
Pojmenování
Výše uvedené přístupy se někdy také označují jako
Local model-checking problém — M, s0 |= ϕ.
Global model-checking problém — {s | M, s |= ϕ}.
Neplést s vlastností algoritmů.
Local algorithm for global model-checking.
IV113 Úvod do validace a verifikace: CTL Model Checking str. 12/33
Algoritmus pro CTL Model-Checking — Idea
Pozorování
Znám-li pro každý stav platnost formulí ϕ a ψ, snadno
odvodím platnost formulí ¬ϕ, ϕ ∨ ψ, EX ϕ, . . . .
Idea algoritmu pro CTL Model Checking
Je dána Kripkeho struktura M = (S, T, I) a formule ϕ.
Spočítám značkovací funkci label : S → 22ϕ
, která o
každém stavu s ∈ S Kripkeho struktury M řekne, jaké
podformule formule ϕ platí v daném stavu.
Platí, že s0 |= ϕ ⇐⇒ ϕ ∈ label(s0).
Funkci label budu počítat postupně pro jednotlivé
podformule formule ϕ, a to od nejjednodušších podformulí
(atomické propozice) ke složitějším (až po podformuli ϕ).
IV113 Úvod do validace a verifikace: CTL Model Checking str. 13/33
Podformule CTL formule
Podformule formule ϕ
Je dána CTL formule ϕ.
Množinu všech podformulí formule ϕ označujeme 2ϕ
.
Množina 2ϕ
je definována induktivně dle struktury ϕ.
Definice 2ϕ
1) ϕ ∈ 2ϕ
(ϕ je podformule ϕ)
2) Jestliže η ∈ 2ϕ
a
η ≡ ¬ψ, pak ψ ∈ 2ϕ
(ψ je podformule ϕ)
η ≡ ψ1 ∨ ψ2, pak ψ1, ψ2 ∈ 2ϕ
(ψ1, ψ2 jsou podformule ϕ)
η ≡ EX ψ, pak ψ ∈ 2ϕ
(ψ je podformule ϕ)
η ≡ E[ψ1 U ψ2], pak ψ1, ψ2 ∈ 2ϕ
(ψ1, ψ2 jsou podformule ϕ)
η ≡ A[ψ1 U ψ2], pak ψ1, ψ2 ∈ 2ϕ
(ψ1, ψ2 jsou podformule ϕ)
3) Žádná jiná formule není podformulí ϕ.
IV113 Úvod do validace a verifikace: CTL Model Checking str. 14/33
Transformace formule
Pozorování
Je snazší prokazovat, platnost existenčně kvantifikovaných
modálních operátorů než platnost univerzálně
kvantifikovaných modálních operátorů.
Pro účely verifikace CTL formule ϕ nad daným Kripkeho
systémem M, vyjádříme formuli ϕ v modifikovaném tvaru.
Alternativní základní syntax CTL
ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | EX ϕ | E[ϕ U ϕ] | EG ϕ
Příklad
Jak se vyjádří EG ϕ v původní základní syntaxi CTL?
Jak se definují podformule CTL formule ϕ je-li ϕ zapsána
pomocí alternativní syntax?
IV113 Úvod do validace a verifikace: CTL Model Checking str. 15/33
Algoritmus pro CTL Model-Checking
VSTUP: Kripkeho struktura M = (S, T, I, s0), CTL formule ϕ.
VÝSTUP: True, pokud s0 |= ϕ, jinak False.
proc CTLMC(ϕ, M)
label := I
Solved := AP ∩ 2ϕ
while ϕ ∈ Solved do
foreach ( η ∈ {¬ψ1, ψ1 ∨ ψ2, EX ψ1, E[ψ1 U ψ2], EG ψ1 | ψ1, ψ2 ∈ Solved})do
if (η ∈ 2ϕ
and η ∈ Solved)
then label := updateLabel(η, label, M)
Solved := Solved ∪ {η}
fi
od
od
return (ϕ ∈ label(s0))
end
IV113 Úvod do validace a verifikace: CTL Model Checking str. 16/33
Algoritmus pro CTL Model-Checking — updateLabel()
proc updateLabel(η, label, M)
if (η ≡ E[ψ1 U ψ2])
then return checkEU(ψ1, ψ2, label, M)
fi
if (η ≡ EG ψ)
then return checkEG(ψ, label, M)
fi
foreach ( s ∈ S)do
if (η ≡ ¬ψ and ψ ∈ label(s)) or
(η ≡ ψ1 ∨ ψ2 and (ψ1 ∈ label(s) ∨ ψ2 ∈ label(s))) or
(η ≡ EX ψ and (∃t ∈ {t | (s, t) ∈ T} takové, že ψ ∈ label(t)))
then label(s) := label(s) ∪ {η}
fi
od
return label
end
IV113 Úvod do validace a verifikace: CTL Model Checking str. 17/33
Algoritmus pro označení stavů podformulí E[ψ1 U ψ2]
VSTUP: Kripkeho struktura M = (S, T, I),
Značkovací funkce label : S → 2ϕ
, korektní vůči ψ1 a ψ2
VÝSTUP: Značkovací funkce label : S → 2ϕ
, korektní vůči E[ψ1 U ψ2]
proc checkEU(ψ1, ψ2, label, M)
Q := {s | ψ2 ∈ label(s)}
foreach ( s ∈ Q)do
label(s) := label(s) ∪ {E[ψ1 U ψ2]}
od
while (Q = ∅) do
choose s ∈ Q
Q := Q {s}
foreach ( t ∈ {t | T(t, s)}) do /* all immediate predecessors */
if (E[ψ1 U ψ2] ∈ label(t) ∧ ψ1 ∈ label(t))
then label(t) := label(t) ∪ {E[ψ1 U ψ2]}
Q := Q ∪ {t}
fi
od
od
return label
end
IV113 Úvod do validace a verifikace: CTL Model Checking str. 18/33
Silně souvislé komponenty
Podgraf
Nechť G = (V , E) je graf, tj. E ⊆ V × V .
Graf G = (V , E ) nazveme podgrafem grafu G pokud
platí V ⊆ V a E = E ∩ V × V .
Podgraf C = (V , E ) grafu G = (V , E) se nazývá
silně souvislá komponenta, pokud ∀u, v ∈ V platí, že
(u, v) ∈ E ∗
a (v, u) ∈ E ∗
.
maximální silně souvislá komponenta (SCC), pokud C je
silně souvislá komponenta a pro každé v ∈ (V V ) platí,
že (V ∪ {v}, E ∩ (V ∪ {v} × V ∪ {v})) není silně
souvislá komponenta.
netriviální silně souvislá komponenta, pokud C je silně
souvislá komponenta a E = ∅.
IV113 Úvod do validace a verifikace: CTL Model Checking str. 19/33
Algoritmus pro označení stavů podformulí EG ψ
VSTUP: Kripkeho struktura M = (S, T, I, s0),
Značkovací funkce label : S → 2ϕ
, korektní vůči ψ
VÝSTUP: Značkovací funkce label : S → 2ϕ
, korektní vůči EG ψ
proc checkEG(ψ, label, M)
S’ := {s | ψ ∈ label(s)}
SCC := {C | C je netriviální SCC grafu G = (S , T ∩ S × S )}
Q := C∈SCC
{s | s ∈ C}
foreach ( s ∈ Q)do
label(s) := label(s) ∪ {EG ψ}
od
while Q = ∅ do
choose s ∈ Q
Q := Q {s}
foreach ( t ∈ (S ∩ {t | T(t, s)}))do /* all immediate predecessors in S */
if EG ψ ∈ label(t)
then label(t) := label(t) ∪ {EG ψ}
Q := Q ∪ {t}
fi
od
od
end
IV113 Úvod do validace a verifikace: CTL Model Checking str. 20/33
Složitost algoritmu pro ověřování formule CTL
Pozorování
Každá CTL formule ϕ má nejvýše | ϕ | různých
podformulí.
Rozklad každého podgrafu grafu G = (S, T) na SCC lze
provést v čase O(| S | + | T |).
Každé volání funkce updateLabel skončí v čase
O(| S | + | T |).
Celková složitost
Algoritmus CTLMC má časovou složitost
O(| ϕ | (| S | + | T |)).
Algoritmus CTLMC má prostorovou složitost
O(| ϕ || S |).
IV113 Úvod do validace a verifikace: CTL Model Checking str. 21/33
Příklad: Mikrovlnná trouba AG(Start =⇒ AF(Heat))
IV113 Úvod do validace a verifikace: CTL Model Checking str. 22/33
Příklad: Mikrovlnná trouba AG(Start =⇒ AF(Heat))
Přepis formule ϕ ≡ AG(Start =⇒ AF(Heat))
AG(Start =⇒ AF(Heat))
AG(¬(Start ∧ ¬AF(Heat)))
AG(¬(Start ∧ EG(¬Heat)))
¬EF(Start ∧ EG(¬Heat))
¬E[true U (Start ∧ EG(¬Heat))]
Platnost podformulí [S(ϕ) = {s | s |= ϕ}]
S(Start) = {2, 5, 6, 7}
S(Heat) = {4, 7}
S(¬Heat) = {1, 2, 3, 5, 6}
S(EG(¬Heat)) = {1, 2, 3, 5}
S(Start ∧ EG(¬Heat)) = {2, 5}
S(E[true U (Start ∧ EG(¬Heat))]) = {1, 2, 3, 4, 5, 6, 7}
S(¬E[true U (Start ∧ EG(¬Heat))]) = ∅
IV113 Úvod do validace a verifikace: CTL Model Checking str. 23/33
Sekce
Logika CTL∗
IV113 Úvod do validace a verifikace: CTL Model Checking str. 24/33
CTL∗
jako rozšíření CTL
Pozorování
V logice CTL není možné omezit množinu možných
výpočtů libovolnou LTL formulí. Tj. každý modální
operátor LTL musí být bezprostředně předcházen
kvantifikátorem.
Logika CTL∗
Logika větvícího se času stejně jako logika CTL.
Množiny možných běhů lze omezit libovolnou LTL formulí.
V syntax logiky CTL∗
vystupují kvantifikátory cest jako
samostatné operátory.
Příklad
A[p ∧ X(¬p)] je formule CTL∗
, ale není to formule CTL.
IV113 Úvod do validace a verifikace: CTL Model Checking str. 25/33
Syntax CTL∗
Typy CTL∗
formulí
Operátory E a A jsou samostatné, proto existují v CTL∗
formule jejichž modelem je běh Kripkeho struktury.
Aplikací operátorů E a A vznikají z formulí jejichž
modelem je běh Kripkeho struktury, formule, jejichž
modelem je stav Kripkeho struktury.
Rozlišujeme tedy formule stavu a formule cesty.
Syntax CTL∗
formule stavu ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | E ψ
formule cesty ψ ::= ϕ | ¬ψ | ψ ∨ ψ | X ψ | ψ U ψ
IV113 Úvod do validace a verifikace: CTL Model Checking str. 26/33
Sémantika CTL∗
Předpoklady
Je dána množina atomických propozic AP, p ∈ AP.
Je dána Kripkeho struktura M = (S, T, I).
ϕ1, ϕ2 jsou CTL∗
formule stavu, ψ1, ψ2 formule cesty.
Sémantika
M, s |= p iff p ∈ I(s)
M, s |= ¬ϕ1 iff ¬(M, s |= ϕ1)
M, s |= ϕ1 ∨ ϕ2 iff M, s |= ϕ1 or M, s |= ϕ2
M, s |= E ψ1 iff ∃π ∈ PM (s).π |= ψ1
M, π |= ϕ1 iff M, π(0) |= ϕ1
M, π |= ¬ψ1 iff ¬(M, π |= ψ1)
M, π |= ψ1 ∨ ψ2 iff M, π |= ψ1 or M, π |= ψ2
M, π |= X ψ1 iff M, π1
|= ψ1
M, π |= ψ1 U ψ2 iff ∃k ≥ 0.(M, πk
|= ψ2 and
∀0 ≤ i < k.M, πi
|= ψ1)
IV113 Úvod do validace a verifikace: CTL Model Checking str. 27/33
Sekce
Porovnání logik LTL, CTL a CTL∗
IV113 Úvod do validace a verifikace: CTL Model Checking str. 28/33
Unifikace modelů
Pozorování
Každá LTL formule je CTL∗
formule cesty.
Každá CTL formule je CTL∗
formule stavu.
Modelem CTL∗
formule cesty je běh Kripkeho struktury.
Modelem CTL∗
formule stavu je stav Kripkeho struktury.
Nevhodné pro účely porovnání.
Unifikace modelu
Za účelem unifikace modelů definujeme, kdy CTL∗
formule cesty platí ve stavu Kripkeho struktury.
Nechť ψ je CTL∗
formule cesty, pak
M, s |= ψ iff M, s |= A ψ
IV113 Úvod do validace a verifikace: CTL Model Checking str. 29/33
Motivace
Cíl
Chceme zjistit, zda jsou vlastnosti (formule), které lze
vyjádřit v jedné logice a nelze vyjádřit v jiné logice.
Chceme zjistit, ve které logice lze vyjádřit víc vlastností.
Chceme identifikovat vlastnosti, které nelze vyjádřit v jiné
logice, tj. jak vypadá formule logiky L1, pro kterou
neexistuje ekvivalentní formule logiky L2.
Ekvivalence formulí (i různých logik)
Formule ϕ a ψ jsou ekvivalentní, právě když pro všechny
modely M = (S, T, I, s0) a stavy s ∈ S platí
M, s |= ϕ iff M, s |= ψ
IV113 Úvod do validace a verifikace: CTL Model Checking str. 30/33
Expresibilita – vyjadřovací síla
Shodná expresibilita
Temporální logiky L1 a L2 jsou shodně expresibilní (mají
stejnou vyjadřovací sílu), pokud pro všechny modely
M = (S, T, I, s0) a stavy s ∈ S platí
∀ϕ ∈ L1.(∃ψ ∈ L2.(M, s |= ϕ ⇐⇒ M, s |= ψ)) (1)
∧ ∀ψ ∈ L2.(∃ϕ ∈ L1.(M, s |= ϕ ⇐⇒ M, s |= ψ)). (2)
Menší expresibilita
Pokud platí pouze tvrzení (1), tj. neplatí tvrzení (2), pak
je logika L1 méně expresibilní (má menší vyjadřovací sílu)
než logika L2.
IV113 Úvod do validace a verifikace: CTL Model Checking str. 31/33
Porovnání LTL, CTL, a CTL∗
Tvrzení 1
LTL a CTL jsou vyjadřovací silou neporovnatelné.
1) AG(EF(q)) je CTL formule, kterou nelze vyjádřit v LTL.
2) FG(q) je LTL formule, kterou nelze vyjádřit v CTL.
Příklad – důkaz 1)
Najděte dvě různé Kripkeho struktury a v nich
identifikujte stavy, které jsou rozlišitelné CTL formulí
AG(EF(q)) a přitom nejsou rozlišitelné žádnou LTL
formulí (generují shodnou množinu běhů).
Příklad – intuice za 2) [důkaz jde nad rámec tohoto kurzu]
Ukažte, že CTL formule AF(AG(q)) není ekvivalentní
LTL formuli FG(q).
IV113 Úvod do validace a verifikace: CTL Model Checking str. 32/33
Porovnání LTL, CTL, a CTL∗
Důsledek 1
CTL∗
je striktně více expresibilní než LTL.
Každá LTL formule je i formule CTL∗
.
CTL∗
formule AG(EFq) není vyjádřitelná v LTL.
Důsledek 2
CTL∗
je striktně více expresibilní než CTL.
Každá CTL formule je i formule CTL∗
.
CTL∗
formule FG(q) není vyjádřitelná v CTL.
Pozorování
Existují vlastnosti vyjádřitelné jak v LTL tak i v CTL.
CTL formule A[p U q] je ekvivalentní LTL formuli p U q.
IV113 Úvod do validace a verifikace: CTL Model Checking str. 33/33