IA159 Formal Verification Methods
LTL→BA via Very Weak Alternating BA
František Blahoudek
Department of Computer Science
Faculty of Informatics
Masaryk University
Outline & Sources
Outline
1 infinite words
2 Linear Temporal Logic (LTL)
3 nondeterministic Büchi automata (BA) and their variants
4 alternating automata (AA)
5 translation of LTL into BA via AA
Source
P. Gastin and G. Oddoux: Fast LTL to Büchi Automata
Translation, LNCS 2102, Springer, 2001.
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 2/73
Motivation – Infinite Behaviours
system behaviour as a sequence of sets of atomic propositions
{request}{request}{}{print}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 3/73
Motivation – Infinite Behaviours
system behaviour as a sequence of sets of atomic propositions
{request}{request}{}{print}
infinite behaviours = infinite words (ω-words)
{}{request}{}{request, print}{}({request}{print})ω
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 4/73
Motivation – Infinite Behaviours
system behaviour as a sequence of sets of atomic propositions
{request}{request}{}{print}
infinite behaviours = infinite words (ω-words)
{}{request}{}{request, print}{}({request}{print})ω
u = u(0)u(1) . . . ∈ Σω ω-word over the alphabet Σ
ui = u(i)u(i + 1) . . . the i-th suffix of u
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 5/73
Motivation – Infinite Behaviours
system behaviour as a sequence of sets of atomic propositions
{request}{request}{}{print}
infinite behaviours = infinite words (ω-words)
{}{request}{}{request, print}{}({request}{print})ω
u = u(0)u(1) . . . ∈ Σω ω-word over the alphabet Σ
ui = u(i)u(i + 1) . . . the i-th suffix of u
For reasoning about infinite behaviours we need
1 to express interesting properties, and (LTL)
2 to check the properties efficiently. (Büchi automata)
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 6/73
Syntax of LTL
Formulae of Linear Temporal Logic (LTL) in Positive Normal
Form are defined by
ϕ ::= | ⊥ | a | ¬a | ϕ1∧ϕ2 | ϕ1∨ϕ2 | Xϕ | ϕ1 U ϕ2 | ϕ1 R ϕ2
where , ⊥ stand for true, false respectively and a ranges over
a countable set AP of atomic propositions.
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 7/73
Syntax of LTL
Formulae of Linear Temporal Logic (LTL) in Positive Normal
Form are defined by
ϕ ::= | ⊥ | a | ¬a | ϕ1∧ϕ2 | ϕ1∨ϕ2 | Xϕ | ϕ1 U ϕ2 | ϕ1 R ϕ2
where , ⊥ stand for true, false respectively and a ranges over
a countable set AP of atomic propositions.
Abbreviations: Fϕ ≡ U ϕ Gϕ ≡ ⊥ R ϕ
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 8/73
Syntax of LTL
Formulae of Linear Temporal Logic (LTL) in Positive Normal
Form are defined by
ϕ ::= | ⊥ | a | ¬a | ϕ1∧ϕ2 | ϕ1∨ϕ2 | Xϕ | ϕ1 U ϕ2 | ϕ1 R ϕ2
where , ⊥ stand for true, false respectively and a ranges over
a countable set AP of atomic propositions.
Abbreviations: Fϕ ≡ U ϕ Gϕ ≡ ⊥ R ϕ
Temporal operators: terminology and intuitive meaning
Xa next • a • • • . . .
a U b until a a . . . a b • • • . . .
a R b releases b b . . . b a
b • • • . . . or
b b b b . . .
Fa eventually • • . . . • a • • . . .
Ga always a a a a . . .
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 9/73
Semantics of LTL
Let Σ = 2AP where AP ⊆ AP is finite. The validity of an LTL
formula ϕ for u ∈ Σω, written u |= ϕ, is defined as
u |=
u |= a iff a ∈ u(0)
u |= ¬a iff a ∈ u(0)
u |= ϕ1 ∨ ϕ2 iff u |= ϕ1 or u |= ϕ2
u |= ϕ1 ∧ ϕ2 iff u |= ϕ1 and u |= ϕ2
u |= Xϕ iff u1 |= ϕ
u |= ϕ1 U ϕ2 iff ∃i ≥ 0 such that
ui |= ϕ2 and ∀ 0 ≤ j < i . uj |= ϕ1
u |= ϕ1 R ϕ2 iff ∃i ≥ 0 such that
ui |= ϕ1 and ∀ 0 ≤ j ≤ i . uj |= ϕ2,
or ∀i ≥ 0 . ui |= ϕ2
Given an alphabet Σ, an LTL formula ϕ defines the language
LΣ
(ϕ) = {w ∈ Σω
| w |= ϕ}.
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 10/73
Büchi Automata
A Büchi automaton (BA) is a tuple A = (Q, Σ, δ, q0, F) defined
precisely as a finite automaton, but
a Büchi automaton is interpreted over infinite words, and
a run is accepting if it visits some accepting state infinitely
often.
p q
b
a, b
a
b
Accepts all infinite
words over Σ = {a, b}
with infinitely many b.
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 11/73
Büchi Automata
A Büchi automaton (BA) is a tuple A = (Q, Σ, δ, q0, F) defined
precisely as a finite automaton, but
a Büchi automaton is interpreted over infinite words, and
a run is accepting if it visits some accepting state infinitely
often.
p q
b
a, b
a
b
Accepts all infinite
words over Σ = {a, b}
with infinitely many b.
p q
{b}, {a, b}b
∅, {b}, {a}, {a, b}
{a}, ∅¬b
{b}, {a, b}b
Accepts all infinite
words over Σ = 2{a,b}
where b appears in
infinitely many sets.
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 12/73
Büchi Automata
A Büchi automaton (BA) is a tuple A = (Q, Σ, δ, q0, F) defined
precisely as a finite automaton, but
a Büchi automaton is interpreted over infinite words, and
a run is accepting if it visits some accepting state infinitely
often.
p q
b
a, b
a
b
Accepts all infinite
words over Σ = {a, b}
with infinitely many b.
p q
{b}, {a, b}b
∅, {b}, {a}, {a, b}
{a}, ∅¬b
{b}, {a, b}b
Accepts all infinite
words over Σ = 2{a,b}
where b appears in
infinitely many sets.
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 13/73
Extensions of Büchi Automata
1 transition-based acceptance:
a run is accepting if it visits some
accepting transition infinitely often
p q
b
¬b
¬b
b
p q
b
¬b
¬b
b
p
¬b
b
p
¬a ∧ ¬b
a ∧ ¬b ¬a ∧ b
a ∧ b
p q¬b
¬b
state-based
Büchi
p¬b b
transition-based
co-Büchi
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 14/73
Extensions of Büchi Automata
1 transition-based acceptance:
a run is accepting if it visits some
accepting transition infinitely often
p q
b
¬b
¬b
b
p q
b
¬b
¬b
b
p
¬b
b
p
¬a ∧ ¬b
a ∧ ¬b ¬a ∧ b
a ∧ b
p q¬b
¬b
state-based
Büchi
p¬b b
transition-based
co-Büchi
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 15/73
Extensions of Büchi Automata
1 transition-based acceptance:
a run is accepting if it visits some
accepting transition infinitely often
2 generalized Büchi acceptance:
more sets of accepting
states/transitions
a run is accepting if each set is visited
infinitely often
p q
b
¬b
¬b
b
p q
b
¬b
¬b
b
p
¬b
b
p
¬a ∧ ¬b
a ∧ ¬b ¬a ∧ b
a ∧ b
p q¬b
¬b
state-based
Büchi
p¬b b
transition-based
co-Büchi
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 16/73
Extensions of Büchi Automata
1 transition-based acceptance:
a run is accepting if it visits some
accepting transition infinitely often
2 generalized Büchi acceptance:
more sets of accepting
states/transitions
a run is accepting if each set is visited
infinitely often
3 co-Büchi acceptance
a run is accepting if it contains only
finitely many accepting
states/transitions
p q
b
¬b
¬b
b
p q
b
¬b
¬b
b
p
¬b
b
p
¬a ∧ ¬b
a ∧ ¬b ¬a ∧ b
a ∧ b
p q¬b
¬b
state-based
Büchi
p¬b b
transition-based
co-Büchi
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 17/73
TGBA to BA transformation
Let A = (Q, Σ, δ, q0, {F1, F2, . . . , Fk }) be a transition-based
generalized Büchi automaton (TGBA) with k ≥ 2 accepting
sets. We build an equivalent state-based Büchi automaton
B = (QB, Σ, δB, qB, F) as follows.
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 18/73
TGBA to BA transformation
Let A = (Q, Σ, δ, q0, {F1, F2, . . . , Fk }) be a transition-based
generalized Büchi automaton (TGBA) with k ≥ 2 accepting
sets. We build an equivalent state-based Büchi automaton
B = (QB, Σ, δB, qB, F) as follows.
we have k + 1 copies of A (levels 0 to k)
QB = Q × {0, . . . , k} |QB| ≤ (k + 1) · |Q|
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 19/73
TGBA to BA transformation
Let A = (Q, Σ, δ, q0, {F1, F2, . . . , Fk }) be a transition-based
generalized Büchi automaton (TGBA) with k ≥ 2 accepting
sets. We build an equivalent state-based Büchi automaton
B = (QB, Σ, δB, qB, F) as follows.
we have k + 1 copies of A (levels 0 to k)
QB = Q × {0, . . . , k} |QB| ≤ (k + 1) · |Q|
the initial state is on level 0 qB = (q0, 0)
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 20/73
TGBA to BA transformation
Let A = (Q, Σ, δ, q0, {F1, F2, . . . , Fk }) be a transition-based
generalized Büchi automaton (TGBA) with k ≥ 2 accepting
sets. We build an equivalent state-based Büchi automaton
B = (QB, Σ, δB, qB, F) as follows.
we have k + 1 copies of A (levels 0 to k)
QB = Q × {0, . . . , k} |QB| ≤ (k + 1) · |Q|
the initial state is on level 0 qB = (q0, 0)
all transitions from level 0 go to level 1
((q, 0), a, (p, 1)) ∈ δB ⇐⇒ (q, a, p) ∈ δ
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 21/73
TGBA to BA transformation
Let A = (Q, Σ, δ, q0, {F1, F2, . . . , Fk }) be a transition-based
generalized Büchi automaton (TGBA) with k ≥ 2 accepting
sets. We build an equivalent state-based Büchi automaton
B = (QB, Σ, δB, qB, F) as follows.
we have k + 1 copies of A (levels 0 to k)
QB = Q × {0, . . . , k} |QB| ≤ (k + 1) · |Q|
the initial state is on level 0 qB = (q0, 0)
all transitions from level 0 go to level 1
((q, 0), a, (p, 1)) ∈ δB ⇐⇒ (q, a, p) ∈ δ
on level i > 2 we wait for a transition from Fi and then
move to level (i + 1) (or 0 if i = k)
((q, i), a, (p, i)) ∈ δB ⇐⇒ (q, a, p) ∈ δ Fi
((q, i), a, (p, (i +1) mod (k +1))) ∈ δB ⇐⇒ (q, a, p) ∈ δ∩Fi
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 22/73
TGBA to BA transformation
Let A = (Q, Σ, δ, q0, {F1, F2, . . . , Fk }) be a transition-based
generalized Büchi automaton (TGBA) with k ≥ 2 accepting
sets. We build an equivalent state-based Büchi automaton
B = (QB, Σ, δB, qB, F) as follows.
we have k + 1 copies of A (levels 0 to k)
QB = Q × {0, . . . , k} |QB| ≤ (k + 1) · |Q|
the initial state is on level 0 qB = (q0, 0)
all transitions from level 0 go to level 1
((q, 0), a, (p, 1)) ∈ δB ⇐⇒ (q, a, p) ∈ δ
on level i > 2 we wait for a transition from Fi and then
move to level (i + 1) (or 0 if i = k)
((q, i), a, (p, i)) ∈ δB ⇐⇒ (q, a, p) ∈ δ Fi
((q, i), a, (p, (i +1) mod (k +1))) ∈ δB ⇐⇒ (q, a, p) ∈ δ∩Fi
the level 0 is accepting
F = Q × {0}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 23/73
TGBA to BA transformation
Let A = (Q, Σ, δ, q0, {F1, F2, . . . , Fk }) be a transition-based
generalized Büchi automaton (TGBA) with k ≥ 2 accepting
sets. We build an equivalent state-based Büchi automaton
B = (QB, Σ, δB, qB, F) as follows.
we have k + 1 copies of A (levels 0 to k)
QB = Q × {0, . . . , k} |QB| ≤ (k + 1) · |Q|
the initial state is on level 0 qB = (q0, 0)
all transitions from level 0 go to level 1
((q, 0), a, (p, 1)) ∈ δB ⇐⇒ (q, a, p) ∈ δ
on level i > 2 we wait for a transition from Fi and then
move to level (i + 1) (or 0 if i = k)
((q, i), a, (p, i)) ∈ δB ⇐⇒ (q, a, p) ∈ δ Fi
((q, i), a, (p, (i +1) mod (k +1))) ∈ δB ⇐⇒ (q, a, p) ∈ δ∩Fi
the level 0 is accepting
F = Q × {0}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 24/73
TGBA to BA transformation
Let A = (Q, Σ, δ, q0, {F1, F2, . . . , Fk }) be a transition-based
generalized Büchi automaton (TGBA) with k ≥ 2 accepting
sets. We build an equivalent state-based Büchi automaton
B = (QB, Σ, δB, qB, F) as follows.
we have k + 1 copies of A (levels 0 to k)
QB = Q × {0, . . . , k} |QB| ≤ (k + 1) · |Q|
the initial state is on level 0 qB = (q0, 0)
all transitions from level 0 go to level 1
((q, 0), a, (p, 1)) ∈ δB ⇐⇒ (q, a, p) ∈ δ
on level i > 2 we wait for a transition from Fi and then
move to level (i + 1) (or 0 if i = k)
((q, i), a, (p, i)) ∈ δB ⇐⇒ (q, a, p) ∈ δ Fi
((q, i), a, (p, (i +1) mod (k +1))) ∈ δB ⇐⇒ (q, a, p) ∈ δ∩Fi
the level 0 is accepting
F = Q × {0}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 25/73
LTL to BA translations
G¬explosion p q
explosion
¬explosion
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 26/73
LTL to BA translations
G¬explosion p q
explosion
¬explosion
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 27/73
LTL to BA translations
G¬explosion p q
explosion
¬explosion
applications in automata-based LTL model checking,
vacuity checking (checks trivial validity of a specification
formula), . . .
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 28/73
LTL to BA translations
G¬explosion p q
explosion
¬explosion
applications in automata-based LTL model checking,
vacuity checking (checks trivial validity of a specification
formula), . . .
many LTL→BA translations
LTL → generalized Büchi automata (GBA) → BA (Spin)
LTL → transition-based GBA (TGBA) → BA (Spot)
LTL → very weak alternating co-Büchi automata (VWAA) →
→ TGBA → BA (LTL2BA, LTL3BA)
. . .
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 29/73
LTL to BA translations
G¬explosion p q
explosion
¬explosion
applications in automata-based LTL model checking,
vacuity checking (checks trivial validity of a specification
formula), . . .
many LTL→BA translations
LTL → generalized Büchi automata (GBA) → BA (Spin)
LTL → transition-based GBA (TGBA) → BA (Spot)
LTL → very weak alternating co-Büchi automata (VWAA) →
→ TGBA → BA (LTL2BA, LTL3BA)
. . .
translations via alternating automata offer
size-reducing optimizations of alternating automata
smaller resulting BA (in some cases)
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 30/73
Alternating Automata
An alternating co-Büchi automaton is a tuple
A = (Q, Σ, δ, q0, F), where
Q is a finite set of states,
Σ is a finite alphabet,
δ : Q × Σ → 22Q
is a transition function,
q0 ∈ Q is an initial state,
F ⊆ Q is a set of co-Büchi-accepting states.
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 31/73
Alternating Automata – Example
p q
b
a
a
b
δ(p, {a, b}) = {{p}, {p, q}}
δ(q, {b}) = {∅}
δ(q, ∅) = {}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 32/73
Alternating Automata – Runs
A run of A over a word u = u(0)u(1) . . . is a Directed Acyclic
Graph (DAG) G = (V, E) where
V = Q × {0, 1, 2, . . .}
only the state q0 is in the level 0
for any (q, i) ∈ V it holds that
there is exactly one P ∈ δ(q, u(i)) such that
for each p ∈ P it holds that ((q, i), (p, i + 1)) ∈ E
no other nodes and edges are in V and E
p q
b
a
a
b
p
q
0 1 2 3 4 5 6
T0 T1 T2 T3 T4 T5
· · ·
{a} {a} {a} {a}{b} {b}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 33/73
Alternating Automata – Accepting
A run is accepting iff each its infinite branch contains only
finitely many states from F. [co-Büchi acceptance]
An automaton A accepts a word u iff there is an accepting run
of A on u. We set
L(A) = {u ∈ Σω
| A accepts u}.
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 34/73
Very Weak Alternating Automata
Intuitively, an alternating automaton is very weak, written VWAA
(or linear or 1-weak, written A1W) iff it contains no cycles
except selfloops.
Formally, let A = (Q, Σ, δ, q0, F) be an alternating automaton.
Automaton A is very weak iff there exists a partial order on Q
such that for all p, q ∈ Q and α ∈ Σ it holds:
p ∈ P, P ∈ δ(q, α) =⇒ p q
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 35/73
LTL → co-Büchi VWAA
LTL→VWAA
The main ideas:
states are subformulae of ϕ
build bottom-up
what needs to hold now and what in the next step
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 37/73
LTL→VWAA
The main ideas:
states are subformulae of ϕ
build bottom-up
what needs to hold now and what in the next step
Transition combination: Let D, D ⊆ 2Q be two sets of state
sets. We define their product D ⊗ D as
D ⊗ D = {P ∪ P | P ∈ D and P ∈ D }
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 38/73
Notes
standard Büchi automata are alternating Büchi automata
where each set in δ(p, l) is singleton
VWAA automata have the same expressive power as LTL
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 39/73
LTL→VWAA
Input: an LTL formula ϕ and an alphabet Σ = 2AP
for some finite AP ⊆ AP
Output: VWAA automaton A = (Q, Σ, δ, ϕ, F) accepting LΣ(ϕ)
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 40/73
LTL→VWAA
Input: an LTL formula ϕ and an alphabet Σ = 2AP
for some finite AP ⊆ AP
Output: VWAA automaton A = (Q, Σ, δ, ϕ, F) accepting LΣ(ϕ)
Q = {ψ | ψ is a subformula of ϕ}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 41/73
LTL→VWAA
Input: an LTL formula ϕ and an alphabet Σ = 2AP
for some finite AP ⊆ AP
Output: VWAA automaton A = (Q, Σ, δ, ϕ, F) accepting LΣ(ϕ)
Q = {ψ | ψ is a subformula of ϕ}
δ for l ∈ Σ is defined as follows
δ( , l) = {∅}
δ(⊥, l) = ∅
δ(a, l) = {∅} if a ∈ l, ∅ otherwise
δ(¬a, l) = {∅} if a /∈ l, ∅ otherwise
⊥
a
¬a
a
¬a
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 42/73
LTL→VWAA cont.
ψ1 ψ2
α1α2
A1A2
Ai
αi
Bj
βj
ψ1 ∧ ψ2
ψ1 ∨ ψ2
Ai Bj
αi ∧ βj
Ai Bj
βjαi
Xψ1 ψ1
Ai ∈ δ(ψ1, l) ⇐⇒ l |= αi
δ(ψ1 ∧ ψ2, l) = δ(ψ1, l) ⊗ δ(ψ2, l)
δ(ψ1 ∨ ψ2, l) = δ(ψ1, l) ∪ δ(ψ2, l)
δ(Xψ1, l) = {{ψ1}}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 43/73
LTL→VWAA cont.
ψ1 ψ2
α1α2
A1A2
Ai
αi
Bj
βj
ψ1 ∧ ψ2
ψ1 ∨ ψ2
Ai Bj
αi ∧ βj
Ai Bj
βjαi
Xψ1 ψ1
Ai ∈ δ(ψ1, l) ⇐⇒ l |= αi
δ(ψ1 ∧ ψ2, l) = δ(ψ1, l) ⊗ δ(ψ2, l)
δ(ψ1 ∨ ψ2, l) = δ(ψ1, l) ∪ δ(ψ2, l)
δ(Xψ1, l) = {{ψ1}}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 44/73
LTL→VWAA cont.
ψ1 ψ2
α1α2
A1A2
Ai
αi
Bj
βj
ψ1 ∧ ψ2
ψ1 ∨ ψ2
Ai Bj
αi ∧ βj
Ai Bj
βjαi
Xψ1 ψ1
Ai ∈ δ(ψ1, l) ⇐⇒ l |= αi
δ(ψ1 ∧ ψ2, l) = δ(ψ1, l) ⊗ δ(ψ2, l)
δ(ψ1 ∨ ψ2, l) = δ(ψ1, l) ∪ δ(ψ2, l)
δ(Xψ1, l) = {{ψ1}}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 45/73
LTL→VWAA cont.
ψ1 ψ2
α1α2
A1A2
Ai
αi
Bj
βj
ψ1 ∧ ψ2
ψ1 ∨ ψ2
Ai Bj
αi ∧ βj
Ai Bj
βjαi
Xψ1 ψ1
Ai ∈ δ(ψ1, l) ⇐⇒ l |= αi
δ(ψ1 ∧ ψ2, l) = δ(ψ1, l) ⊗ δ(ψ2, l)
δ(ψ1 ∨ ψ2, l) = δ(ψ1, l) ∪ δ(ψ2, l)
δ(Xψ1, l) = {{ψ1}}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 46/73
LTL→VWAA cont.
ψ1 ψ2
α1α2
A1A2
Ai
αi
Bj
βj
ψ1 ∧ ψ2
ψ1 ∨ ψ2
Ai Bj
αi ∧ βj
Ai Bj
βjαi
Xψ1 ψ1
Ai ∈ δ(ψ1, l) ⇐⇒ l |= αi
δ(ψ1 ∧ ψ2, l) = δ(ψ1, l) ⊗ δ(ψ2, l)
δ(ψ1 ∨ ψ2, l) = δ(ψ1, l) ∪ δ(ψ2, l)
δ(Xψ1, l) = {{ψ1}}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 47/73
LTL→VWAA cont.
ψ1 R ψ2
ψ1 U ψ2ψ1 U ψ2
Ai Bj
αi ∧ βj βi
Ai Bj
βjαi
δ(ψ1 R ψ2, l) = δ(ψ2, l) ⊗ δ(ψ1, l) ∪ {{ψ1 R ψ2}}
δ(ψ1 U ψ2, l) = δ(ψ2, l) ∪ δ(ψ1, l) ⊗ {{ψ1 U ψ2}}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 48/73
LTL→VWAA cont.
ψ1 R ψ2
ψ1 U ψ2ψ1 U ψ2
Ai Bj
αi ∧ βj βi
Ai Bj
βjαi
δ(ψ1 R ψ2, l) = δ(ψ2, l) ⊗ δ(ψ1, l) ∪ {{ψ1 R ψ2}}
δ(ψ1 U ψ2, l) = δ(ψ2, l) ∪ δ(ψ1, l) ⊗ {{ψ1 U ψ2}}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 49/73
LTL→VWAA cont.
ψ1 R ψ2
ψ1 U ψ2ψ1 U ψ2
Ai Bj
αi ∧ βj βi
Ai Bj
βjαi
δ(ψ1 R ψ2, l) = δ(ψ2, l) ⊗ δ(ψ1, l) ∪ {{ψ1 R ψ2}}
δ(ψ1 U ψ2, l) = δ(ψ2, l) ∪ δ(ψ1, l) ⊗ {{ψ1 U ψ2}}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 50/73
LTL→VWAA cont.
ψ1 R ψ2
ψ1 U ψ2ψ1 U ψ2
Ai Bj
αi ∧ βj βi
Ai Bj
βjαi
δ(ψ1 R ψ2, l) = δ(ψ2, l) ⊗ δ(ψ1, l) ∪ {{ψ1 R ψ2}}
δ(ψ1 U ψ2, l) = δ(ψ2, l) ∪ δ(ψ1, l) ⊗ {{ψ1 U ψ2}}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 51/73
LTL→VWAA cont.
ψ1 R ψ2
ψ1 U ψ2ψ1 U ψ2
Ai Bj
αi ∧ βj βi
Ai Bj
βjαi
δ(ψ1 R ψ2, l) = δ(ψ2, l) ⊗ δ(ψ1, l) ∪ {{ψ1 R ψ2}}
δ(ψ1 U ψ2, l) = δ(ψ2, l) ∪ δ(ψ1, l) ⊗ {{ψ1 U ψ2}}
F = {ψ1 U ψ2 | ψ1 U ψ2 is a subformula of ϕ}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 52/73
LTL→VWAA - Example
F (Ga ∧ Fb) ∨ Gc ∨ Gb
0 | F (Ga ∧ Fb) ∨ Gc ∨ Gb
4 | Ga
1 | Gb 2 | Gc
3 | Fb
a
b c
b
b c
a
a ∧ b
Ga ∧ Fb
a
a ∧ b
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 53/73
LTL→VWAA - Example
F (Ga ∧ Fb) ∨ Gc ∨ Gb
0 | F (Ga ∧ Fb) ∨ Gc ∨ Gb
4 | Ga
1 | Gb 2 | Gc
3 | Fb
a
b c
b
b c
a
a ∧ b
Ga ∧ Fb
a
a ∧ b
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 54/73
LTL→VWAA - Example
F (Ga ∧ Fb) ∨ Gc ∨ Gb
0 | F (Ga ∧ Fb) ∨ Gc ∨ Gb
4 | Ga
1 | Gb 2 | Gc
3 | Fb
a
b c
b
b c
a
a ∧ b
Ga ∧ Fb
a
a ∧ b
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 55/73
LTL→VWAA - Example
F (Ga ∧ Fb) ∨ Gc ∨ Gb
0 | F (Ga ∧ Fb) ∨ Gc ∨ Gb
4 | Ga
1 | Gb 2 | Gc
3 | Fb
a
b c
b
b c
a
a ∧ b
Ga ∧ Fb
a
a ∧ b
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 56/73
LTL→VWAA - Example
F (Ga ∧ Fb) ∨ Gc ∨ Gb
0 | F (Ga ∧ Fb) ∨ Gc ∨ Gb
4 | Ga
1 | Gb 2 | Gc
3 | Fb
a
b c
b
b c
a
a ∧ b
Ga ∧ Fb
a
a ∧ b
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 57/73
LTL→VWAA
Note that every infinite branch of a run of A has a suffix with
states of the form ψ1 U ψ2 or ψ1 R ψ2 (other states have no
loops and can appear at most once on a branch). F is defined
to ensure that ψ2 eventually holds for each ψ1 U ψ2.
Theorem
Given an LTL formula ϕ and an alphabet Σ, one can construct a
VWAA A accepting LΣ(ϕ) such that the number of states of A
is linear in the length of ϕ.
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 58/73
co-Büchi VWAA → TGBA
VWAA → TGBA
The key ideas:
the TGBA tracks (selected) possible runs of the VWAA
a run of the TGBA tracks states on each level of the run
(DAG)
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 60/73
VWAA → TGBA
The key ideas:
the TGBA tracks (selected) possible runs of the VWAA
a run of the TGBA tracks states on each level of the run
(DAG)
states of the TGBA are sets (conjunction) of states
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 61/73
VWAA → TGBA
The key ideas:
the TGBA tracks (selected) possible runs of the VWAA
a run of the TGBA tracks states on each level of the run
(DAG)
states of the TGBA are sets (conjunction) of states
once a state q is left by a branch, the branch never visits q
again
escaping f-transitions for an co-Büchi accepting state f
A transition (q, l, P) ∈ δ is q-escaping iff q /∈ P.
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 62/73
VWAA → TGBA
Input: a co-Büchi VWAA A = (Q, Σ, δ, q0, F) with k = |F|
Output: TGBA B = (Q , Σ, δ , q0, F) accepting L(A)
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 63/73
VWAA → TGBA
Input: a co-Büchi VWAA A = (Q, Σ, δ, q0, F) with k = |F|
Output: TGBA B = (Q , Σ, δ , q0, F) accepting L(A)
Q = 2Q
q0 = {q0}
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 64/73
VWAA → TGBA
Input: a co-Büchi VWAA A = (Q, Σ, δ, q0, F) with k = |F|
Output: TGBA B = (Q , Σ, δ , q0, F) accepting L(A)
Q = 2Q
q0 = {q0}
δ (P, l) = p∈P δ(p, l) is an unoptimized tr. function
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 65/73
VWAA → TGBA
Input: a co-Büchi VWAA A = (Q, Σ, δ, q0, F) with k = |F|
Output: TGBA B = (Q , Σ, δ , q0, F) accepting L(A)
Q = 2Q
q0 = {q0}
δ (P, l) = p∈P δ(p, l) is an unoptimized tr. function
F = {Tf ⊆ δ | f ∈ F} where
Tf = {(P1, l, P2) | f /∈ P2, or
(f, l, P ) ∈ δ, P ⊆ P2 and f /∈ P }
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 66/73
VWAA → TGBA
Input: a co-Büchi VWAA A = (Q, Σ, δ, q0, F) with k = |F|
Output: TGBA B = (Q , Σ, δ , q0, F) accepting L(A)
Q = 2Q
q0 = {q0}
δ (P, l) = p∈P δ(p, l) is an unoptimized tr. function
F = {Tf ⊆ δ | f ∈ F} where
Tf = {(P1, l, P2) | f /∈ P2, or
(f, l, P ) ∈ δ, P ⊆ P2 and f /∈ P }
is a relation on transitions of δ where
t1 t2 iff t1 = (P, l, P1) and t2 = (P, l, P2) and
P1 ⊆ P2 and
t1 ∈ Tf =⇒ t2 ∈ Tf for all f ∈ F
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 67/73
VWAA → TGBA
Input: a co-Büchi VWAA A = (Q, Σ, δ, q0, F) with k = |F|
Output: TGBA B = (Q , Σ, δ , q0, F) accepting L(A)
Q = 2Q
q0 = {q0}
δ (P, l) = p∈P δ(p, l) is an unoptimized tr. function
F = {Tf ⊆ δ | f ∈ F} where
Tf = {(P1, l, P2) | f /∈ P2, or
(f, l, P ) ∈ δ, P ⊆ P2 and f /∈ P }
is a relation on transitions of δ where
t1 t2 iff t1 = (P, l, P1) and t2 = (P, l, P2) and
P1 ⊆ P2 and
t1 ∈ Tf =⇒ t2 ∈ Tf for all f ∈ F
δ is the set of -minimal transitions of δ
F = {Tf ∩ δ | Tf ∈ F }
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 68/73
VWAA → TGBA – Example
0 | F (Ga ∧ Fb) ∨ Gc ∨ Gb
4 | Ga
1 | Gb 2 | Gc
3 | Fb
a
b c
b
b c
a
a ∧ b
{0}
{1} {2}
{3, 4}
{4}3
0
3
b
0
3
c
0
a
0
3
a ∧ b
0
3b
0
3 c
0
a
0
3 a ∧ b
03
a
P1 f
l
P2
if f /∈ P2 or
(f, l, P ), P ⊆ P2, f /∈ P
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 69/73
VWAA → TGBA – Example
0 | F (Ga ∧ Fb) ∨ Gc ∨ Gb
4 | Ga
1 | Gb 2 | Gc
3 | Fb
a
b c
b
b c
a
a ∧ b
{0}
{1} {2}
{3, 4}
{4}3
0
3
b
0
3
c
0
a
0
3
a ∧ b
0
3b
0
3 c
0
a
0
3 a ∧ b
03
a
P1 f
l
P2
if f /∈ P2 or
(f, l, P ), P ⊆ P2, f /∈ P
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 70/73
VWAA → TGBA – Example
0 | F (Ga ∧ Fb) ∨ Gc ∨ Gb
4 | Ga
1 | Gb 2 | Gc
3 | Fb
a
b c
b
b c
a
a ∧ b
{0}
{1} {2}
{3, 4}
{4}3
0
3
b
0
3
c
0
a
0
3
a ∧ b
0
3b
0
3 c
0
a
0
3 a ∧ b
03
a
P1 f
l
P2
if f /∈ P2 or
(f, l, P ), P ⊆ P2, f /∈ P
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 71/73
LTL→A1W
Theorem
Given an co-Büchi VWAA A = (Q, Σ, δ, q0, F), one can
construct a TGBA B with 2|Q| states that accepts L(A).
Corollary
Given an LTL formula ϕ and an alphabet Σ, one can construct a
TGBA B accepting LΣ(ϕ) such that the number of states of B is
2|ϕ|. Consequently, one can construct a BA C that accepts
LΣ(ϕ) and that has at most |ϕ| · 2|ϕ| states.
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 72/73
Coming next week
Partial order reduction
When can a state/transition be safely removed from a
Kripke structure?
What is a stuttering principle?
Can we effectively compute the reduction?
IA159 Formal Verification Methods: LTL→BA via Very Weak Alternating BA 73/73