IA169 Model Checking
Automata-based LTL model checking
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Automata-based LTL model checking
system K specification formula φ
automaton AK
representing runs of K
automaton A¬φ
representing runs violating φ
Do AK and A¬φ represent
disjoint sets of runs?
YES,
all runs of K satisfy φ
NO + counterexample,
i.e. a run of K violating φ
IA169 Model Checking: Automata-based LTL model checking 2/130
Agenda and sources
agenda
formalization of the state-based LTL model checking problem:
(fair) Kripke structure and LTL
Büchi automata (BA) and generalized Büchi automata (GBA)
transformation of finite (fair) Kripke structures to (G)BA
translation of LTL to BA via self-loop alternating automata
algorithms checking disjointness of AK and A¬φ
algorithm based on SCC decomposition
nested DFS algorithm
optimizations
action-based version of LTL model checking
sources
Chapter 7 of E. M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith:
Model Checking, Second Edition, MIT, 2018.
M. Y. Vardi: An Automata-Theoretic Approach to Linear Temporal Logic,
LNCS 1043, Springer, 1995.
IA169 Model Checking: Automata-based LTL model checking 3/130
Formalization of the state-based LTL model checking problem
Atomic propositions
atomic propositions
basic observable properties of each state of the system
for example: x ≥ y + 10, z is even, gate is open, program is at line 10
the validity of each atomic proposition in each state of the system has to be
fully determined by the state
specification talks only about validity of atomic proposition during system runs
AP denotes a countable set of atomic propositions
IA169 Model Checking: Automata-based LTL model checking 5/130
Atomic propositions
atomic propositions
basic observable properties of each state of the system
for example: x ≥ y + 10, z is even, gate is open, program is at line 10
the validity of each atomic proposition in each state of the system has to be
fully determined by the state
specification talks only about validity of atomic proposition during system runs
AP denotes a countable set of atomic propositions
basic formalism for state-based systems is a Kripke structure
IA169 Model Checking: Automata-based LTL model checking 6/130
Kripke structure
Definition (Kripke structure)
A Kripke structure is a tuple K = (S, T, S0, L), where
S is a set of states,
T ⊆ S × S is a transition relation,
S0 ⊆ S is a set of initial states,
L : S → 2AP is a labeling function associating to each state s ∈ S the set of
atomic propositions that are true in s.
IA169 Model Checking: Automata-based LTL model checking 7/130
Kripke structure
Definition (Kripke structure)
A Kripke structure is a tuple K = (S, T, S0, L), where
S is a set of states,
T ⊆ S × S is a transition relation,
S0 ⊆ S is a set of initial states,
L : S → 2AP is a labeling function associating to each state s ∈ S the set of
atomic propositions that are true in s.
Kripke structures are typically described in an implicit way
formats for implicit description typically offer
programs, processes, finite-state machines
synchronous or asynchronous composition
communication and synchronization mechanisms
nondeterminism or inputs
IA169 Model Checking: Automata-based LTL model checking 8/130
Example in the modelling language DVE
channel {byte} c[0];
process A {
byte a;
state q1,q2,q3;
init q1;
trans
q1→q2 { effect a=a+1; },
q2→q3 { effect a=a+1; },
q3→q1 { sync c!a; effect a=0; };
}
process B {
byte b,x;
state p1,p2,p3,p4;
init p1;
trans
p1→p2 { effect b=b+1; },
p2→p3 { effect b=b+1; },
p3→p4 { sync c?x; },
p4→p1 { guard x==b; effect b=0, x=0; };
}
system async;
IA169 Model Checking: Automata-based LTL model checking 9/130
Example of a simple mutual exclusion system
cobegin P0 ∥ P1 coend
P0:: l0: while true do
NC0: wait (turn = 0);
CR0: turn := 1
end while
P1:: l1: while true do
NC1: wait (turn = 1);
CR1: turn := 0
end while
assume that turn is initially 0 or 1
IA169 Model Checking: Automata-based LTL model checking 10/130
Example of a simple mutual exclusion system
cobegin P0 ∥ P1 coend
P0:: l0: while true do
NC0: wait (turn = 0);
CR0: turn := 1
end while
P1:: l1: while true do
NC1: wait (turn = 1);
CR1: turn := 0
end while
assume that turn is initially 0 or 1
turn = 0
⊥, ⊥
turn = 0
l0, l1
turn = 0
l0, NC1
turn = 0
NC0, l1
turn = 0
NC0, NC1
turn = 0
CR0, l1
turn = 0
CR0, NC1
turn = 1
⊥, ⊥
turn = 1
l0, l1
turn = 1
l0, NC1
turn = 1
NC0, l1
turn = 1
l0, CR1
turn = 1
NC0, NC1
turn = 1
NC0, CR1
IA169 Model Checking: Automata-based LTL model checking 11/130
Run of a Kripke structure
Definition (run)
Let K = (S, T, S0, L) be a Kripke structure. A run of K is an infinite sequence
π = s0s1s2 . . . of states such that s0 ∈ S0 and (si, si+1) ∈ T holds for each i ≥ 0.
IA169 Model Checking: Automata-based LTL model checking 12/130
Run of a Kripke structure
Definition (run)
Let K = (S, T, S0, L) be a Kripke structure. A run of K is an infinite sequence
π = s0s1s2 . . . of states such that s0 ∈ S0 and (si, si+1) ∈ T holds for each i ≥ 0.
linear time model checking decides whether all runs satisfy the specification
the set of infinite sequences of states is denoted by Sω
to consider also finite runs, we can define a run as a maximal sequence
π = s0s1s2 · · · ∈ S+ ∪ Sω of successive states starting in an initial state,
where maximal means infinite or ending in a state without any successor
it is usually assumed that there are no states without any successors: any
system can be transformed to this form by adding self-loops to such states
IA169 Model Checking: Automata-based LTL model checking 13/130
Linear temporal logic (LTL)
Definition (linear temporal logic, LTL)
Formulae of Linear Temporal Logic (LTL) are defined by
φ ::= ⊤ | a | ¬φ | φ1 ∧ φ2 | Xφ | φ1 U φ2
where ⊤ stands for true and a ranges over a countable set AP.
IA169 Model Checking: Automata-based LTL model checking 14/130
Linear temporal logic (LTL)
Definition (linear temporal logic, LTL)
Formulae of Linear Temporal Logic (LTL) are defined by
φ ::= ⊤ | a | ¬φ | φ1 ∧ φ2 | Xφ | φ1 U φ2
where ⊤ stands for true and a ranges over a countable set AP.
abbreviations and alternative notation
⊥ ≡ ¬⊤
φ ∨ ψ ≡ ¬(¬φ ∧ ¬ψ)
φ ⇒ ψ ≡ ¬φ ∨ ψ
φ ⇔ ψ ≡ φ ⇒ ψ ∧ φ ⇐ ψ
⃝φ ≡ Xφ
Fφ ≡ ♢φ ≡ ⊤ U φ
Gφ ≡ □φ ≡ ¬F¬φ
IA169 Model Checking: Automata-based LTL model checking 15/130
Intuitive semantic of LTL
operator name intuitive meaning
Xa next • a • • • . . .
a U b until a a . . . a b • • • . . .
Fa eventually • • . . . • a • • • . . .
Ga always or globally a a a a . . .
IA169 Model Checking: Automata-based LTL model checking 16/130
Semantics of LTL
we interpret LTL on infinite words w = w(0)w(1) . . . ∈ (2AP)ω
by wi we denote the suffix of w of the form w(i)w(i + 1)w(i + 2) . . .
IA169 Model Checking: Automata-based LTL model checking 17/130
Semantics of LTL
we interpret LTL on infinite words w = w(0)w(1) . . . ∈ (2AP)ω
by wi we denote the suffix of w of the form w(i)w(i + 1)w(i + 2) . . .
Definition
The relation w |= φ, meaning that w satisfies φ, is defined inductively as follows.
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 ≥ 0 . wi |= φ2 ∧ ∀ 0 ≤ j < i . wj |= φ1
IA169 Model Checking: Automata-based LTL model checking 18/130
Semantics of LTL
we interpret LTL on infinite words w = w(0)w(1) . . . ∈ (2AP)ω
by wi we denote the suffix of w of the form w(i)w(i + 1)w(i + 2) . . .
Definition
The relation w |= φ, meaning that w satisfies φ, is defined inductively as follows.
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 ≥ 0 . wi |= φ2 ∧ ∀ 0 ≤ j < i . wj |= φ1
By AP(φ) we denote the set of atomic propositions appearing in φ.
The language of φ is defined as L(φ) = {w ∈ Σω | w |= φ}, where Σ = 2AP(φ).
IA169 Model Checking: Automata-based LTL model checking 19/130
The goal of LTL model checking
Definition
Let K = (S, T, S0, L) be a Kripke structure and φ be an LTL formula.
A run π = s0s1s2 . . . of K satisfies φ, written π |= φ, if L(s0)L(s1)L(s2) . . . |= φ.
K satisfies φ, written K |= φ, if π |= φ holds for every run π of K.
IA169 Model Checking: Automata-based LTL model checking 20/130
The goal of LTL model checking
Definition
Let K = (S, T, S0, L) be a Kripke structure and φ be an LTL formula.
A run π = s0s1s2 . . . of K satisfies φ, written π |= φ, if L(s0)L(s1)L(s2) . . . |= φ.
K satisfies φ, written K |= φ, if π |= φ holds for every run π of K.
Given a Kripke structure K and an LTL formula φ, the goal of LTL model checking
is to decide whether K |= φ or not. In the negative case, model checking should
provide a counterexample, i.e., a run π of K such that π ̸|= φ.
IA169 Model Checking: Automata-based LTL model checking 21/130
Example
turn = 0
⊥, ⊥
turn = 0
l0, l1
turn = 0
l0, NC1
turn = 0
NC0, l1
turn = 0
NC0, NC1
turn = 0
CR0, l1
turn = 0
CR0, NC1
turn = 1
⊥, ⊥
turn = 1
l0, l1
turn = 1
l0, NC1
turn = 1
NC0, l1
turn = 1
l0, CR1
turn = 1
NC0, NC1
turn = 1
NC0, CR1
which formulae are satisfied?
G¬(CR0 ∧ CR1)
GFturn = 0 ∧ GFturn = 1
IA169 Model Checking: Automata-based LTL model checking 22/130
Extension with fairness
fairness allows to add additional restrictions on the system runs
can reflect properties of process schedulers
IA169 Model Checking: Automata-based LTL model checking 23/130
Extension with fairness
fairness allows to add additional restrictions on the system runs
can reflect properties of process schedulers
Definition (fair Kripke structure)
A fair Kripke structure is a tuple K = (S, T, S0, L, F), where (S, T, S0, L) is a
Kripke structure and F = {F1, F2, . . . , Fn} is a finite set of fairness constraints such
that Fi ⊆ S for each 1 ≤ i ≤ n.
A sequence π = s0s1s2 ∈ Sω is called a fair run of K if it is a run of (S, T, S0, L)
and it visits each Fi ∈ F infinitely often, i.e., sj ∈ Fi for infinitely many j.
K fairly satisfies an LTL formula φ, written K |=F φ, if each fair run of K satisfies φ.
IA169 Model Checking: Automata-based LTL model checking 24/130
Extension with fairness
fairness allows to add additional restrictions on the system runs
can reflect properties of process schedulers
Definition (fair Kripke structure)
A fair Kripke structure is a tuple K = (S, T, S0, L, F), where (S, T, S0, L) is a
Kripke structure and F = {F1, F2, . . . , Fn} is a finite set of fairness constraints such
that Fi ⊆ S for each 1 ≤ i ≤ n.
A sequence π = s0s1s2 ∈ Sω is called a fair run of K if it is a run of (S, T, S0, L)
and it visits each Fi ∈ F infinitely often, i.e., sj ∈ Fi for infinitely many j.
K fairly satisfies an LTL formula φ, written K |=F φ, if each fair run of K satisfies φ.
add reasonable fairness constraint to the mutual exclusion system
IA169 Model Checking: Automata-based LTL model checking 25/130
Büchi automata (BA) and generalized Büchi automata (GBA)
Büchi automaton (BA)
Definition (Büchi automaton, BA)
A Büchi automaton (BA) is a tuple A = (Q, Σ, δ, Q0, F), where
Q is a finite set of states,
Σ is a finite alphabet,
δ ⊆ Q × Σ × Q is a transition relation,
Q0 ⊆ Q is a set of initial states,
F ⊆ Q is a set of accepting states.
IA169 Model Checking: Automata-based LTL model checking 27/130
Büchi automaton (BA)
Definition (Büchi automaton, BA)
A Büchi automaton (BA) is a tuple A = (Q, Σ, δ, Q0, F), where
Q is a finite set of states,
Σ is a finite alphabet,
δ ⊆ Q × Σ × Q is a transition relation,
Q0 ⊆ Q is a set of initial states,
F ⊆ Q is a set of accepting states.
we write p
a
→ q instead of (p, a, q) ∈ δ
a
b
b
a
IA169 Model Checking: Automata-based LTL model checking 28/130
Büchi automaton (BA)
for an arbitrary infinite sequence σ, by inf(σ) we denote the set of its elements
that appear infinitely often in σ
IA169 Model Checking: Automata-based LTL model checking 29/130
Büchi automaton (BA)
for an arbitrary infinite sequence σ, by inf(σ) we denote the set of its elements
that appear infinitely often in σ
Definition (run, language)
Let A = (Q, Σ, δ, Q0, F) be a BA.
A run of A over an infinite word w = a1a2 . . . ∈ Σω is a sequence of states
π = s0s1 . . . ∈ Qω satisfying s0 ∈ Q0 and si−1
ai
→ si for each i ≥ 1.
A run π is accepting if inf(π) ∩ F ̸= ∅.
A word w ∈ Σω is accepted by A if there exists an accepting run of A over w.
A language represented by A is the set L(A) ⊆ Σω of words accepted by A.
IA169 Model Checking: Automata-based LTL model checking 30/130
Büchi automaton (BA)
for an arbitrary infinite sequence σ, by inf(σ) we denote the set of its elements
that appear infinitely often in σ
Definition (run, language)
Let A = (Q, Σ, δ, Q0, F) be a BA.
A run of A over an infinite word w = a1a2 . . . ∈ Σω is a sequence of states
π = s0s1 . . . ∈ Qω satisfying s0 ∈ Q0 and si−1
ai
→ si for each i ≥ 1.
A run π is accepting if inf(π) ∩ F ̸= ∅.
A word w ∈ Σω is accepted by A if there exists an accepting run of A over w.
A language represented by A is the set L(A) ⊆ Σω of words accepted by A.
L(A) = {w ∈ {a, b}ω | a ∈ inf(w)}
a
b
b
a
IA169 Model Checking: Automata-based LTL model checking 31/130
Properties of Büchi automata
languages represented by Büchi automata are called ω-regular
the class of ω-regular languages is closed under ∪, ∩, and complement
(though complementation of Büchi automata is highly non-trivial)
deterministic Büchi automata are less expressive than nondeterministic ones:
for example {a, b}∗.{b}ω cannot be described by any deterministic BA
L(A) = {a, b}∗.{b}ωb
a, b b
IA169 Model Checking: Automata-based LTL model checking 32/130
Properties of Büchi automata
languages represented by Büchi automata are called ω-regular
the class of ω-regular languages is closed under ∪, ∩, and complement
(though complementation of Büchi automata is highly non-trivial)
deterministic Büchi automata are less expressive than nondeterministic ones:
for example {a, b}∗.{b}ω cannot be described by any deterministic BA
L(A) = {a, b}∗.{b}ωb
a, b b
the class of languages represented by deterministic Büchi automata is not
closed under complement
L(B) = {w ∈ {a, b}ω | a ∈ inf(w)}
L(B) = {a, b}ω ∖ L(A)
a
b
b
a
IA169 Model Checking: Automata-based LTL model checking 33/130
Generalized Büchi automaton (GBA)
Definition (generalized Büchi automaton, GBA)
A generalized Büchi automaton (GBA) is a tuple A = (Q, Σ, δ, Q0, F), where
Q, Σ, δ, Q0 have the same meaning as in BA and F = {F1, . . . , Fn} is a finite set of
accepting sets satisfying Fi ⊆ Q for each Fi ∈ F.
The definition of run is the same as for BA.
A run π is accepting if for each Fi ∈ F it holds inf(π) ∩ Fi ̸= ∅.
The definition of an accepted word and language is the same as for BA.
IA169 Model Checking: Automata-based LTL model checking 34/130
Generalized Büchi automaton (GBA)
Definition (generalized Büchi automaton, GBA)
A generalized Büchi automaton (GBA) is a tuple A = (Q, Σ, δ, Q0, F), where
Q, Σ, δ, Q0 have the same meaning as in BA and F = {F1, . . . , Fn} is a finite set of
accepting sets satisfying Fi ⊆ Q for each Fi ∈ F.
The definition of run is the same as for BA.
A run π is accepting if for each Fi ∈ F it holds inf(π) ∩ Fi ̸= ∅.
The definition of an accepted word and language is the same as for BA.
each BA (Q, Σ, δ, Q0, F) can be seen as a GBA (Q, Σ, δ, Q0, {F})
each GBA can be transformed into a BA representing the same language
GBAs can be more succinct
IA169 Model Checking: Automata-based LTL model checking 35/130
Transformation of finite (fair) Kripke structures to (G)BA
Kripke structure → BA
since now on, we consider only Kripke structures K with finitely many states
assume that we know the set AP(φ), which is always finite
when deciding K
?
|= φ, we can ignore atomic propositions outside AP(φ)
we transform K into a Büchi automaton AK with alphabet Σ = 2AP(φ)
representing the language
LΣ
K = {a0a1a2 . . . ∈ Σω | there exists a run s0s1s2 . . . of K such that
ai = L(si) ∩ AP(φ) for each i ≥ 0}
corresponding to runs of K projected to AP(φ)
IA169 Model Checking: Automata-based LTL model checking 37/130
Kripke structure → BA
input: a set AP(φ) and a Kripke structure K = (S, T, S0, L)
output: a BA AK = (S, 2AP(φ), δ, S0, S) representing LΣ
K , where Σ = 2AP(φ)
δ = {(p, a, q) | (p, q) ∈ T and a = L(p) ∩ AP(φ)}
IA169 Model Checking: Automata-based LTL model checking 38/130
Kripke structure → BA
input: a set AP(φ) and a Kripke structure K = (S, T, S0, L)
output: a BA AK = (S, 2AP(φ), δ, S0, S) representing LΣ
K , where Σ = 2AP(φ)
δ = {(p, a, q) | (p, q) ∈ T and a = L(p) ∩ AP(φ)}
go
go
go,pf pf
AP(φ) = {go}
IA169 Model Checking: Automata-based LTL model checking 39/130
Kripke structure → BA
input: a set AP(φ) and a Kripke structure K = (S, T, S0, L)
output: a BA AK = (S, 2AP(φ), δ, S0, S) representing LΣ
K , where Σ = 2AP(φ)
δ = {(p, a, q) | (p, q) ∈ T and a = L(p) ∩ AP(φ)}
go
go
go,pf pf
AP(φ) = {go}
{go}
∅
{go}{go}
{go}
∅
{go}{go}
{go}
∅
IA169 Model Checking: Automata-based LTL model checking 40/130
Fair Kripke structure → GBA
similarly, we transform a fair Kripke structure K into a generalized Büchi
automaton AK with alphabet Σ = 2AP(φ) representing the language
LΣ
K = {a0a1a2 . . . ∈ Σω | there exists a fair run s0s1s2 . . . of K such that
ai = L(si) ∩ AP(φ) for each i ≥ 0}
IA169 Model Checking: Automata-based LTL model checking 41/130
Fair Kripke structure → GBA
similarly, we transform a fair Kripke structure K into a generalized Büchi
automaton AK with alphabet Σ = 2AP(φ) representing the language
LΣ
K = {a0a1a2 . . . ∈ Σω | there exists a fair run s0s1s2 . . . of K such that
ai = L(si) ∩ AP(φ) for each i ≥ 0}
input: a set AP(φ) and a fair Kripke structure K = (S, T, S0, L, F)
output: a GBA AK = (S, 2AP(φ), δ, S0, F) representing LΣ
K , where Σ = 2AP(φ)
δ = {(p, a, q) | (p, q) ∈ T and a = L(p) ∩ AP(φ)}
IA169 Model Checking: Automata-based LTL model checking 42/130
Translation of LTL to BA via self-loop alternating automata
LTL → BA translations in general
translates an LTL formula φ into a BA Aφ accepting L(φ)
many LTL → BA translations
LTL → GBA → BA (Spin)
LTL → transition-based GBA (TGBA) → BA (Spot)
LTL → self-loop alternating BA → TGBA → BA (LTL2BA, LTL3BA)
LTL → self-loop alternating BA → BA
. . .
translations via self-loop alternating automata offer
size-reducing optimizations of self-loop alternating automata
smaller resulting BA (in some cases)
IA169 Model Checking: Automata-based LTL model checking 44/130
Translation of LTL to BA via self-loop alternating automata
Alternating automata
Positive Boolean formulae
Definition (positive boolean formulae)
Positive Boolean formulae over set Q, denoted with B+(Q), are defined by
φ ::= ⊤ | ⊥ | q | φ1 ∧ φ2 | φ1 ∨ φ2
where ⊤ stands for true, ⊥ stands for false, and q ranges over Q.
IA169 Model Checking: Automata-based LTL model checking 46/130
Positive Boolean formulae
Definition (positive boolean formulae)
Positive Boolean formulae over set Q, denoted with B+(Q), are defined by
φ ::= ⊤ | ⊥ | 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 φ
IA169 Model Checking: Automata-based LTL model checking 47/130
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}
IA169 Model Checking: Automata-based LTL model checking 48/130
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 correspond to clauses in disjunctive normal form
(without superfluous clauses)
φ ≡
S|=φ
(
p∈S
p)
IA169 Model Checking: Automata-based LTL model checking 49/130
Alternating Büchi automaton
Definition (alternating Büchi automaton)
An alternating Büchi automaton is a tuple A = (Q, Σ, δ, Q0, F), where
Q is a finite set of states,
Σ is a finite alphabet,
δ : Q × Σ → B+(Q) is a transition function,
Q0 ⊆ Q is a set of initial states,
F ⊆ Q is a set of accepting states.
IA169 Model Checking: Automata-based LTL model checking 50/130
Trees
Definition (tree, Q-labeled tree)
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.
IA169 Model Checking: Automata-based LTL model checking 51/130
Trees
Definition (tree, Q-labeled tree)
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}
IA169 Model Checking: Automata-based LTL model checking 52/130
Trees
Definition (tree, Q-labeled tree)
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.
A Q-labeled tree is a pair (T, r) of a tree T and a labeling function r : T → Q.
ε
0 1 2 3
00 01 20 21 22
210
T = {ε, 0, 1, 2, 3, 00, 01,
20, 21, 22, 210}
IA169 Model Checking: Automata-based LTL model checking 53/130
Alternating Büchi automaton
Definition (run, language)
A run of an alternating BA A = (Q, Σ, δ, Q0, F) on word w = a0a1 . . . ∈ Σω is a
Q-labeled tree (T, r) such that
r(ε) ∈ Q0 and
for each x ∈ T: {r(xc) | c ∈ N0, xc ∈ T} |= δ(r(x), a|x|).
A run (T, r) is accepting iff for each infinite branch σ in T it holds that infinitely
many nodes of the branch are labeled with a state in F.
A word w ∈ Σω is accepted by A iff there exists an accepting run of A over w.
A language represented by A is the set L(A) ⊆ Σω of words accepted by A.
IA169 Model Checking: Automata-based LTL model checking 54/130
Example of an alternating Büchi automaton
p
q1 q2
q3
a b
a
b
a, b, c
c
c
IA169 Model Checking: Automata-based LTL model checking 55/130
Example of an alternating Büchi automaton
p
q1 q2
q3
a b
a
b
a, b, c
c
c
L(A) = {a}∗.{b}.{a, b, c}∗.{c}ω
IA169 Model Checking: Automata-based LTL model checking 56/130
Self-loop alternating Büchi automaton
Intuitively, an alternating BA is self-loop (or 1-weak or linear or very weak, written
SLAA or A1W or VWAA) if it contains no cycles except self-loops.
IA169 Model Checking: Automata-based LTL model checking 57/130
Self-loop alternating Büchi automaton
Intuitively, an alternating BA is self-loop (or 1-weak or linear or very weak, written
SLAA or A1W or VWAA) if it contains no cycles except self-loops.
Definition (self-loop alternating BA)
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 | ∃a ∈ Σ, S ⊆ Q : S ∪ {q} |= δ(p, a)}.
Automaton A is self-loop (or 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
IA169 Model Checking: Automata-based LTL model checking 58/130
Notes
standard Büchi automata are alternating Büchi automata where each δ(p, a)
is ⊥ or a disjunction of states
self-loop alternating BA have the same expressive power as LTL
IA169 Model Checking: Automata-based LTL model checking 59/130
Translation of LTL to BA via self-loop alternating automata
LTL → self-loop alternating BA
LTL → self-loop alternating BA
input: an LTL formula φ
output: self-loop alternating BA A = (Q, Σ, δ, {qφ}, F) accepting L(φ)
IA169 Model Checking: Automata-based LTL model checking 61/130
LTL → self-loop alternating BA
input: an LTL formula φ
output: self-loop alternating BA A = (Q, Σ, δ, {qφ}, F) accepting L(φ)
Q = {qψ, q¬ψ | ψ is a subformula of φ}
Σ = 2AP(φ)
IA169 Model Checking: Automata-based LTL model checking 62/130
LTL → self-loop alternating BA
input: an LTL formula φ
output: self-loop alternating BA A = (Q, Σ, δ, {qφ}, F) accepting L(φ)
Q = {qψ, q¬ψ | ψ is a subformula of φ}
Σ = 2AP(φ)
δ 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ρ) β ∨ γ = β ∧ γ
IA169 Model Checking: Automata-based LTL model checking 63/130
LTL → self-loop alternating BA
input: an LTL formula φ
output: self-loop alternating BA A = (Q, Σ, δ, {qφ}, F) accepting L(φ)
Q = {qψ, q¬ψ | ψ is a subformula of φ}
Σ = 2AP(φ)
δ 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 φ}
IA169 Model Checking: Automata-based LTL model checking 64/130
LTL → self-loop alternating BA
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 φ, one can construct an self-loop alternating BA A accepting
L(φ) and such that the number of states of A is linear in the length of φ.
IA169 Model Checking: Automata-based LTL model checking 65/130
Translation of LTL to BA via self-loop alternating automata
Self-loop alternating BA → BA
Self-loop alternating BA → BA
input: a self-loop alternating BA A = (Q, Σ, δ, Q0, F)
output: a BA A′ = (Q′, Σ, δ′, Q′
0, F′) accepting L(A)
IA169 Model Checking: Automata-based LTL model checking 67/130
Self-loop alternating BA → BA
input: a self-loop alternating BA A = (Q, Σ, δ, Q0, F)
output: a BA A′ = (Q′, Σ, δ′, Q′
0, 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.
IA169 Model Checking: Automata-based LTL model checking 68/130
Self-loop alternating BA → BA
input: a self-loop alternating BA A = (Q, Σ, δ, Q0, F)
output: a BA A′ = (Q′, Σ, δ′, Q′
0, F′) accepting L(A)
Q′ = 2Q × 2Q
IA169 Model Checking: Automata-based LTL model checking 69/130
Self-loop alternating BA → BA
input: a self-loop alternating BA A = (Q, Σ, δ, Q0, F)
output: a BA A′ = (Q′, Σ, δ′, Q′
0, F′) accepting L(A)
Q′ = 2Q × 2Q
Q′
0 = {({q0}, ∅) | q0 ∈ Q0}
IA169 Model Checking: Automata-based LTL model checking 70/130
Self-loop alternating BA → BA
input: a self-loop alternating BA A = (Q, Σ, δ, Q0, F)
output: a BA A′ = (Q′, Σ, δ′, Q′
0, F′) accepting L(A)
Q′ = 2Q × 2Q
Q′
0 = {({q0}, ∅) | 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)}
IA169 Model Checking: Automata-based LTL model checking 71/130
Self-loop alternating BA → BA
input: a self-loop alternating BA A = (Q, Σ, δ, Q0, F)
output: a BA A′ = (Q′, Σ, δ′, Q′
0, F′) accepting L(A)
Q′ = 2Q × 2Q
Q′
0 = {({q0}, ∅) | 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
IA169 Model Checking: Automata-based LTL model checking 72/130
Self-loop alternating BA → BA
Theorem
Given a self-loop 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|).
IA169 Model Checking: Automata-based LTL model checking 73/130
Self-loop alternating BA → BA
Theorem
Given a self-loop 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(|φ|).
IA169 Model Checking: Automata-based LTL model checking 74/130
Algorithms checking disjointness of AK and A¬φ
Automata-based LTL model checking
(fair) Kripke structure K LTL formula φ
(generalized) Büchi automaton AK
representing (fair) runs of K
Büchi automaton A¬φ
representing runs violating φ
YES,
K |=(F) φ
NO + counterexample,
i.e. a (fair) run π of K such that π ̸|= φ
L(Ak ) ∩ L(A¬φ)
?
= ∅
IA169 Model Checking: Automata-based LTL model checking 76/130
Automata-based LTL model checking
(fair) Kripke structure K LTL formula φ
(generalized) Büchi automaton AK
representing (fair) runs of K
Büchi automaton A¬φ
representing runs violating φ
YES,
K |=(F) φ
NO + counterexample,
i.e. a (fair) run π of K such that π ̸|= φ
product generalized Büchi automaton B
L(B) = L(AK ) ∩ L(A¬φ)
L(B)
?
= ∅
IA169 Model Checking: Automata-based LTL model checking 77/130
Construction of product automaton
input: GBAs A1 = (Q1, Σ, δ1, Q01, F1) and A2 = (Q2, Σ, δ2, Q02, F2)
output: a GBA B = (Q1 × Q2, Σ, δ, Q01 × Q02, F) representing L(A1) ∩ L(A2)
δ = {((p1, p2), a, (q1, q2)) | (p1, a, q1) ∈ δ1 and (p2, a, q2) ∈ δ2}
F = {F1i × Q2 | F1i ∈ F1} ∪ {Q1 × F2i | F2i ∈ F2}
IA169 Model Checking: Automata-based LTL model checking 78/130
Construction of product automaton
input: GBAs A1 = (Q1, Σ, δ1, Q01, F1) and A2 = (Q2, Σ, δ2, Q02, F2)
output: a GBA B = (Q1 × Q2, Σ, δ, Q01 × Q02, F) representing L(A1) ∩ L(A2)
δ = {((p1, p2), a, (q1, q2)) | (p1, a, q1) ∈ δ1 and (p2, a, q2) ∈ δ2}
F = {F1i × Q2 | F1i ∈ F1} ∪ {Q1 × F2i | F2i ∈ F2}
1
2
F1 = {{1}, {2}}
a
b, c
b
a, c
p q r F2 = {{p, r}}a, c
a, c
a, b, c c
c
IA169 Model Checking: Automata-based LTL model checking 79/130
Construction of product automaton
input: GBAs A1 = (Q1, Σ, δ1, Q01, F1) and A2 = (Q2, Σ, δ2, Q02, F2)
output: a GBA B = (Q1 × Q2, Σ, δ, Q01 × Q02, F) representing L(A1) ∩ L(A2)
δ = {((p1, p2), a, (q1, q2)) | (p1, a, q1) ∈ δ1 and (p2, a, q2) ∈ δ2}
F = {F1i × Q2 | F1i ∈ F1} ∪ {Q1 × F2i | F2i ∈ F2}
Lemma
L(B) = L(A1) ∩ L(A2).
IA169 Model Checking: Automata-based LTL model checking 80/130
Emptiness of a GBA
Theorem
Let B = (Q, Σ, δ, Q0, F) be a GBA. The following conditions are equivalent.
1 L(B) ̸= ∅
2 There exists a nontrivial SCC of B reachable from Q0 and such that the SCC
contains at least one state of each Fi ∈ F.
3 There exists an accepting run of B of the form τ.ρω (so-called lasso-shaped).
IA169 Model Checking: Automata-based LTL model checking 81/130
Emptiness of a GBA
Theorem
Let B = (Q, Σ, δ, Q0, F) be a GBA. The following conditions are equivalent.
1 L(B) ̸= ∅
2 There exists a nontrivial SCC of B reachable from Q0 and such that the SCC
contains at least one state of each Fi ∈ F.
3 There exists an accepting run of B of the form τ.ρω (so-called lasso-shaped).
Proof.
1 =⇒ 2 Assume that L(B) ̸= ∅. Hence, there exists an accepting run π. The
run has to contain an infinite suffix contained in a single nontrivial
SCC of B reachable form Q0. As the run visits each Fi ∈ F infinitely
often, this SCC has to contain at least one state of each Fi ∈ F.
IA169 Model Checking: Automata-based LTL model checking 82/130
Emptiness of a GBA
Theorem
Let B = (Q, Σ, δ, Q0, F) be a GBA. The following conditions are equivalent.
1 L(B) ̸= ∅
2 There exists a nontrivial SCC of B reachable from Q0 and such that the SCC
contains at least one state of each Fi ∈ F.
3 There exists an accepting run of B of the form τ.ρω (so-called lasso-shaped).
Proof.
2 =⇒ 3 Assume that B has a nontrivial SCC reachable from Q0 and
containing at least one state of each Fi ∈ F. Let τ be a sequence of
successive states starting in Q0 and leading to a state q of the SCC.
Due to the properties of the SCC, there exists a sequence ρ of states
of the SCC which starts in some successor of q, ends in q, and
contains some state of each Fi ∈ F. Then τ.ρω is an accepting run.
IA169 Model Checking: Automata-based LTL model checking 83/130
Emptiness of a GBA
Theorem
Let B = (Q, Σ, δ, Q0, F) be a GBA. The following conditions are equivalent.
1 L(B) ̸= ∅
2 There exists a nontrivial SCC of B reachable from Q0 and such that the SCC
contains at least one state of each Fi ∈ F.
3 There exists an accepting run of B of the form τ.ρω (so-called lasso-shaped).
Proof.
3 =⇒ 1 Obvious.
IA169 Model Checking: Automata-based LTL model checking 84/130
Algorithms checking disjointness of AK and A¬φ
Algorithm based on SCC decomposition
Emptiness check by SCC decomposition
input : a GBA B = (Q, Σ, δ, Q0, F)
output: true if L(B) = ∅; false otherwise
procedure isGBAempty
remove unreachable states from the automaton
decompose the automaton into SCCs
if some nontrivial SCC contains at least one state of each Fi ∈ F then
return false
else
return true
IA169 Model Checking: Automata-based LTL model checking 86/130
Emptiness check by SCC decomposition
input : a GBA B = (Q, Σ, δ, Q0, F)
output: true if L(B) = ∅; false otherwise
procedure isGBAempty
remove unreachable states from the automaton
decompose the automaton into SCCs
if some nontrivial SCC contains at least one state of each Fi ∈ F then
return false
else
return true
if L(B) ̸= ∅, a counterexample accepted by a lasso-shaped run τ.ρω can be
constructed such that τ reaches the found SCC from Q0 and ρ is a loop
containing all states of the SCC
the corresponding accepted word u.vω ∈ L(B) is also lasso-shaped
IA169 Model Checking: Automata-based LTL model checking 87/130
Emptiness check by SCC decomposition
pros
simple
SCC decomposition can be done in time O(|Q| + |δ|)
IA169 Model Checking: Automata-based LTL model checking 88/130
Emptiness check by SCC decomposition
pros
simple
SCC decomposition can be done in time O(|Q| + |δ|)
cons
the whole GBA has to be known before the procedure starts
in model checking, GBA is a product of AK and A¬φ, where AK is typically
very large and described implicitly
IA169 Model Checking: Automata-based LTL model checking 89/130
Emptiness check by SCC decomposition
pros
simple
SCC decomposition can be done in time O(|Q| + |δ|)
cons
the whole GBA has to be known before the procedure starts
in model checking, GBA is a product of AK and A¬φ, where AK is typically
very large and described implicitly
on-the-fly model checking algorithms
the emptiness check explores the product automaton gradually and can
detect nonemptiness without knowing the whole product
the states and transitions of the product are constructed from A¬φ and the
implicit description of AK only on demand
IA169 Model Checking: Automata-based LTL model checking 90/130
Algorithms checking disjointness of AK and A¬φ
Nested DFS algorithm
Nested DFS check
also called double DFS
allows on-the-fly model checking
checks emptiness of a BA (not generalized)
can be easily used for model checking of a (not fair) Kripke structure K
such K is transformed into a BA AK where all states are accepting
IA169 Model Checking: Automata-based LTL model checking 92/130
Nested DFS check
also called double DFS
allows on-the-fly model checking
checks emptiness of a BA (not generalized)
can be easily used for model checking of a (not fair) Kripke structure K
such K is transformed into a BA AK where all states are accepting
construction of product BA for a BA with all states accepting and another BA
input: a BA A1 = (Q1, Σ, δ1, Q01, Q1) and a BA A2 = (Q2, Σ, δ2, Q02, F2)
output: a BA B = (Q1 × Q2, Σ, δ, Q01 × Q02, F) representing L(A1) ∩ L(A2)
δ = {((p1, p2), a, (q1, q2)) | (p1, a, q1) ∈ δ1 and (p2, a, q2) ∈ δ2}
F = Q1 × F2
IA169 Model Checking: Automata-based LTL model checking 93/130
Emptiness of a BA
Theorem
Let B = (Q, Σ, δ, Q0, F) be a BA. The L(B) ̸= ∅ ⇐⇒ there exist a run of the form
τ.ρω where ρ starts with a state of F.
IA169 Model Checking: Automata-based LTL model checking 94/130
Emptiness of a BA
Theorem
Let B = (Q, Σ, δ, Q0, F) be a BA. The L(B) ̸= ∅ ⇐⇒ there exist a run of the form
τ.ρω where ρ starts with a state of F.
Proof.
⇐= Follows directly from the fact that τ.ρω is an accepting run of B.
IA169 Model Checking: Automata-based LTL model checking 95/130
Emptiness of a BA
Theorem
Let B = (Q, Σ, δ, Q0, F) be a BA. The L(B) ̸= ∅ ⇐⇒ there exist a run of the form
τ.ρω where ρ starts with a state of F.
Proof.
⇐= Follows directly from the fact that τ.ρω is an accepting run of B.
=⇒ Assume that L(B) ̸= ∅. There exists an accepting run
π = s0s1 . . . ∈ Qω. As π is accepting, there exists a state
q ∈ inf(π) ∩ F. Let i < j be such that si, sj are the first two
occurrences of q in π. Further, let τ = s0s1 . . . si−1 and
ρ = sisi+1 . . . sj−1. Then τ.ρω = s0s1 . . . si−1.(sisi+1 . . . sj−1)ω is a run
of B and ρ starts with si ∈ F.
IA169 Model Checking: Automata-based LTL model checking 96/130
Nested DFS algorithm
the algorithm uses two nested instances of depth-first search
the first DFS searches for reachable accepting states
the nested DFS looks for a cycle from accepting states
the algorithm terminates when a cycle from an accepting state is found
all executions of the nested DFS share the information about visited states:
without this feature, the overall complexity of nested DFS executions would be
O(|F| · (|Q| + |δ|))
IA169 Model Checking: Automata-based LTL model checking 97/130
Nested DFS algorithm
input : a BA B = (Q, Σ, δ, Q0, F)
output: true if L(B) = ∅;
false otherwise
procedure isBAempty
visited1 ← ∅
visited2 ← ∅
onStack ← ∅
forall q0 ∈ Q0 do
dfs1(q0)
terminate true
procedure dfs1(q)
visited1 ← visited1 ∪ {q}
onStack ← onStack ∪ {q}
forall successors q′
of q do
if q′
̸∈ visited1 then dfs1(q′
)
if q ∈ F then dfs2(q)
onStack ← onStack ∖ {q}
procedure dfs2(q)
visited2 ← visited2 ∪ {q}
forall successors q′
of q do
if q′
∈ onStack then terminate false
if q′
̸∈ visited2 then dfs2(q′
)
IA169 Model Checking: Automata-based LTL model checking 98/130
Example
A B C
D E F
G H I
J K
IA169 Model Checking: Automata-based LTL model checking 99/130
Nested DFS algorithm
if the algorithm returns false, it can produce a counterexample corresponding
to the lasso-shaped accepting run given by the current content of DFS stacks
let q be the accepting state from which the last nested DFS was executed
let q′ be the state on stack discovered by the nested DFS
q0
q′
q
stack of the first DFS
stack of the nested DFS
accepting lasso-shaped run:
q0 q′ (q q′ )ω
IA169 Model Checking: Automata-based LTL model checking 100/130
Correctness of the nested DFS algorithm
Theorem
The nested DFS algorithm returns false ⇐⇒ L(B) ̸= ∅.
IA169 Model Checking: Automata-based LTL model checking 101/130
Correctness of the nested DFS algorithm
Theorem
The nested DFS algorithm returns false ⇐⇒ L(B) ̸= ∅.
Proof.
=⇒ is obvious. We prove ⇐= by contradiction. Assume that L(B) ̸= ∅ and the
algorithm returns true. As L(B) ̸= ∅, there is a run τ.ρω where ρ starts with a state
q ∈ F. When the nested DFS is started from q, there has to be a state q′ on the
stack of the first DFS reachable from q. Nested DFS has not found the cycle
because q′ is reachable only via r ∈ visited2. Assume that q is the first such a
state and that r is added to visited2 during the nested DFS started from q′′ ∈ F.
1 If q′′ is reachable from q, then there is a cycle q′′ r q q′′ which is
the contradiction with the assumption that q is the first such state.
2 If q′′ is not reachable from q, then q is reachable from q′′ via q′′ r q.
We have the contradiction with the fact that the first DFS backtracks from a
state only after it backtracks from all states reachable from them and thus
nested DFS from q′′ cannot be executed before the nested DFS from q.
IA169 Model Checking: Automata-based LTL model checking 102/130
Complexity of the nested DFS algorithm
complexity of the first DFS
time: O(|Q| + |δ|)
space: O(|Q|)
IA169 Model Checking: Automata-based LTL model checking 103/130
Complexity of the nested DFS algorithm
complexity of the first DFS
time: O(|Q| + |δ|)
space: O(|Q|)
complexity of the nested DFS (all executions)
time: O(|Q| + |δ|)
space: O(|Q|)
IA169 Model Checking: Automata-based LTL model checking 104/130
Complexity of the nested DFS algorithm
complexity of the first DFS
time: O(|Q| + |δ|)
space: O(|Q|)
complexity of the nested DFS (all executions)
time: O(|Q| + |δ|)
space: O(|Q|)
overall complexity
time: O(|Q| + |δ|)
space: O(|Q|)
IA169 Model Checking: Automata-based LTL model checking 105/130
Algorithms checking disjointness of AK and A¬φ
Optimizations
Terminal and weak BA
Definition (terminal BA, weak BA)
Let B be a Büchi automaton with alphabet Σ. A Büchi automaton is terminal if
each accepting state has a loop transition under each a ∈ Σ.
A Büchi automaton is weak if each strongly connected component consists either
of accepting states or of nonaccepting states.
IA169 Model Checking: Automata-based LTL model checking 107/130
Terminal and weak BA
Definition (terminal BA, weak BA)
Let B be a Büchi automaton with alphabet Σ. A Büchi automaton is terminal if
each accepting state has a loop transition under each a ∈ Σ.
A Büchi automaton is weak if each strongly connected component consists either
of accepting states or of nonaccepting states.
many LTL properties translate to terminal or weak BA
if this is the case, simpler emptiness checks can be used
IA169 Model Checking: Automata-based LTL model checking 108/130
Optimization for terminal automata
assume that A¬φ is a terminal BA and each state of BA AK is accepting and
has a successor
let B be the product BA of A¬φ and AK
L(B) ̸= ∅ iff B has a reachable accepting state
instead of nested DFS, emptiness of L(B) can be decided by a single DFS
checking the reachability of an accepting state
properties φ with terminal A¬φ are called safety properties
typical safety property: G¬err
IA169 Model Checking: Automata-based LTL model checking 109/130
Optimization for weak automata
assume that A¬φ is a weak BA and each state of BA AK is accepting
let B be the product BA of A¬φ and a BA AK
each cycle of B contains either only accepting states or no accepting state
instead of nested DFS, emptiness of L(B) can be decided by a single DFS
that looks for a cycle and if a cycle is found, it checks whether the current
state is accepting
typical property φ with weak A¬φ: G(a =⇒ Fb) (responsivity)
IA169 Model Checking: Automata-based LTL model checking 110/130
Extending LTL with release
another derived LTL operator release: φ R ψ ≡ ¬(¬φ U ¬ψ)
equivalently: φ R ψ ≡ Gψ ∨ ψ U (ψ ∧ φ)
a R b b b b b . . . or b b . . . b (ab) . . .
by adding ⊥, ∨, and R to the basic syntax of LTL, we can push all negations
towards atomic propositions using equivalences
¬(φ U ψ) ≡ ¬φ R ¬ψ
¬(φ R ψ) ≡ ¬φ U ¬ψ
¬Xφ ≡ X¬φ
¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ
¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ
¬¬a ≡ a
IA169 Model Checking: Automata-based LTL model checking 111/130
Hierarchy of LTL classes
Definition (hierarchy of LTL classes)
Σ0 = Π0 is the smallest set of LTL formulas containing all atomic propositions
and closed under application of ∧, ∨, ¬, and X.
Σi+1 is the smallest set of LTL formulas containing Πi and closed under
application of ∧, ∨, X, and U.
Πi+1 is the smallest set of LTL formulas containing Σi and closed under
application of ∧, ∨, X, and R.
IA169 Model Checking: Automata-based LTL model checking 112/130
Hierarchy of LTL classes
Definition (hierarchy of LTL classes)
Σ0 = Π0 is the smallest set of LTL formulas containing all atomic propositions
and closed under application of ∧, ∨, ¬, and X.
Σi+1 is the smallest set of LTL formulas containing Πi and closed under
application of ∧, ∨, X, and U.
Πi+1 is the smallest set of LTL formulas containing Σi and closed under
application of ∧, ∨, X, and R.
for each φ ∈ Πi, ¬φ can be transformed (by pushing negations towards atomic
propositions) to an equivalent formula ψ ∈ Σi
for each φ ∈ Σi, ¬φ can be transformed (by pushing negations towards atomic
propositions) to an equivalent formula ψ ∈ Πi
IA169 Model Checking: Automata-based LTL model checking 113/130
Properties corresponding to LTL classes
Σ1 describes guarantee properties
Π1 describes safety properties
B+(Σ1 ∪ Π1) describes obligation properties
Σ2 describes persistence properties
Π2 describes recurrence (or response) properties
B+(Σ2 ∪ Π2) describes reactivity properties
the LTL classes are sometimes called guarantee, safety, . . . formulae
IA169 Model Checking: Automata-based LTL model checking 114/130
Hierarchy of properties
safety
Π1
recurrence
Π2
guarantee
Σ1
persistence
Σ2
obligation
B+(Σ1 ∪ Π1)
reactivity
B+(Σ2 ∪ Π2)
Σ0 = Π0
terminal BA
weak BA
each language definable in LTL is definable in B+(Σ2 ∪ Π2)
formulae of Σ1 can be translated to terminal BA
formulae of Σ2 can be translated to weak BA
IA169 Model Checking: Automata-based LTL model checking 115/130
Fighting state-space explosion
state-space explosion problem
Kripke structure (and thus also the product automaton) can have enormous
number of states, often exponential in the size of its implicit description
model checking algorithms often run out of memory
IA169 Model Checking: Automata-based LTL model checking 116/130
Fighting state-space explosion
state-space explosion problem
Kripke structure (and thus also the product automaton) can have enormous
number of states, often exponential in the size of its implicit description
model checking algorithms often run out of memory
methods fighting the problem
low-level techniques for saving memory
lossless compression of states in memory
heuristics based on lossy compression
forgetting some visited states
IA169 Model Checking: Automata-based LTL model checking 117/130
Fighting state-space explosion
state-space explosion problem
Kripke structure (and thus also the product automaton) can have enormous
number of states, often exponential in the size of its implicit description
model checking algorithms often run out of memory
methods fighting the problem
low-level techniques for saving memory
lossless compression of states in memory
heuristics based on lossy compression
forgetting some visited states
on-the-fly approaches
can help to find a counterexample, but does not help for correct systems
IA169 Model Checking: Automata-based LTL model checking 118/130
Fighting state-space explosion
state-space explosion problem
Kripke structure (and thus also the product automaton) can have enormous
number of states, often exponential in the size of its implicit description
model checking algorithms often run out of memory
methods fighting the problem
low-level techniques for saving memory
lossless compression of states in memory
heuristics based on lossy compression
forgetting some visited states
on-the-fly approaches
can help to find a counterexample, but does not help for correct systems
state-space reduction methods
partial order reduction (only for LTL properties without X operators)
symmetry reduction (avoids exploration of symmetric parts)
abstraction
IA169 Model Checking: Automata-based LTL model checking 119/130
Fighting state-space explosion
state-space explosion problem
Kripke structure (and thus also the product automaton) can have enormous
number of states, often exponential in the size of its implicit description
model checking algorithms often run out of memory
methods fighting the problem
low-level techniques for saving memory
lossless compression of states in memory
heuristics based on lossy compression
forgetting some visited states
on-the-fly approaches
can help to find a counterexample, but does not help for correct systems
state-space reduction methods
partial order reduction (only for LTL properties without X operators)
symmetry reduction (avoids exploration of symmetric parts)
abstraction
symbolic representation of sets of states (by formulae or BDDs)
parallel and distributed algorithms
IA169 Model Checking: Automata-based LTL model checking 120/130
Action-based version of LTL model checking
Action-based LTL model checking
actions
basic observable information attached to each transition of the system
for example: gate openning, process P entered critical section
Act denotes a countable set of actions
IA169 Model Checking: Automata-based LTL model checking 122/130
Action-based LTL model checking
actions
basic observable information attached to each transition of the system
for example: gate openning, process P entered critical section
Act denotes a countable set of actions
basic formalism for action-based systems is a labeled transition system
IA169 Model Checking: Automata-based LTL model checking 123/130
Labeled transition system
Definition (labeled transition system, LTS)
A labeled transition systems (LTS) is a tuple M = (S, Act′
, δ, S0), where
S is a set of states,
Act′
⊆ Act is a finite set of actions,
δ ⊆ S × Act′
× S is a transition relation,
S0 ⊆ S is a set of initial states.
IA169 Model Checking: Automata-based LTL model checking 124/130
Labeled transition system
Definition (labeled transition system, LTS)
A labeled transition systems (LTS) is a tuple M = (S, Act′
, δ, S0), where
S is a set of states,
Act′
⊆ Act is a finite set of actions,
δ ⊆ S × Act′
× S is a transition relation,
S0 ⊆ S is a set of initial states.
Definition (run, trace)
Let M = (S, Act′
, δ, S0) be an LTS. A run of M is an infinite sequence
π = (s0, a0, s1)(s1, a1, s2)(s2, a2, s3) . . . ∈ δω of adjacent transitions such that
s0 ∈ S0.
The trace of π is then the infinite word σ(π) = a0a1a2 . . ..
IA169 Model Checking: Automata-based LTL model checking 125/130
Modified syntax and semantics of LTL
modified syntax of LTL
the only change is that a ranges over Act (instead of AP)
IA169 Model Checking: Automata-based LTL model checking 126/130
Modified syntax and semantics of LTL
modified syntax of LTL
the only change is that a ranges over Act (instead of AP)
modified semantics of LTL
we interpret LTL on infinite words w = w(0)w(1) . . . ∈ Actω
the only change in the inductive definition of w |= φ is the line
w |= a iff a = w(0) (instead of w |= a iff a ∈ w(0))
IA169 Model Checking: Automata-based LTL model checking 127/130
The goal of action-based LTL model checking
Definition
Let M = (S, Act′
, δ, S0) be an LTS and φ be an LTL formula.
A run π of M satisfies φ, written π |= φ, if σ(π) |= φ.
M satisfies φ, written M |= φ, if π |= φ holds for every run π of M.
IA169 Model Checking: Automata-based LTL model checking 128/130
The goal of action-based LTL model checking
Definition
Let M = (S, Act′
, δ, S0) be an LTS and φ be an LTL formula.
A run π of M satisfies φ, written π |= φ, if σ(π) |= φ.
M satisfies φ, written M |= φ, if π |= φ holds for every run π of M.
The goal of action-based LTL model checking is to decide whether a given LTS M
satisfies a given LTL formula φ. In the negative case, model checking should
provide a counterexample, i.e., a run π of M such that π ̸|= φ.
IA169 Model Checking: Automata-based LTL model checking 129/130
Automata-based approach to action-based LTL model checking
The automata-based approach to LTL model checking of finite LTS is basically
identical as for finite Kripke structures.
changes
Büchi automata use the alphabet Σ = Act′
given by the LTS
we assume that φ contains only actions from Act′
(otherwise, we extend Act′
)
LTS M = (S, Act′
, δ, S0) is transformed into a BA AM = (S, Act′
, δ, S0, S)
modification of LTL → self-loop alternating BA translation
δ(qa, l) = ⊤ if a = l, ⊥ otherwise (instead of δ(qa, l) = ⊤ if a ∈ l, ⊥ otherwise)
IA169 Model Checking: Automata-based LTL model checking 130/130