IA159 Formal Verification Methods
LTL Model Checking of Pushdown Systems
Jan Strejˇcek
Department of Computer Science
Faculty of Informatics
Masaryk University
Focus and sources
Focus
pushdown systems
representation of sets of configurations
computing all predecessors: checking safety properties
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 2/47
Motivation
Pushdown systems can be used to precisely model sequential
programs with procedure calls, recursion, and both local and
global variables.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 3/47
Pushdown systems
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 as language acceptors.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 4/47
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 }
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 5/47
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)
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 6/47
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
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 7/47
Notation convention
In the rest of this section, we use
p, p , p , . . . to denote initial states of an automaton
(i.e. elements of P)
s, s , s , . . . to denote non-initial states, and
q, q , q , . . . to denote arbitrary states (initial or not).
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 8/47
Verification of pushdown systems: the first step
Computing pre∗(C) for a regular set C
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 9/47
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 10/47
Intuition
p1, γ0 → p2, γ1γ2
p3, γ3 → p1, γ0γ1
GFED@ABCp1
γ0
GFED@ABCp2
γ1
//?>=<89:;q
γ2
**?>=<89:;q
γ1
jj //
$$IIIIIIII · · ·
GFED@ABCp3 γ3
JJ
...
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 11/47
Intuition
p1, γ0 → p2, γ1γ2
p3, γ3 → p1, γ0γ1
GFED@ABCp1
γ0
GFED@ABCp2
γ1
//?>=<89:;q
γ2
**?>=<89:;q
γ1
jj //
$$IIIIIIII · · ·
GFED@ABCp3 γ3
JJ
...
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 12/47
Intuition
p1, γ0 → p2, γ1γ2
p3, γ3 → p1, γ0γ1
GFED@ABCp1
γ0
GFED@ABCp2
γ1
//?>=<89:;q
γ2
**?>=<89:;q
γ1
jj //
$$IIIIIIII · · ·
GFED@ABCp3 γ3
JJ
...
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 13/47
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∗
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 14/47
Example
Apre∗ GFED@ABCp0
γ0
//
γ1

γo
##
GFED@ABCs1
γ0
//GFED@ABC?>=<89:;s2
GFED@ABCp1
γ1
99ssssssss
γ1
::
GFED@ABCp2
γ2
==
transition rules of P:
p0, γ0 → p1, γ1γ0 p2, γ2 → p0, γ1
p1, γ1 → p2, γ2γ0 p0, γ1 → p0, ε
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 15/47
Example
Apre∗ GFED@ABCp0
γ0
//
γ1

γo
##
GFED@ABCs1
γ0
//GFED@ABC?>=<89:;s2
GFED@ABCp1
γ1
99ssssssss
γ1
::
GFED@ABCp2
γ2
==
transition rules of P:
p0, γ0 → p1, γ1γ0 p2, γ2 → p0, γ1
p1, γ1 → p2, γ2γ0 p0, γ1 → p0, ε
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 16/47
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 17/47
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 18/47
Algorithm
Input: a pushdown system P = (P, Γ, ∆) in normal form
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
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 19/47
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 20/47
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 · |∆|.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 21/47
Proof: time complexity
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 22/47
Proof: space complexity
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 23/47
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 24/47
Verification of pushdown systems: the second step
LTL model checking
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 25/47
The problem
The global state-based LTL model checking problem
for pushdown processes
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 ϕ).
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 26/47
Extending pushdown systems
state-based =⇒ validity of atomic propositions
labelling 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)
labelling function is an extension of L: L( p, γw ) = L(p, γ)
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 27/47
The schema
pushdown system P
with labelling function L

LTL formula ϕ

Kripke structure
with infinitely many states
((RRRRRRRRRR
Büchi automaton A¬ϕ
words over 2AP(ϕ) violating ϕ
vvlllllllll
product: Büchi pushdown system BP

Accepting run problem
to compute the set of all configurations
of BP where accepting runs start
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 28/47
Büchi pushdown system
Büchi pushdown system = pushdown system with a set
of accepting control locations.
An accepting run of a Büchi pushdown system is a path
passing through some accepting control location infinitely often.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 29/47
Product
Product of
a pushdown system P = (P, Γ, ∆) with a labelling L and
a Büchi automaton A¬ϕ = (2AP(ϕ), Q, δ, q0, F)
is a Büchi pushdown system BP = ((P × Q), Γ, ∆ , G), where
(p, q), γ → (p , q ), w ∈ ∆ if p, γ → p , w ∈ ∆ and
q ∈ δ(q, L(p, γ) ∩ AP(ϕ))
and G = P × F.
Clearly, a configuration p, w of P violates ϕ if BP has an
accepting run starting from (p, q0), w .
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 30/47
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 31/47
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 if c ⇒ g, u
+
⇒ c
for some configuration g, u with g ∈ G.
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 32/47
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 ∈ Γ∗.
The implication “⇐=” is obvious.
We prove “=⇒”.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 33/47
Proof
assume that BP has an accepting run
p0, w0 , p1, w1 , p2, w2 , . . .
starting from 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
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 34/47
Proof
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 “=⇒”
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 35/47
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
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 36/47
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 37/47
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 38/47
Computing R
Once G is constructed, R can be computed using the fact that:
(p, γ) is in a strongly connected
a head p, γ is repeating ⇐⇒ component of G which has an
internal edge labelled with 1
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 39/47
Example
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 40/47
Example
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, ε }.
_^]\XYZ[p0, γ0
0 //
_^]\XYZ[p1, γ1
1
oo
0

_^]\XYZ[p0, γ1 _^]\XYZ[p2, γ2
1oo
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 41/47
Example
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, ε }.
_^]\XYZ[p0, γ0
0 //
_^]\XYZ[p1, γ1
1
oo
0

_^]\XYZ[p0, γ1 _^]\XYZ[p2, γ2
1oo
Repeating heads: p0, γ0 , p1, γ1
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 42/47
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 of Apre∗ : transitions (p, γ, p ) are replaced by
(p, [γ, b], p ) where b is a boolean. The meaning of a
transition (p, [γ, 1], p ) should be that p, γ
r
⇒ p , ε .
2 It constructs the graph G, identifies its strongly conected
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 43/47
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
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 44/47
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.
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.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 45/47
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 · |B|3)
time and O(|P|2 · |B|2) space, where B is a Büchi automaton
corresponding to ¬ϕ.
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 46/47
Coming next week
Abstraction
How to verify large systems?
How to find a good abstraction?
When is an abstraction considered to be good?
IA159 Formal Verification Methods: LTL Model Checking of Pushdown Systems 47/47