IA159 Formal Verification Methods
LTL→BA via Alternating 1-Weak BA
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Focus and sources
Focus
linear temporal logic (LTL) and Büchi automata (BA)
alternating 1-weak Büchi automata (A1W)
translation LTL→A1W
translation A1W→BA
Source
M. Y. Vardi: An Automata-Theoretic Approach to Linear
Temporal Logic, LNCS 1043, Springer, 1995.
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 2/34
Syntax of LTL
Linear Temporal Logic (LTL) is defined by
ϕ ::= | a | ¬ϕ | ϕ1 ∧ ϕ2 | Xϕ | ϕ1 U ϕ2
where stands for true and a ranges over a countable set AP
of atomic propositions.
Abbreviations: ⊥ ≡ ¬ Fϕ ≡ U ϕ Gϕ ≡ ¬F¬ϕ
Terminology and intuitive meaning
Xa next • a • • • . . .
a U b until a a . . . a b • • • . . .
Fa eventually • • . . . • a • • • . . .
Ga always a a a a . . .
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 3/34
Semantics of LTL
Let Σ = 2AP , where AP ⊆ AP is a finite subset. We interpret
LTL on infinite words w = w(0)w(1) . . . ∈ Σω. By wi we denote
the suffix of w of the form w(i)w(i + 1)w(i + 2) . . ..
The validity of an LTL formula ϕ for w ∈ Σω, written w |= ϕ, is
defined as
w |=
w |= a iff a ∈ w(0)
w |= ¬ϕ iff w |= ϕ
w |= ϕ1 ∧ ϕ2 iff w |= ϕ1 ∧ w |= ϕ2
w |= Xϕ iff w1 |= ϕ
w |= ϕ1 U ϕ2 iff ∃i ∈ N0 : wi |= ϕ2 ∧ ∀ 0 ≤ j < i : wj |= ϕ1
Given an alphabet Σ, an LTL formula ϕ defines the language
LΣ
(ϕ) = {w ∈ Σω
| w |= ϕ}.
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 4/34
Büchi automata (BA)
A Büchi automaton (BA) is a tuple A = (Σ, Q, δ, q0, F) defined
precisely as a finite automaton. There are just two differences:
a Büchi automaton is interpreted over infinite words
a run is accepting if it visits some accepting state infinitely
often
p q
l
k, l
k
l
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 5/34
Büchi automata (BA)
A Büchi automaton (BA) is a tuple A = (Σ, Q, δ, q0, F) defined
precisely as a finite automaton. There are just two differences:
a Büchi automaton is interpreted over infinite words
a run is accepting if it visits some accepting state infinitely
often
p q
l
k, l
k
l
Accepts all infinite words over Σ = {k, l} with infinitely many l.
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 6/34
LTL→BA translations in general
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 → alternating 1-weak Büchi automata (A1W) → BA
LTL → A1W → TGBA → BA (LTL2BA, LTL3BA)
. . .
translations via alternating 1-weak automata offer
size-reducing optimizations of alternating 1-weak BA
smaller resulting BA (in some cases)
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 7/34
LTL→BA via alternating 1-weak BA
Alternating Büchi automata
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 8/34
Positive boolean formulae
Positive boolean formulae over set Q (B+(Q)) are defined as
ϕ ::= | ⊥ | q | ϕ1 ∧ ϕ2 | ϕ1 ∨ ϕ2
where stands for true, ⊥ stands for false, and q ranges
over Q.
S ⊆ Q is a model of ϕ ⇐⇒ the valuation assigning true just
to elements of S satisfies ϕ
S is a minimal model of ϕ ⇐⇒ S is a model of ϕ and no proper
(written S |= ϕ) subset of S is a model of ϕ
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 9/34
Examples of positive boolean formulae
formulae of B+({p, q, r}) (minimal) models
⊥ no model
∅, {p}, {q}, {r}, {p, q}, . . .
p ∧ q {p, q}, {p, q, r}
p ∨ (q ∧ r) {p}, {p, q}, {p, r}, {q, r}, {p, q, r}
p ∧ (q ∨ r) {p, q}, {p, r}, {p, q, r}
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 10/34
Examples of positive boolean formulae
formulae of B+({p, q, r}) (minimal) models
⊥ no model
∅, {p}, {q}, {r}, {p, q}, . . .
p ∧ q {p, q}, {p, q, r}
p ∨ (q ∧ r) {p}, {p, q}, {p, r}, {q, r}, {p, q, r}
p ∧ (q ∨ r) {p, q}, {p, r}, {p, q, r}
minimal models = clauses in disjunctive normal form
ϕ ≡
S|=ϕ
(
p∈S
p)
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 11/34
Alternating Büchi automata
An alternating Büchi automaton is a tuple A = (Σ, Q, δ, q0, F),
where
Σ is a finite alphabet,
Q is a finite set of states,
δ : Q × Σ → B+(Q) is a transition function,
q0 ∈ Q is an initial state,
F ⊆ Q is a set of accepting states.
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 12/34
Trees
A tree is a set T ⊆ N∗
0 such that if xc ∈ T, where x ∈ N∗
0 and
c ∈ N0, then also
x ∈ T and
xc ∈ T for all 0 ≤ c < c.
ε
0 1 2 3
00 01 20 21 22
210
T = { ε, 0, 1, 2, 3,
00, 01, 20,
21, 22, 210 }
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 13/34
Trees
A tree is a set T ⊆ N∗
0 such that if xc ∈ T, where x ∈ N∗
0 and
c ∈ N0, then also
x ∈ T and
xc ∈ T for all 0 ≤ c < c.
ε
0 1 2 3
00 01 20 21 22
210
T = { ε, 0, 1, 2, 3,
00, 01, 20,
21, 22, 210 }
A Q-labeled tree is a pair (T, r) of a tree T and a labeling
function r : T → Q.
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 14/34
Alternating Büchi automata: a run
A run of an alternating BA A = (Σ, Q, δ, q0, F) on word
w = w(0)w(1) . . . ∈ Σω is a Q-labeled tree (T, r) such that
r(ε) = q0 and
for each x ∈ T: {r(xc) | c ∈ N0, xc ∈ T} |= δ(r(x), w(|x|)).
A run (T, r) is accepting iff for each infinite path π in T it holds
that Inf(π) ∩ F = ∅, where Inf(π) is the set of all labels
(i.e. states) appearing on π infinitely often.
An automaton A accepts a word w iff there is an accepting run
of A on w. We set
L(A) = {w ∈ Σω
| A accepts w}.
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 15/34
Example of an alternating Büchi automaton
m
l
m
l
n
q3
q2
p
q1
n
n
l
m
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 16/34
Example of an alternating Büchi automaton
m
l
m
l
n
q3
q2
p
q1
n
n
l
m
Accepts the language l∗m(l + m + n)∗nω.
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 17/34
Alternating 1-weak Büchi automata (A1W)
Intuitively, an alternating BA is 1-weak (or linear or very weak,
written A1W or VWAA) if it contains no cycles except selfloops.
Formally, let A = (Σ, Q, δ, q0, F) be an alternating BA. For each
p ∈ Q we define the set of all successors of p as
Succ(p) = {q | ∃l ∈ Σ, S ⊆ Q : S ∪ {q} |= δ(p, l)}.
Automaton A is 1-weak (or linear or very weak) if there exists
a partial order ≤ on Q such that for all p, q ∈ Q it holds:
q ∈ Succ(p) =⇒ q ≤ p
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 18/34
Notes
standard Büchi automata are alternating Büchi automata
where each δ(p, l) is ⊥ or a disjunction of states
A1W automata have the same expressive power as LTL
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 19/34
LTL→BA via alternating 1-weak BA
LTL→A1W
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 20/34
LTL→A1W
Input: an LTL formula ϕ and an alphabet Σ = 2AP
for some finite AP ⊆ AP
Output: A1W automaton A = (Σ, Q, δ, qϕ, F) accepting LΣ(ϕ)
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 21/34
LTL→A1W
Input: an LTL formula ϕ and an alphabet Σ = 2AP
for some finite AP ⊆ AP
Output: A1W automaton A = (Σ, Q, δ, qϕ, F) accepting LΣ(ϕ)
Q = {qψ, q¬ψ | ψ is a subformula of ϕ}
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 22/34
LTL→A1W
Input: an LTL formula ϕ and an alphabet Σ = 2AP
for some finite AP ⊆ AP
Output: A1W automaton A = (Σ, Q, δ, qϕ, F) accepting LΣ(ϕ)
Q = {qψ, q¬ψ | ψ is a subformula of ϕ}
δ is defined as follows (where α ∈ B+(Q) satisfies α ≡ ¬α)
δ(q , l) = = ⊥
δ(qa, l) = if a ∈ l, ⊥ otherwise ⊥ =
δ(q¬ψ, l) = δ(qψ, l) q¬ψ = qψ
δ(qψ∧ρ, l) = δ(qψ, l) ∧ δ(qρ, l) qψ = q¬ψ
δ(qXψ, l) = qψ β ∧ γ = β ∨ γ
δ(qψUρ, l) = δ(qρ, l) ∨ (δ(qψ, l) ∧ qψUρ) β ∨ γ = β ∧ γ
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 23/34
LTL→A1W
Input: an LTL formula ϕ and an alphabet Σ = 2AP
for some finite AP ⊆ AP
Output: A1W automaton A = (Σ, Q, δ, qϕ, F) accepting LΣ(ϕ)
Q = {qψ, q¬ψ | ψ is a subformula of ϕ}
δ is defined as follows (where α ∈ B+(Q) satisfies α ≡ ¬α)
δ(q , l) = = ⊥
δ(qa, l) = if a ∈ l, ⊥ otherwise ⊥ =
δ(q¬ψ, l) = δ(qψ, l) q¬ψ = qψ
δ(qψ∧ρ, l) = δ(qψ, l) ∧ δ(qρ, l) qψ = q¬ψ
δ(qXψ, l) = qψ β ∧ γ = β ∨ γ
δ(qψUρ, l) = δ(qρ, l) ∨ (δ(qψ, l) ∧ qψUρ) β ∨ γ = β ∧ γ
F = {q¬(ψUρ) | ψ U ρ is a subformula of ϕ}
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 24/34
LTL→A1W
Note that every infinite path of a run of A has a suffix labeled
with a state of the form qψUρ or q¬(ψUρ) (other states have no
loops and can appear at most once on a path). F is defined to
prevent the first case: ψUρ is satisfied only if ρ eventually holds.
Theorem
Given an LTL formula ϕ and an alphabet Σ, one can construct
an A1W automaton A accepting LΣ(ϕ) and such that the
number of states of A is linear in the length of ϕ.
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 25/34
LTL→BA via alternating 1-weak BA
A1W→BA
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 26/34
A1W→BA
Input: an alternating BA A = (Σ, Q, δ, q0, F)
Output: a BA A = (Σ, Q , δ , q0, F ) accepting L(A)
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 27/34
A1W→BA
Input: an alternating BA A = (Σ, Q, δ, q0, F)
Output: a BA A = (Σ, Q , δ , q0, F ) accepting L(A)
Intuitively, A tracks states on each level of the computation tree
of A. Moreover, A has to divide the set of states into two sets:
states labeling paths with recent occurrence of an accepting
state, and states labeling the other paths.
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 28/34
A1W→BA
Input: an alternating BA A = (Σ, Q, δ, q0, F)
Output: a BA A = (Σ, Q , δ , q0, F ) accepting L(A)
Q = 2Q × 2Q
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 29/34
A1W→BA
Input: an alternating BA A = (Σ, Q, δ, q0, F)
Output: a BA A = (Σ, Q , δ , q0, F ) accepting L(A)
Q = 2Q × 2Q
q0 = ({q0}, ∅)
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 30/34
A1W→BA
Input: an alternating BA A = (Σ, Q, δ, q0, F)
Output: a BA A = (Σ, Q , δ , q0, F ) accepting L(A)
Q = 2Q × 2Q
q0 = ({q0}, ∅)
δ ((U, V), l) is defined as:
if U = ∅ then
δ ((U, V), l) = {(U , V ) | ∃X, Y ⊆ Q such that
X |= q∈U δ(q, l) and
Y |= q∈V δ(q, l) and
U = X F and V = Y ∪ (X ∩ F)}
if U = ∅ then
δ ((∅, V), l) = {(U , V ) | ∃Y ⊆ Q such that
Y |= q∈V δ(q, l) and
U = Y F and V = Y ∩ F)}
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 31/34
A1W→BA
Input: an alternating BA A = (Σ, Q, δ, q0, F)
Output: a BA A = (Σ, Q , δ , q0, F ) accepting L(A)
Q = 2Q × 2Q
q0 = ({q0}, ∅)
δ ((U, V), l) is defined as:
if U = ∅ then
δ ((U, V), l) = {(U , V ) | ∃X, Y ⊆ Q such that
X |= q∈U δ(q, l) and
Y |= q∈V δ(q, l) and
U = X F and V = Y ∪ (X ∩ F)}
if U = ∅ then
δ ((∅, V), l) = {(U , V ) | ∃Y ⊆ Q such that
Y |= q∈V δ(q, l) and
U = Y F and V = Y ∩ F)}
F = {∅} × 2Q
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 32/34
LTL→A1W
Theorem
Given an alternating BA A = (Σ, Q, δ, q0, F), one can construct
a BA A accepting L(A) and such that the number of states of
A is 2O(|Q|).
Corollary
Given an LTL formula ϕ and an alphabet Σ, one can construct a
BA A accepting LΣ(ϕ) and such that the number of states of
A is 2O(|ϕ|).
IA159 Formal Verification Methods: LTL→BA via Alternating 1-Weak BA 33/34
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 Alternating 1-Weak BA 34/34