IA169 Model Checking
Reachability in Pushdown Systems
Jan Strejˇcek
Faculty of Informatics
Masaryk University
Motivation
Pushdown systems can be used to precisely model sequential programs with
procedure calls, unbounded recursion, and both local and global variables with
finite domains.
IA169 Model Checking: Reachability in Pushdown Systems 2/51
Agenda and sources
agenda
pushdown systems
representation of sets of configurations
computing all predecessors
bonus: state-based LTL model checking
sources
J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon: Efficient algorithms
for model checking pushdown systems, CAV 2000, LNCS 1855, Springer,
2000.
S. Schwoon: Model-Checking Pushdown Systems, PhD thesis, TUM, 2002.
IA169 Model Checking: Reachability in Pushdown Systems 3/51
Pushdown systems
Pushdown systems
Definition (pushdown system)
A pushdown system is a triple P = (P, Γ, ∆), where
P is a finite set of control locations,
Γ is a finite stack alphabet,
∆ ⊆ (P × Γ) × (P × Γ∗) is a finite set of transition rules.
IA169 Model Checking: Reachability in Pushdown Systems 5/51
Pushdown systems
Definition (pushdown system)
A pushdown system is a triple P = (P, Γ, ∆), where
P is a finite set of control locations,
Γ is a finite stack alphabet,
∆ ⊆ (P × Γ) × (P × Γ∗) is a finite set of transition rules.
we write ⟨q, γ⟩ → ⟨q′, w⟩ instead of ((q, γ), (q′, w)) ∈ ∆
we do not consider any input alphabet as we do not use pushdown systems to
represent languages
IA169 Model Checking: Reachability in Pushdown Systems 6/51
Definitions
a configuration of P is a pair ⟨p, w⟩ ∈ P × Γ∗, where w is a stack content (the
topmost symbol is on the left)
the set of all configurations is denoted by C
an immediate successor relation on configurations is defined in standard way
reachability relation ⇒ ⊆ C × C is the reflexive and transitive closure of the
immediate successor relation
+
⇒ ⊆ C × C is the transitive closure of the immediate successor relation
given a set C ⊆ C of configurations, we define the set of their predecessors as
pre∗
(C) = {c ∈ C | ∃c′
∈ C . c ⇒ c′
}
IA169 Model Checking: Reachability in Pushdown Systems 7/51
Representation of sets of configurations
P-automata
P-automata
are finite automata used to represent sets of configurations
use Γ as an alphabet
have one initial state for every control location of the pushdown (we use P as
the set of initial states)
Definition (P-automaton)
Given a pushdown system P = (P, Γ, ∆), a P-automaton (or simply automaton) is
a tuple A = (Q, Γ, δ, P, F) where
Q is a finite set of states such that P ⊆ Q,
δ ⊆ Q × Γ × Q is a set of transitions,
F ⊆ Q is a set of final states.
IA169 Model Checking: Reachability in Pushdown Systems 9/51
More definitions
a (reflexive and transitive) transition relation → ⊆ Q × Γ∗ × Q is defined in a
standard way
P-automaton A represents the set of configurations
Conf(A) = {⟨p, w⟩ | ∃q ∈ F . p
w
→ q}
a set of configurations of P is called regular if it is recognized by some
P-automaton
IA169 Model Checking: Reachability in Pushdown Systems 10/51
More definitions
a (reflexive and transitive) transition relation → ⊆ Q × Γ∗ × Q is defined in a
standard way
P-automaton A represents the set of configurations
Conf(A) = {⟨p, w⟩ | ∃q ∈ F . p
w
→ q}
a set of configurations of P is called regular if it is recognized by some
P-automaton
notation convention
p, p′, p′′, . . . denote initial states of an automaton (i.e. elements of P)
s, s′, s′′, . . . denote non-initial states
q, q′, q′′, . . . denote arbitrary states (initial or not)
IA169 Model Checking: Reachability in Pushdown Systems 11/51
Computing all predecessors
Statements
1 Given a pushdown system P and a regular set of configurations C, the set
pre∗(C) is again regular.
2 If C is defined by a P-automaton A, then the automaton Apre∗ representing
pre∗(C) is effectively constructible.
IA169 Model Checking: Reachability in Pushdown Systems 13/51
Intuition
⟨p1, γ0⟩ → ⟨p2, γ1γ2⟩
⟨p3, γ3⟩ → ⟨p1, γ0γ1⟩
p1
p2
p3
· · ·
...
γ1
γ2
γ1
IA169 Model Checking: Reachability in Pushdown Systems 14/51
Intuition
⟨p1, γ0⟩ → ⟨p2, γ1γ2⟩
⟨p3, γ3⟩ → ⟨p1, γ0γ1⟩
p1
p2
p3
· · ·
...
γ1
γ2
γ1
γ0
IA169 Model Checking: Reachability in Pushdown Systems 15/51
Intuition
⟨p1, γ0⟩ → ⟨p2, γ1γ2⟩
⟨p3, γ3⟩ → ⟨p1, γ0γ1⟩
p1
p2
p3
· · ·
...
γ1
γ2
γ1
γ0
γ3
IA169 Model Checking: Reachability in Pushdown Systems 16/51
Idea
Let P be a pushdown system and A be a P-automaton. We assume (w.l.o.g.) that
A has no transition leading to an initial state. The automaton Apre∗ is obtained
from A by addition of new transitions according to the following rule:
Saturation rule
If ⟨p, γ⟩ → ⟨p′, w⟩ and p′ w
→ q in the current automaton,
add a transition (p, γ, q).
we apply this rule repeatedly until we reach a fixpoint
a fixpoint exists as the number of possible new transitions is finite
the resulting P-automaton is Apre∗
IA169 Model Checking: Reachability in Pushdown Systems 17/51
Example
p0
p1
p2
s1 s2
γ0 γ0
transition rules of P:
⟨p0, γ0⟩ → ⟨p1, γ1γ0⟩ ⟨p2, γ2⟩ → ⟨p0, γ1⟩
⟨p1, γ1⟩ → ⟨p2, γ2γ0⟩ ⟨p0, γ1⟩ → ⟨p0, ε⟩
IA169 Model Checking: Reachability in Pushdown Systems 18/51
Example
p0
p1
p2
s1 s2
γ0 γ0
γ1
γ0
γ1
γ1γ2
transition rules of P:
⟨p0, γ0⟩ → ⟨p1, γ1γ0⟩ ⟨p2, γ2⟩ → ⟨p0, γ1⟩
⟨p1, γ1⟩ → ⟨p2, γ2γ0⟩ ⟨p0, γ1⟩ → ⟨p0, ε⟩
IA169 Model Checking: Reachability in Pushdown Systems 19/51
Normal form
Definition (normal form)
A pushdown system is in normal form if every rule ⟨p, γ⟩ → ⟨p′, w⟩ satisfies
|w| ≤ 2.
any pushdown system can be transformed into normal form with only linear
size increase
IA169 Model Checking: Reachability in Pushdown Systems 20/51
Algorithm: notes
We give an algorithm that, for a given A, computes transitions of Apre∗ . The rest of
the automaton Apre∗ is identical to A.
The algorithm uses sets rel and trans containing the transitions that are known to
belong to Apre∗ :
rel contains transitions that have already been examined
no transition is examined more than once
when we have a rule ⟨p, γ⟩ → ⟨p′, γ′γ′′⟩ and transitions t1 = (p′, γ′, q′) and
t2 = (q′, γ′′, q′′) (where q, q′ are arbitrary states), we have to add transition
(p, γ, q′′)
we do it in such a way that whenever we examine t1, we check if there is a
corresponding t2 ∈ rel and we add an extra rule ⟨p, γ⟩ → ⟨q′, γ′′⟩ to a set of
such extra rules ∆′
the extra rule guarantees that if a suitable t2 will be examined in the future,
(p, γ, q′′) will be added.
IA169 Model Checking: Reachability in Pushdown Systems 21/51
Algorithm
input : a pushdown system P = (P, Γ, ∆) in normal form and
a P-automaton A=(Q, Γ, δ, P, F) without transitions into P
output: the set of transitions of Apre∗
1 rel ← ∅; trans ← δ; ∆′ ← ∅
2 forall ⟨p, γ⟩ → ⟨p′, ε⟩ ∈ ∆ do trans ← trans ∪ {(p, γ, p′)}
3 while trans ̸= ∅ do
4 pop t = (q, γ, q′) from trans
5 if t ̸∈ rel then
6 rel ← rel ∪ {t}
7 forall ⟨p1, γ1⟩ → ⟨q, γ⟩ ∈ (∆ ∪ ∆′) do
8 trans ← trans ∪ {(p1, γ1, q′)}
9 forall ⟨p1, γ1⟩ → ⟨q, γγ2⟩ ∈ ∆ do
10 ∆′ ← ∆′ ∪ {⟨p1, γ1⟩ → ⟨q′, γ2⟩}
11 forall (q′, γ2, q′′) ∈ rel do
12 trans ← trans ∪ {(p1, γ1, q′′)}
13 return rel
IA169 Model Checking: Reachability in Pushdown Systems 22/51
Theorem
Theorem
Let P = (P, Γ, ∆) be a pushdown system and A = (Q, Γ, δ, P, F) be a
P-automaton. There exists an automaton Apre∗ recognizing pre∗(Conf(A)).
Moreover, Apre∗ can be constructed in O(|Q|2 · |∆|) time and O(|Q| · |∆| + |δ|)
space.
Proof.
We can assume that every transition is added to trans at most once. This can
be done (without asymptotic loss of time) by storing all transitions which are
ever added to trans in an additional hash table.
Further, we assume that there is at least one rule in ∆ for every γ ∈ Γ
(transitions of A under some γ not satisfying this assumption can be moved
directly to rel).
The number of transitions in δ as well as the number of iterations of the
while-loop is bounded by |Q|2 · |∆|.
IA169 Model Checking: Reachability in Pushdown Systems 23/51
Proof: time complexity
Proof (Cont.)
Line 10 is executed for each combination of a rule ⟨p1, γ1⟩ → ⟨q, γγ2⟩ and a
transition (q, γ, q′) ∈ trans, i.e. at most |Q| · |∆| times.
Hence, |∆′| ≤ |Q| · |∆|.
For the loop starting at line 11, q′ and γ2 are fixed. Thus, line 12 is executed
at most |Q|2 · |∆| times.
Line 8 is executed for each combination of a rule ⟨p1, γ1⟩ → ⟨q, γ⟩ ∈ (∆ ∪ ∆′)
and a transition (q, γ, q′) ∈ trans. As |∆′| ≤ |Q| · |∆|, line 8 is executed at most
O(|Q|2 · |∆|) times.
As a conclusion, the algorithm takes O(|Q|2 · |∆|) time.
IA169 Model Checking: Reachability in Pushdown Systems 24/51
Proof: space complexity
Proof (Cont.)
Memory is needed for storing rel, trans, and ∆′.
The size of ∆′ is in O(|Q| · |∆|).
Line 1 adds |δ| transitions to trans.
Line 2 adds at most |∆| transitions to trans.
In lines 8 and 12, p1 and γ1 are given by the head of a rule in ∆ (note that
every rule in ∆′ have the same head as some rule in ∆). Hence, lines 8 and
12 add at most |Q| · |∆| different transitions.
We directly get that the algorithm needs O(|Q| · |∆| + |δ|) space. As this is also the
size of the result rel, the algorithm is optimal with respect to the memory
usage.
IA169 Model Checking: Reachability in Pushdown Systems 25/51
Notes
the algorithm can be used to verify safety property: given an automaton A
representing error configurations, we can compute Apre∗ , i.e. the set of all
configurations from which an error configuration is reachable
there is a similar algorithm computing, for a given regular set of configurations
C, the set of all successors
post∗
(C) = {c′
∈ C | ∃c ∈ C . c ⇒ c′
}
Theorem
Let P = (P, Γ, ∆) be a pushdown system and A = (Q, Γ, δ, P, F) be a
P-automaton. There exists an automaton Apost∗ recognizing post∗
(Conf(A)).
Moreover, Apost∗ can be constructed in O(|P| · |∆| · (|Q| + |∆|) + |P| · |δ|) time and
space.
IA169 Model Checking: Reachability in Pushdown Systems 26/51
Bonus: State-based LTL model checking
The problem
The global state-based LTL model checking problem for pushdown systems
Compute the set of all configurations of a given pushdown system P that violate a
given LTL formula φ (where a configuration c violates φ if there is a path starting
from c and not satisfying φ).
IA169 Model Checking: Reachability in Pushdown Systems 28/51
Extending pushdown systems
state-based =⇒ validity of atomic propositions
labeling function L : (P × Γ) → 2AP assigns valid atomic propositions to every
pair (p, γ) of a control location p and a topmost stack symbol γ
pushdown system P and L define Kripke structure
states = configurations of P
transition relation = immediate successor relation
no initial states (global model checking)
labeling function is an extension of L: L(⟨p, γw⟩) = L(p, γ)
IA169 Model Checking: Reachability in Pushdown Systems 29/51
The schema
pushdown system P
with labeling function L
LTL formula φ
representing Kripke structure
with infinitely many states
Büchi automaton A¬φ
representing runs violating φ
product: Büchi pushdown system BP
accepting run problem
to compute the set of configurations
of BP where accepting runs start
IA169 Model Checking: Reachability in Pushdown Systems 30/51
Büchi pushdown system
Büchi pushdown system
pushdown system with a set of accepting control locations
an accepting run is a path passing through some accepting control location
infinitely often
IA169 Model Checking: Reachability in Pushdown Systems 31/51
Product
Product of
a pushdown system P = (P, Γ, ∆) with a labeling function L and
a Büchi automaton A¬φ = (Q, 2AP(φ), δ, Q0, F)
is a Büchi pushdown system BP = ((P × Q), Γ, ∆′, G), where
⟨(p, q), γ⟩ → ⟨(p′, q′), w⟩ ∈ ∆′ iff ⟨p, γ⟩ → ⟨p′, w⟩ ∈ ∆ and
(q, L(p, γ) ∩ AP(φ), q′) ∈ δ
and G = P × F it the set of accepting control locations.
Clearly, a configuration ⟨p, w⟩ of P violates φ iff BP has an accepting run starting
from ⟨(p, q0), w⟩ for some q0 ∈ Q0.
IA169 Model Checking: Reachability in Pushdown Systems 32/51
Accepting run problem
The original model checking problem reduces to the following:
The accepting run problem
Compute the set Ca of configurations c of BP such that BP has an accepting run
starting from c.
IA169 Model Checking: Reachability in Pushdown Systems 33/51
Repeating heads
⇒ denotes the (reflexive and transitive) reachability relation
+
⇒ denotes the (transitive) reachability relation
IA169 Model Checking: Reachability in Pushdown Systems 34/51
Repeating heads
⇒ denotes the (reflexive and transitive) reachability relation
+
⇒ denotes the (transitive) reachability relation
We define the relation
r
⇒ on configurations of BP as
c
r
⇒ c′ iff c ⇒ ⟨g, u⟩
+
⇒ c′ for some configuration ⟨g, u⟩ with g ∈ G.
IA169 Model Checking: Reachability in Pushdown Systems 35/51
Repeating heads
⇒ denotes the (reflexive and transitive) reachability relation
+
⇒ denotes the (transitive) reachability relation
We define the relation
r
⇒ on configurations of BP as
c
r
⇒ c′ iff c ⇒ ⟨g, u⟩
+
⇒ c′ for some configuration ⟨g, u⟩ with g ∈ G.
Definition (head, repeating head)
The head of a rule ⟨p, γ⟩ → ⟨p′, w⟩ is the configuration ⟨p, γ⟩.
A head ⟨p, γ⟩ is repeating if ⟨p, γ⟩
r
⇒ ⟨p, γv⟩ for some v ∈ Γ∗.
The set of repeating heads of BP is denoted by R.
IA169 Model Checking: Reachability in Pushdown Systems 36/51
Characterization of configurations with accepting runs
Lemma
Let c be a configuration of a Büchi pushdown system BP.
BP has an accepting run starting from c ⇐⇒ there exists a repeating head ⟨p, γ⟩
such that c ⇒ ⟨p, γw⟩ for some w ∈ Γ∗.
IA169 Model Checking: Reachability in Pushdown Systems 37/51
Characterization of configurations with accepting runs
Lemma
Let c be a configuration of a Büchi pushdown system BP.
BP has an accepting run starting from c ⇐⇒ there exists a repeating head ⟨p, γ⟩
such that c ⇒ ⟨p, γw⟩ for some w ∈ Γ∗.
Proof.
The implication “⇐=” is obvious. We prove “=⇒”.
assume that BP has an accepting run ⟨p0, w0⟩, ⟨p1, w1⟩, ⟨p2, w2⟩, . . . starting
from c
let i0, i1, . . . be an increasing sequence of indices such that
|wi0
| = min{|wj | | j ≥ 0}
|wik
| = min{|wj | | j > ik−1} for k > 0
once a configuration ⟨pik
, wik
⟩ is reached, the rest of the run never looks at or
changes the bottom |wik
| − 1 stack symbols
IA169 Model Checking: Reachability in Pushdown Systems 38/51
Proof
Proof (Cont.)
let γik
be the topmost symbol of wik
for each k ≥ 0
as the number of pairs (pik
, γik
) is bounded by |P × Γ|, there has to be a pair
(p, γ) repeated infinitely many times
moreover, since some g ∈ G becomes a control location infinitely often, we
can select two indeces j1 < j2 out of i0, i1, . . . such that
⟨pj1
, wj1
⟩ = ⟨p, γw⟩
r
⇒ ⟨pj2
, wj2
⟩ = ⟨p, γvw⟩
for some w, v ∈ Γ∗
as w is never looked at or changed in the rest of the run, we have that
⟨p, γ⟩
r
⇒ ⟨p, γv⟩
this proves “=⇒”
IA169 Model Checking: Reachability in Pushdown Systems 39/51
Consequences
Lemma
Let c be a configuration of a Büchi pushdown system BP.
BP has an accepting run starting from c ⇐⇒ there exists a repeating head ⟨p, γ⟩
such that c ⇒ ⟨p, γw⟩ for some w ∈ Γ∗.
the set of all configurations violating the considered formula φ can be
computed as pre∗(RΓ∗), where RΓ∗ = {⟨p, γw⟩ | ⟨p, γ⟩ ∈ R, w ∈ Γ∗}
as R is finite, RΓ∗ is clearly regular
pre∗(C) can be easily computed for regular sets C
the only remaining step to solve the model checking problem is the algorithm
computing R
IA169 Model Checking: Reachability in Pushdown Systems 40/51
Computing R
Computing R is reduced to a graph-theoretic problem.
Given a BP = (P, Γ, ∆, G), we construct a graph G = (P × Γ, E) representing the
reachability relation between heads, i.e.
nodes are the heads of BP,
E ⊆ (P × Γ) × {0, 1} × (P × Γ) is the smallest relation satisfying the following
rule:
Rule
If ⟨p, γ⟩ → ⟨p′′, v1γ′v2⟩ and ⟨p′′, v1⟩ ⇒ ⟨p′, ε⟩ then
1 ((p, γ), 1, (p′, γ′)) ∈ E if ⟨p′′, v1⟩
r
⇒ ⟨p′, ε⟩ or p ∈ G
2 ((p, γ), 0, (p′, γ′)) ∈ E otherwise.
IA169 Model Checking: Reachability in Pushdown Systems 41/51
Computing R
Rule
If ⟨p, γ⟩ → ⟨p′′, v1γ′v2⟩ and ⟨p′′, v1⟩ ⇒ ⟨p′, ε⟩ then
1 ((p, γ), 1, (p′, γ′)) ∈ E if ⟨p′′, v1⟩
r
⇒ ⟨p′, ε⟩ or p ∈ G
2 ((p, γ), 0, (p′, γ′)) ∈ E otherwise.
Edges are labelled with 1 if an accepting control state is passed between the
heads, by 0 otherwise.
Conditions ⟨p′′, v1⟩ ⇒ ⟨p′, ε⟩ or ⟨p′′, v1⟩
r
⇒ ⟨p′, ε⟩ can be checked by the algorithm
for pre∗({⟨p′, ε⟩}) or its small modification, respectively.
IA169 Model Checking: Reachability in Pushdown Systems 42/51
Computing R
Once G is constructed, R can be computed using the fact that:
a head ⟨p, γ⟩ is repeating ⇐⇒ (p, γ) is in a strongly connected component of G
which has an internal edge labelled with 1
IA169 Model Checking: Reachability in Pushdown Systems 43/51
Example
Construct the graph G for BP = ({p0, p1, p2}, {γ0, γ1, γ2}, ∆, {p2}), where
∆ = { ⟨p0, γ0⟩ → ⟨p1, γ1γ0⟩, ⟨p2, γ2⟩ → ⟨p0, γ1⟩,
⟨p1, γ1⟩ → ⟨p2, γ2γ0⟩, ⟨p0, γ1⟩ → ⟨p0, ε⟩ }.
Rule
If ⟨p, γ⟩ → ⟨p′′, v1γ′v2⟩ and ⟨p′′, v1⟩ ⇒ ⟨p′, ε⟩ then
1 ((p, γ), 1, (p′, γ′)) ∈ E if ⟨p′′, v1⟩
r
⇒ ⟨p′, ε⟩ or p ∈ G
2 ((p, γ), 0, (p′, γ′)) ∈ E otherwise.
IA169 Model Checking: Reachability in Pushdown Systems 44/51
Example
Construct the graph G for BP = ({p0, p1, p2}, {γ0, γ1, γ2}, ∆, {p2}), where
∆ = { ⟨p0, γ0⟩ → ⟨p1, γ1γ0⟩, ⟨p2, γ2⟩ → ⟨p0, γ1⟩,
⟨p1, γ1⟩ → ⟨p2, γ2γ0⟩, ⟨p0, γ1⟩ → ⟨p0, ε⟩ }.
p0, γ0 p1, γ1
p2, γ2p0, γ1
0
1
0
1
IA169 Model Checking: Reachability in Pushdown Systems 45/51
Example
Construct the graph G for BP = ({p0, p1, p2}, {γ0, γ1, γ2}, ∆, {p2}), where
∆ = { ⟨p0, γ0⟩ → ⟨p1, γ1γ0⟩, ⟨p2, γ2⟩ → ⟨p0, γ1⟩,
⟨p1, γ1⟩ → ⟨p2, γ2γ0⟩, ⟨p0, γ1⟩ → ⟨p0, ε⟩ }.
p0, γ0 p1, γ1
p2, γ2p0, γ1
0
1
0
1
repeating heads: ⟨p0, γ0⟩, ⟨p1, γ1⟩
IA169 Model Checking: Reachability in Pushdown Systems 46/51
Algorithm: notes
We give an algorithm computing R for a given BP in normal form.
The algorithm runs in two phases.
1 It computes Apre∗ recognizing pre∗({⟨p, ε⟩ | p ∈ P}). Every transition (p, γ, p′)
of Apre∗ signifies that ⟨p, γ⟩ ⇒ ⟨p′, ε⟩.
We enrich the transitions of Apre∗ : transitions (p, γ, p′) are replaced by
(p, [γ, b], p′) where b is a Boolean. The meaning of (p, [γ, 1], p′) should be
that ⟨p, γ⟩
r
⇒ ⟨p′, ε⟩.
2 It constructs the graph G, identifies its strongly connected components
(e.g. using Tarjan’s algorithm), and determines the set of repeating heads.
We define G(p) = 1 if p ∈ G and G(p) = 0 otherwise.
IA169 Model Checking: Reachability in Pushdown Systems 47/51
Algorithm
input : BP = (P, Γ, ∆, G) in normal form
output: the set of repeating heads in BP
1 rel ← ∅; trans ← ∅; ∆′ ← ∅
2 forall ⟨p, γ⟩ → ⟨p′, ε⟩ ∈ ∆ do trans ← trans ∪ {(p, [γ, G(p)], p′)}
3 while trans ̸= ∅ do
4 pop t = (p, [γ, b], p′) from trans
5 if t ̸∈ rel then
6 rel ← rel ∪ {t}
7 forall ⟨p1, γ1⟩ → ⟨p, γ⟩ ∈ ∆ do trans ← trans ∪ {(p1, [γ1, b ∨ G(p1)], p′)}
8 forall ⟨p1, γ1⟩
b′
−→ ⟨p, γ⟩ ∈ ∆′ do trans ← trans ∪ {(p1, [γ1, b ∨ b′], p′)}
9 forall ⟨p1, γ1⟩ → ⟨p, γγ2⟩ ∈ ∆ do
10 ∆′ ← ∆′ ∪ {⟨p1, γ1⟩
b∨G(p1)
−→ ⟨p′, γ2⟩}
11 forall (p′, [γ2, b′], p′′) ∈ rel do
12 trans ← trans ∪ {(p1, [γ1, b ∨ b′ ∨ G(p1)], p′′)} // end of part 1
13 R ← ∅; E ← ∅ // beginning of part 2
14 forall ⟨p, γ⟩ → ⟨p′, γ′⟩ ∈ ∆ do E ← E ∪ {((p, γ), G(p), (p′, γ′))}
15 forall ⟨p, γ⟩
b
−→ ⟨p′, γ′⟩ ∈ ∆′ do E ← E ∪ {((p, γ), b, (p′, γ′))}
16 forall ⟨p, γ⟩ → ⟨p′, γ′γ′′⟩ ∈ ∆ do E ← E ∪ {((p, γ), G(p), (p′, γ′))}
17 find all strongly connected components in G = ((P × Γ), E)
18 forall components C do
19 if C has a 1-edge then R ← R ∪ C
20 return R
IA169 Model Checking: Reachability in Pushdown Systems 48/51
Theorem
Theorem
Let BP = (P, Γ, ∆, G) be a Büchi pushdown system. The set of repeating heads R
can be computed in O(|P|2 · |∆|) time and O(|P| · |∆|) space.
IA169 Model Checking: Reachability in Pushdown Systems 49/51
Theorem
Theorem
Let BP = (P, Γ, ∆, G) be a Büchi pushdown system. The set of repeating heads R
can be computed in O(|P|2 · |∆|) time and O(|P| · |∆|) space.
Proof.
The first part is similar to the algorithm computing Apre∗ .
The size of G is in O(|P| · |∆|). Determining the strongly connected components
takes linear time in the size of the graph [Tarjan1972]. The same holds for
searching each component for an internal 1-edge.
IA169 Model Checking: Reachability in Pushdown Systems 50/51
Theorem
Theorem
Let P be a pushdown system and φ be an LTL formula. The global model
checking problem can be solved in O(|P|3 · |A|3) time and O(|P|2 · |A|2) space,
where A is a Büchi automaton corresponding to ¬φ.
IA169 Model Checking: Reachability in Pushdown Systems 51/51