The Complexity of Model Checking (Collapsible)
Higher-Order Pushdown Systems
Matthew Hague1 and Anthony Widjaja To2
1,2 Oxford University Computing Laboratory
Wolfson Building, Parks Road
Oxford, OX1 3QD

Abstract
We study (collapsible) higher-order pushdown systems — theoretically robust and wellstudied models of higher-order programs — along with their natural subclass called (collapsible)
higher-order basic process algebras. We provide a comprehensive analysis of the model checking complexity of a range of both branching-time and linear-time temporal logics. We obtaintight bounds on data, expression, and combined-complexity for both (collapsible) higher-order
pushdown systems and (collapsible) higher-order basic process algebra. At order-k, results range
from polynomial to (k + 1)-exponential time.
1998 ACM Subject Classification D.2.4
Keywords and phrases Higher-Order, Collapsible, Pushdown Systems, Temporal Logics, Complexity, Model Checking

1

Introduction

Recently, there has been a burgeoning interest in collapsible higher-order pushdown systems (CPDSs), both as generators of structures and as models of higher-order computation. Whereas an order-1 pushdown system augments a finite-state automaton with anunbounded stack memory, a higher-order pushdown system (HOPDS) provides a nested“stack-of-stacks” structure. CPDSs allow a further backtracking operation called collapse.
Higher-order pushdown automata (HOPDA) were introduced by Maslov [24]. Higherorder pushdown systems (HOPDS) are HOPDA viewed as generators of infinite trees orgraphs. Recently these models have been generalised to collapsible pushdown systems(CPDS) [17, 19]. In terms of expressivity, order-k CPDSs generate the same class of ranked
trees as deterministic order-k recursion schemes [17]. The analogous result holds for safe recursion schemes and HOPDSs [18]. These systems provide a natural model for higher-orderprograms with (unbounded) recursive function calls and are therefore useful in software verification. Further results show an intimate connection with the Caucal hierarchy [10, 11].
For verification, reachability properties — which ask whether a given set of control states
can be reached from the initial configuration — are complete for (k − 1)-ExpTime [5, see appendix], whilst µ-calculus properties are k-ExpTime-complete [7, 26, 17]. Despite these highcomplexities, Kobayashi has verified resource usage properties of higher-order programs [20]using a novel approach based on intersection types [21, 23].
Hitherto, there has been little work addressing the precise complexity of model checking
higher-order programs with respect to the common temporal logics. In most cases, there
is currently a single or double exponential gap in the best known upper and lower bounds(derived usually from µ-calculus and reachability respectively). One main contribution ofthis paper is a nearly complete picture of the model checking complexities against temporal© M. Hague and A. W. To;
licensed under Creative Commons License NC-ND
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

2

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems(Collapsible) HOPDS
Expression& Combined(k − 1)-ExpTime
k-ExpTime(k − 1)-ExpTime
k-ExpTime(k − 1)-ExpTime
k-ExpTimek-ExpTimek-ExpTimek-ExpTime(k + 1)-ExpTime
k-ExpTime(k + 1)-ExpTime(k − 1)-ExpSpace-hard(k − 1)-ExpSpace-hard
DataµLTL / LTL
LTL(F, X)
LTL(U)
CTL
CTL+
CTL*
EF

(Collapsible) HOBPA
Expression& Combined
P-timek-ExpTimeP-timek-ExpTimeP-timek-ExpTimeP-timek-ExpTimeP-time(k + 1)-ExpTime
P-time(k + 1)-ExpTime
P-time(k − 1)-ExpSpace-hard
Data

Figure 1 The complexity of model checking order-k higher-order systems. Unless stated, allresults are complete.

logics. In particular, we consider data complexity (formulas are fixed), expression complexity (systems are fixed), and combined complexity (both formulas and systems are input
parameters). Table 1 (left column) summarises our results. In all cases, our lower bounds
hold without the collapse operation, whilst our upper bounds allow collapse.
Basic process algebras (BPAs) are a natural and well-studied subclass of order-1 PDSs (cf.
[6]), which are suitable abstractions for modelling the control-flow of sequential programs (cf.
[2, 14]). We propose higher-order extensions of BPAs, called (collapsible) higher-order basic
process algebras (HOBPAs), that form a natural subclass of (collapsible) HOPDSs. Thisdiffers from the single-state HOPDSs introduced by Bouajjani and Meyer [3]. As graphgenerators, (collapsible) HOBPAs are almost as powerful as (collapsible) HOPDSs in thefollowing sense: (1) like CPDS, there exists a collapsible order-2 BPA whose graph has anundecidable monadic second-order logic (MSO) theory, and (2) the class of graphs generated
by order-k BPAs coincide with those generated by order-k PDSs up to MSO interpretations.
In this paper, we provide an almost complete picture for the model checking complexities ofstandard temporal logics over (collapsible) HOBPAs. See Table 1 (right column). We showthat the restriction to HOBPA does not, in most cases, simplify the model checking problem;a notable exception is for data complexity, where the problem becomes polynomial time.
Again, our lower bounds hold without collapse, whilst our upper bounds allow collapse.
Similar analyses appear across a number of papers for the special case of order-1 pushdown systems [1, 6, 30, 31, 4]. In all cases we generalise the resulting picture in a naturalmanner. That is, a 1-ExpTime-complete complexity becomes k-ExpTime-complete, andso on. Our upper bound results concern the data complexity of Collapsible HOBPAs andthe data and combined complexities for LTL over CPDSs. Previous work studied reachability, LTL and the alternation-free µ-calculus [16, 27, 13] over HOPDS without collapse.
However, we believe the LTL algorithm contains an error, and provide a new algorithm.
Furthermore, the alternation-free µ-calculus algorithm in [16] is not optimal. Our remaining results concern lower bounds. We begin with two techniques from in the literature:(1) Engelfriet’s characterization of complexity classes k-ExpTime by extensions of HOPDAs(e.g. with space-bounded worktape) [13], and (2) Cachat and Walukiewicz’s more “direct”
approach via encodings of large numbers using HOPDSs [8]. We employ Technique (1) toprove the lower bounds for LTL (and its fragments), CTL, CTL+, and CTL*. This does
not mean that the proofs of the results are immediate: it was left as an open problem in[8] whether the two techniques can be used to derive these lower bounds. Since Technique(1) seems only suited to deriving k-ExpTime lower bounds (for some k), we give two variations of Technique (2) to derive (k − 1)-ExpSpace lower bounds for EF model checking over
HOPDSs and HOBPAs (the latter proof is substantially more involved). The lower boundproofs in this paper suggest that Technique (1) yields simpler proofs, while Technique (2)M. Hague and A. W. To

3

offers more flexibility.
The preliminaries are given in §2. We begin in §3 with the results for fixed formulas overcollapsible HOBPA. In §4 we discuss branching-time logics, and linear-time in §5. Finally,
we conclude this paper with future work in §6. Due to the length and intricate nature of
the proofs, we relegate the full details into the full version.

2

Preliminaries

We define (collapsible) higher-order pushdown systems and basic process algebra and givea result of Engelfriet used in some proofs. Note, after defining higher-order and collapsible
stores, we only define higher-order systems. For the collapsible version, simply replace thehigher-order store with a collapsible one, expanding the stack operations accordingly. Also,
the definitions generalise from non-deterministic to alternating in the standard way.

Higher-Order Collapsible Pushdown Stores
We begin by defining a higher-order pushdown store. Collapse links will be introduced
afterwards. Intuitively, a higher-order store is a stack of lower order stacks.
I Definition 1 (k-Stores). Let C0Σ be a finite alphabet Σ with [, ] ∈/ Σ. For k ≥ 1, the set ofΣ
k-stores CkΣ contains all [γ1 . . . γm ] with m ≥ 1 and γi ∈ Ck−1
for all 1 ≤ i ≤ m.
There are two operations defined over 1-stores (for all w ∈ Σ∗ )pushw [a1 . . . am ] = [wa2 . . . am ]andtop1 [a1 . . . am ] = a1 .

We define pop1 = pushε . Let O1 = { pushw | w ∈ Σ∗ }. When k > 1, a push operation
creates a copy of the topmost stack, while a pop removes it. We assume w.l.o.g. thatΣ ∩ N = ∅, where N is the set of natural numbers. Finally, let [γ1 . . . γm ] ∈ CkΣ for some k.
pushw [γ1 . . . γm ]pushl [γ1 . . . γm ]pushk [γ1 . . . γm ]popl [γ1 . . . γm ]popk [γ1 . . . γm ]topl [γ1 . . . γm ]topk [γ1 . . . γm ]

=
=
=
=
=
=
=

[pushw (γ1 )γ2 . . . γm ][pushl (γ1 )γ2 . . . γm ] if 2 ≤ l < k[γ1 γ1 γ2 . . . γm ][popl (γ1 )γ2 . . . γm ]if 1 ≤ l < k[γ2 . . . γm ]if m > 1
topl (γ1 )if 1 ≤ l < kγ1Note, when m = 1, popk is undefined. Let Ok = { pushw | w ∈ Σ∗ } ∪ { pushl , popl | 1 <l ≤ k }. We designate ⊥ to be a bottom of stack symbol that is neither pushed nor popped.
Let [w]1 = [w] and [w]k = [[w]k−1 ].
For collapse, the order-1 push operation pushw is replaced with pushai1 ...aim b for 1 ≤m1
iz ≤ k and az , b ∈ Σ where 1 ≤ z ≤ m. A pushai1 ...aim b on some stack with top1 characterm1
a is equivalent to pusha1 ...am b except each az is augmented with a pair (iz , 1). That is,(i ,1)(i ,1)
the top of stack character a(i,j) is replaced by a1 1 . . . amm b(i,j) . The collapse operation(i,j)
from a character ais equivalent to j applications of popi . The second component j isincremented at every pushi . Hence, (i, j) is a link to the order-(i − 1) stack beneath thecharacter when it was first pushed.
 (2,1) Consider [[[⊥] [⊥]]].
pusha2 ⊥ givesa⊥ [⊥] . The pair (2, 1) points toApplying[⊥]. A push2 leads to a(2,2) ⊥ a(2,1) ⊥ [⊥] . Note the second component is incremented
in the copy of a, and, thus, (2, 2) also points to [⊥]. A subtlety occurs after a push3 . We

4

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

obtain the stack below on the left, where the copies of a now refer to the copies of [⊥] within
the order-2 stack they occupy. After a collapse, we obtain the stack on the right.
   (2,2)   (2,1) 


a
⊥
a
⊥
[⊥]
 (2,2)   (2,1)  (2,2) [[⊥]]
 (2,1) 

a
⊥ a
⊥ [⊥]
a
⊥ a
⊥ [⊥]
Formally, weorder-k stores with links in terms of order-k stores over the infinite
 define(i,j)
alphabet Σ = a| i, j ∈ N . The set of operations over an order-k store with links is
Okc

=

n

pushai1 ...aim b | ∀1 ≤ z ≤ m.1 ≤ iz ≤ k ∧ az ∈ Σ

o

m

1

∪ { pushl , popl , collapse | 1 < l ≤ k } .

Note that this set of operations is slightly different from the original definition [17]. We show,
in the full version, that the definitions are equivalent. The semantics of the operations are
given below, in terms of the standard order-k pushdown operators, and an order-k stackγ = [γ1 . . . γm ]. Let γ <k> be the stack γ where each superscript (i, j) with i ≥ k is replacedwith (i, j + 1).
pushai1 ...aim b (γ)
1

m

=

0

0

pusha(i1 ,1) ...a(im ,1) b(i0 ,j0 ) (γ) where top1 (γ) = b(i ,j )1mm

collapse(γ) = popji (γ)
pushk [γ1 . . . γm ] = [γ1<k> γ1 . . . γm ]pushl [γ1 . . . γm ] = [pushl (γ1 )γ2 . . . γm ]where top1 (γ) = b(i,j)
where l < kHigher-Order Pushdown Systems
A HOPDS is a finite-state system with a higher-order store. The finite-state component
is the control state. At each step, the applicable transitions are determined by the control
state and the top1 character of the stack. Each transition updates the control state and thestack.
I Definition 2. An order-k PDS is a tuple (P, R, Σ, p0 , ⊥) where P is a finite set of control
states, R ⊆ P × Σ × Ok × P is a finite set of rules, Σ is a finite stack alphabet, p0 ∈ P is an
initial control state and ⊥∈ Σ is a bottom of stack symbol.
A configuration of a higher-order PDS is a pair hp, γi where p ∈ P and γ is a k-store.
We have a transition hp, γi ,→ hp0 , γ 0 i iff we have (p, a, o, p0 ) ∈ R, top1 (γ) = a and γ 0 = o(γ).
The initial configuration is hp0 , [⊥]k i.

Higher-Order Basic Process Algebra
An order-1 BPA is an order-1 PDS with a single control state. By applying the same restriction, Bouajjani and Meyer have obtained one definition of higher-order BPA [3]. However,consider hp, [[a ⊥]]i and the rule (omitting the control) (a, push2 ). We obtain hp, [[a ⊥] [a ⊥]]iand the same rule can be applied, ad infinitum. However, at order-1 we may use (a, pushbc )to rewrite the top character before adding a new top character. Hence, at order-j, it is natural to be able to rewrite the top order-(j − 1) stack, before adding a new one. Consequently,
we introduce (a, pushj , b) = pusha ; pushj ; pushb for all 2 ≤ j ≤ k. E.g., such rules can simulate push2 ; push3 ; pop2 . Let Ok0 = { pushw | w ∈ Σ∗ } ∪ { (a, pushj , b), popj | 1 < j ≤ k }.
I Definition 3. An order-k BPA is a tuple (R, Σ, ⊥) where R ⊆ Σ × Ok0 is a finite set ofrules, Σ is a finite stack alphabet, and ⊥∈ Σ is the bottom of stack symbol.

M. Hague and A. W. To

5

We mention two results on the expressive power of HOBPAs as graph generators. Familiarity with monadic second-order logic (MSO) is assumed (cf. [28]). As graph generators,(collapsible) HOBPAs are as powerful as (collapsible) HOPDAs up to monadic second-orderlogic (MSO) interpretation in the following sense. First, it is known that there exists anorder-2 CPDA generating a graph with an undecidable MSO theory [17]. In contrast, over
HOPDAs, MSO is decidable. This CPDA is not a collapsible HOBPA. On the other hand,using the ideas from [17], it is not difficult to come up with an order-2 collapsible HOBPA
generating a graph with an undecidable MSO theory.
I Proposition 1. There exists a fixed collapsible order-2 BPA which generates a graph withan undecidable MSO theory.
We sketch the proof of this proposition in the full version. Secondly, we discuss the expressive
power of HOBPAs without collapse. Carayol and Wöhrle [9, 10] gave a fixed graph ∆k2 , foreach integer k > 0, such that the class of graphs that are MSO-interpretable in the graphs
generated by order-k PDSs coincide with the class of graphs that are MSO-interpretable in∆k2 . It is easy to check that ∆k2 can be generated by a fixed order-k BPAs (e.g. see [9]),which implies the following proposition.
I Proposition 2. The class of graphs that are MSO-interpretable in the graphs generated byorder-k BPAs coincide with the class of graphs MSO-interpretable in the graphs generated
by order-k PDSs.

Higher-Order Pushdown Automata with an Auxiliary Work Tape
For the lower bound proofs we use HOPDA with a space-bounded work tape. That is, inaddition to the control state and the stack, the machine has a bounded, two-way work tape.
This tape operates identically to the tape in a Turing machine.
I Definition 4. An order-k PDA with an s(n)-space work tape is a tuple (P, R, Σ, Γ ∪{ε} , ∆, p0 , ⊥, 2, F) where P is a finite set of control states, R ⊆ (P × Γ ∪ {ε} × Σ × ∆) ×
Ok × (∆ × {l, r} × P ) is a finite set of rules, Σ is a finite stack alphabet, Γ is a finite input
alphabet, ∆ is a finite tape alphabet, p0 ∈ P is an initial control state, ⊥∈ Σ is the bottomof stack symbol, 2 ∈ ∆ denotes a blank tape cell and F ⊆ P is a set of accepting control
states.
Given an input word of length n, a configuration of a HOPDA with s(n) bounded work
tape is a tuple hp, γ, t, ji where p ∈ P , γ is a k-store, t (the tape contents) is a word in ∆s(n)and 1 ≤ j ≤ s(n) indicates the position of the read/write head on the tape.
A rule (p, α, a, x, o, y, d, p0 ) ∈ R can be applied when the current control state is p, theinput character is α, the top-of-stack character is a, and the tape contents at position j are
x. The control state is then updated to p0 , the command o is applied to the stack, and y is
written to the tape. The tape head moves accordingly for d = l (left) or d = r (right).
αMore formally, we have a transition hp, γ, t, ji ,−→ hp0 , γ 0 , t0 , j 0 i iff we have00(p, α, a, x, o, y, l, p ) ∈ R, j > 1, top1 (γ) = a, t(j) = x, γ = o(γ), t0 (j) = y, t0 (h) = t(h) forall h 6= j and j 0 = j − 1 or we have (p, α, a, x, o, y, r, p0 ) ∈ R, j < s(n), top1 (γ) = a, t(j) = x,αγ 0 = o(γ), t0 (j) = y, t0 (h) = t(h) for all h 6= j and j 0 = j − 1. For α 6= ε, we write c ,−→ε c0whenever there is a sequence of ε-transitions from c to some c1 , an α-transition from c1 to
c2 and a sequence of ε-transitions to c0 . A word α1 , . . . , αn is accepted by the automaton iff
α1αncn = hp, γi and p ∈ F and c0 ,−→ε · · · ,−→ε cn where c0 = hp0 , [⊥]k , 2s(n) , 1i.

6

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

Temporal Logics
We will assume familiarity with the temporal logics discussed, remarking only that µLTL is
LTL extended with fixed point operators. Full definitions can be found in the literature [12,29]. We assume, for all logics, the valuations of atomic propositions depend only on thecontrol state and current top-of-stack character, referred to as a head. That is, Λ : P × Σ →2P rop is an assignment of satisfied atomic propositions from the set P rop to each head in
P × Σ. We say a system satisfies a formula if it holds at the initial state of the system.

Engelfriet’s Results
We use the following theorem of Engelfriet [13] in some proofs. Let NSPACE(s(n))-P k denote the class of languages accepted by a non-deterministic order-k PDA with an s(n)-spacebounded work tape, where n is the length of the input word. Similarly, ASPACE(s(n))-P k
denotes the class of languages accepted by an alternating order-k PDA with an s(n)-spaceS
bounded work tape. Finally d>0 DTIME(expk (ds(n))) is the class of languages acceptedby a time-bounded Turing machine, where exp0 (x) = x and expk (x) = 2expk−1 (x) .
I Theorem 5 ([13], Thm. 2.5). For any k ≥ 1 and s(n) ≥ log(n), we have NSPACE(s(n))SP k = ASPACE(s(n))-P k−1 = d>0 DTIME(expk (ds(n))).
That is, a non-deterministic order-k PDA with a polynomially-bounded work tape exists for every k-ExpTime language, and an alternating order-k PDA with a polynomiallybounded work tape exists for every (k + 1)-ExpTime language.

3

Model Checking Collapsible HOBPA Against Fixed Formulas

We begin with a P-time algorithm for model checking collapsible HOBPA against fixed
formulas. Hardness follows from the P-time-hardness of context-free language emptiness [15].
I Theorem 6. For any logic that can be translated into µ-calculus, model checking collapsible
HOBPA against a fixed formula is in P-time.
Proof. As argued in the full version, any collapsible HOBPA can be simulated by a CPDS
with a fixed number of control states. Therefrom, and since the formula is fixed, we construct
a CPDS parity game with a fixed number of control states. At order-k, the winner of thesegames can be determined in k-ExpTime in the number of control states, and polynomial in
the alphabet [17]. Hence, the algorithm runs in P-time.
J

4

Branching TimeWe begin by observing, for CPDS, the upper bounds for CTL, CTL+ and CTL* can beobtained by translating into µ-calculus, which has a k-ExpTime model checking problem.
For CTL, the translation is polynomial. For CTL+ and CTL* it is exponential, giving(k + 1)-ExpTime, and k-ExpTime when the formula is fixed. For the lower bound results,
we discuss EF, CTL and then CTL+.
I Theorem 7. For a fixed formula, and a given order-k CPDS, model checking CTL, CTL+
and CTL* is in k-ExpTime. For a non-fixed system and non-fixed formula, CTL is kExpTime, and CTL+ and CTL* are in (k + 1)-ExpTime.

M. Hague and A. W. To

4.1

Lower Bounds for EF

In most cases, we are able to derive optimal lower bounds using Theorem 5. However,
Theorem 5 is not immediately applicable for (e.g.) (k − 1)-ExpSpace problems. In thecase of EF-logic, the model checking problem over order-1 PDSs and BPAs is PSpacecomplete [25, 31]. We now give (k − 1)-ExpSpace lower bounds for data complexity oforder-k PDSs and the expression complexity of order-k BPAs (and thus of order-k PDSs)
using the technique of [8] of encoding large numbers. We conjecture that these lower bounds
are tight (currently, the best upper bound is k-ExpTime, which is inherited from µ-calculus).
I Theorem 8. Model checking EF over order-k PDS without collapse is (k − 1)-ExpSpacehard, even for a fixed formula.
Proof. (sketch) We reduce membership for a given (k − 1)-ExpSpace Turing machine M
using expk−1 (p(n)) space on an input word of length n, for some polynomial function p. Fix
a number m ∈ Z>0 , which we will later define as p(n) once n is set. The proof combines thetechnique of [1] for proving that EF-logic over PDS is PSpace-hard and the technique of [8]for encoding and checking large numbers (i.e. k-towers of exponentials) using operations inOk .
We shall start by briefly recalling the encoding techniques of large numbers from [8]. For
Sieach i ∈ Z>0 , we define Σi := {ai , bi } and Σ≤i := j=1 Σi . We now define the notion of
i-counters by induction. A 1-counter (of length m) is a word σm−1 . . . σ0 ∈ (Σ1 )m . Such a
Pm−1
word naturally represents the number i=0 σi 2i where a1 represents 0 and b1 represents
1. Assuming that the notion of i-counter has been defined, an (i + 1)-counter is simply aword σr lr . . . σ0 l0 over Σ≤i+1 , where r = expi (m) − 1, σj ∈ Σi+1 , and lj is an i-counterPr
representing the number j. This (i + 1)-counter represents the number j=0 σj 2j , where(as before) ai+1 and bi+1 are used to (respectively) represent 0 and 1.
Cachat and Walukiewicz [8] showed that a polynomial-size order-k pushdown game arena
P with a reachability objective could be defined (depending only on m) with the following
control states and properties: counterk — from configuration (counterk , γ) of P, Player
0 wins iff γ ends with a k-counter; f irstk (resp. lastk ) — from configuration (f irstk , γ)(resp. (lastk , γ), Player 0 wins iff γ ends with a k-counter representing 0 (resp. expk−1 (m));
equalk — from (equalk , γ), Player 0 wins iff γ ends with two k-counters representing equalvalues; succk — from (succk , γ), Player 0 wins iff γ ends with two k-counters representing
successive values. We observe that the game element of P can easily be translated into fixed
EF formulas (i.e. not depending on m) satisfying the same properties, the main reason beingthat the game arena P has a fixed number of rounds.
The rest of the proof uses the idea of [1]. Using an EF operator, we will first guessa word in Σ≤k+1 representing an accepting computation of M on the given input word
w = α1 . . . αn . We then need to check that the guess is valid. That is, it represents asequence of configurations, the initial configuration is the right form, the final configurationis reached, and consecutive configurations respect the transition relation. All these can bedone by means of a fixed formula, thanks to the result above for encoding large numbers. J
I Theorem 9. For a fixed order-k HOBPA without collapse, model checking EF is (k − 1)ExpSpace-hard.
Proof. (sketch) The proof uses some general ideas from the previous proof, but, without
control states to encode tests for large numbers, we need an entirely different construction.
We briefly explain the order-2 case. Our HOBPA P will guess an accepting run of a fixed
exponential space Turing machine M accepting an ExpSpace-complete language, obtaining a7

8

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

stack of the form [w]2 . For the checking stage, our HOBPA P now tries to find some location
inside the stack that is invalid. In doing so, we need to ensure that all of the information
on top of this location is not destroyed. To this end, we will build a stair-like structurefrom [w]2 by performing operations of the form [push1 (a0 ); push2 ; push1 (prime)] or of theform [push1 (a00 ); push2 ; push1 (dprime)] when seeing a topmost stack symbol a. Here, primeand dprime are simply intermediate symbols to help signify the action that was previous
executed, i.e., we could simply only allow pop1 operation when prime or dprime is seen as
topmost symbol. The double prime marking is used to “remember” the starting point of(sub)configuration that we suspect is invalid. That is, we will have to make sure that it isput precisely once. At some point, P simply applies rules of the form push1 (a0 ) when a isseen without applying push2 , which marks the end point of a (sub)configuration that wesuspect is invalid. We then only allow rules pop2 when primed or double primed symbols
are seen. To make sure that we see precisely one separator symbol (i.e. a3 ∈ Σ3 ), we canuse an EF formula saying facts about the location of the double primed symbol a003 . Such a
stair-like structure will allow us to define EF formulas that play the roles of counteri , f irsti ,lasti , equali , and succi and their associated EF formulas in the previous proof.
J

4.2

Lower Bounds for CTL

Data Complexity We know, for a fixed formula, model checking CTL, CTL+ and CTL*
against HOPDSs is in k-ExpTime. Here, we show the lower bound.
I Theorem 10. For a fixed formula, model checking CTL over a given order-k HOPDS
without collapse is k-ExpTime-hard.
Proof. (sketch) From Theorem 5 we take a language that is k-ExpTime-hard and fix anequivalent order-(k − 1) alternating HOPDA with a polynomially space-bounded work tape
P. The reduction is inspired by Bozzelli [4].
We use an order-k stack to navigate a computation tree of the HOPDA. To simulate thework tape, at each step, after an operation on the order-(k − 1) stack, a sequence of tapesymbols are pushed on to the top order-1 stack. Then, the system can do a check branch toensure the guessed tape is consistent with the previous, or continue simulating the execution.
To continue, an order-k push saves the current state (for backtracking), the work tape iserased, the next rule is announced, and a pushk remembers the rule. This process repeats.
Consider the example order-3 stack below.
 
[tw1 ]  [w2 ] ...

[r . . .]
...







[t0 w10 ] [w20 ]  · · · ...

This stack is at a configuration with the tape given by the word t and order-2 stack[[w1 ] [w2 ] . . .], which can backtrack to a configuration with tape t0 and order-2 stack[[w10 ] [w20 ] . . .]. The rule r connects the configurations. When an accepting configurationis seen, or the children of the current node have been fully explored, we backtrack using
popk , and check untested universal branches. The automaton accepts when the (marked)
initial stack is reached. That is, all paths have been explored, and found to be accepting.
The check branches have further branches for each of the polynomially many positionsof the work tape. Each branch uses the control state to find the correct position, and then,using the control state, compares it with the corresponding positions in the previous work
tape, which is recovered via popk operations.

M. Hague and A. W. To

The CTL formula E ((op ∧ AX(check → AF good)) U f in) asserts a path encoding an
accepting tree exists, and checking branches all accept. The proposition op indicates thecurrent path is simulating a tree, and check indicates a checking branch. Finally, good
indicates that the check has been passed, and f in denotes the (successful) completion of therun.
J
Expression Complexity The following theorem takes care of all cases.
I Theorem 11. For a fixed order-k HOBPA without collapse, model checking CTL is kExpTime-hard.
Proof. (sketch) The proof is in stages. First, we adapt Theorem 10, unfixing the formula tofix the HOPDS. A HOBPA is obtained using a more complex formula. There are two main
assertions we move from the HOPDS to the formula. First, the check branch becomes astraight-line sequence of pops and the formula uses sequences of EX to compare positions.
Secondly, the word position being read has to be guessed and added to the work tapeinformation, then checked by the formula. Hence, we have the result for a fixed HOPDS.
To obtain a HOBPA the main difficulty is that control states were used to separate thecheck, backtrack and simulation phases of the model. Here we use the (a, pushj , b) rules
so that, when pushing, the automaton can read a character a, and mark it a in the next
applied rule. Hence the system knows when it is moving up or down the stack, and when
it has simulated a stack action. Also the automaton announces the intended phases. For
example, the check branch announces “check”, removes the work tape, announces “popk ”,
pops, announces “check” again and removes the work tape. The formula can then use EX j
to look into the first tape, and E(tapeU (popk ∧ EX(check ∧ EX j ϕ))) to look j steps into
the next tape, where tape indicates that a tape character is seen.
J

4.3

Lower Bounds for CTL+

For data complexity, the CTL lower bound transfers to CTL+ and CTL*. For the expression
complexity, the following theorem suffices.
I Theorem 12. For a fixed order-k HOBPA without collapse, model checking CTL+ is(k + 1)-ExpTime-hard.
Proof. (sketch) First we adapt the proof of Theorem 10 to show, CTL* is (k + 1)-ExpTimehard. We then replace the CTL* formula with a CTL+ formula. Then we show how to fix
the system, and restrict ourselves to HOBPA.
For a non-fixed formula and system, our CTL* proof adapts Bozzelli’s order-1 proof [4].
Fix a language that is hard for (k + 1)-ExpTime and an equivalent order-(k − 1) alternating
HOPDA with an exponentially space-bounded work tape. The system proceeds as before,
but guesses the length of the work tape and uses a word binn (0)c0 binn (1)c1 · · · binn (2n −1)c2n −1 to represent it, where binn (i) is the n-digit binary representation of i, and cj are cell
contents. The check phase has one branch to check the cell counters are sequential, and theothers, instead of just popping down the stack, mark a position in each tape. The formulaasserts, when markings are sensible, the tape contents are locally consistent. This can, in
fact, be encoded in CTL+ by taking advantage of straight-line parts of the execution andadding extra markings. Obtaining a fixed HOBPA is similar to the CTL case, with someextra tricks. E.g., to ensure each marker is placed once and in the correct order.
J

9

10

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

5

Linear Time

We consider the linear time logics. We first deal with the upper bound for linear timeµ-calculus (µLTL) — and hence LTL — before considering the lower bounds in turn.

5.1

Upper Bounds for µLTL

Since the linear time µ-calculus (µLTL) does not translate polynomially into µ-calculus, weshow the k-ExpTime upper bound of model checking µLTL against CPDS separately. Notethat µLTL trivially subsumes all other linear time logics considered in this paper.
I Theorem 13. Model checking µLTL against order-k CPDSs is in k-ExpTime for a nonfixed formula, and (k − 1)-ExpTime for a fixed formula.
Proof. (sketch) We can translate any µLTL formula ϕ into a Büchi automaton B at an
exponential cost [29]. From a given CPDS P we construct a product CPDS PB = P × B
which has a Büchi acceptance condition such that PB accepts iff P does not satisfy ϕ.
An order-k Büchi CPDS is a CPDS parity game with two colours and only one player.
Hence, non-emptiness can be reduced to determining the winner in a parity game, whichtakes k-ExpTime in the size of the CPDS [17]. Since the Büchi CPDS is exponential in
the size of ϕ, this complexity is too high. The algorithm for an order-k parity game is bya reduction to an order-(k − 1) game of exponential size. Because the Büchi CPDS has
one player, we can avoid the exponential blow up, constructing an order-(k − 1) game ofpolynomial size. This can be solved in (k − 1)-ExpTime in the size of the Büchi CPDS,
giving an algorithm in k-ExpTime for a non-fixed formula, and (k − 1)-ExpTime for a fixed
formula.
J

5.2

Lower Bounds for LTL

We first give a matching lower bound for data complexity (fixed formula) of LTL, which
already hold for its fragments LTL(F,X) and LTL(U). Since we have previously shown thatorder-k HOBPA can be analysed in P-time for fixed formulas, it remains to consider HOPDS.
I Theorem 14. Model checking HOPDS without collapse against fixed LTL(F, X) andLTL(U) formulas is (k − 1)-ExpTime-hard.
Proof. The non-emptiness problem for HOPDS is (k − 1)-ExpTime-complete [13]. This
problem easily reduces to checking the fixed formula G(¬f ), where f holds at all accepting
states. Since this formula is both in LTL(F, X) and LTL(U), we are done.
J
Next we study the expression complexity (fixed system). This is our main result of thissection: already for a fixed order-k HOBPA, both LTL(F, X) and LTL(U) are k-ExpTimehard.
I Theorem 15. Model checking LTL(F, X) and LTL(U) against a fixed HOBPA without
collapse is k-ExpTime-hard.
Proof. (sketch) We take a k-ExpTime-hard language L, and, by Theorem 5, its equivalent
HOPDS with s(n)-bounded space work tape P, for some polynomial s(n). We shall construct
a fixed HOBPA P 0 such that the language L is polynomial-time reducible to the LTL(F,X)
model checking problem over P 0 . We can similarly derive the desired lower bound for LTL(U)by “weakly” simulating the next operators with the until operator in the standard way.

M. Hague and A. W. To
We shall now give an intuition of the construction of P 0 . Our HOBPA P 0 is an “overapproximation” of P in the sense that P 0 can do whatever actions P can do but also more.
We will then use LTL(F,X) formulas to enforce correct simulations. This is of course dueto the fact that P 0 lacks control states and work tape, and its definition should not dependon the input word to P. We shall now elaborate more on how this can be implemented.
Given a word w = α1 . . . αn ∈ Γ∗ , we would like to determine if there is an accepting runof P on w, i.e., a sequence of configurations of the form hp, γ, t, ji starting with a starting
configuration and ending with a final configuration. Here, p is a control state of P, γ is a
k-store, t ∈ ∆s(n) is a tape content, and 1 ≤ j ≤ s(n) is the position of the tape head. We
will represent each such configuration as the topmost symbols of a contiguous sequence ofconfigurations of P 0 . For example, suppose that the current configuration of P is hp, γ, t, ji
where top1 (γ) = a. The HOBPA P 0 will start by having (p, a) as its topmost stack symbol.
It will then keep modifing its topmost symbol to reflect the tape content t and the position j.
This is done by guessing each individual tape cell content from left to right. At some point,
P 0 will nondetermistically choose some rule of P to fire. We simulate this by first executing
the stack operation and then guess some new state, which we put on top of the stack (thisguess is needed because pop operations will destroy control state information). It will thencontinue by guessing next tape content in the same manner. This process can be repeatedindefinitely, unless P 0 decides to go to a final (i.e. sink) state, in which P 0 will just loop
forever. Given an input word w = α1 . . . αn ∈ Γ∗ , we may force a correct simulation of P on
w by P 0 using an LTL(F,X) formula. That is, we give a formula ϕw such that w ∈ L(P) iff
P 0 , c0 6|= ϕw , where c0 is an appropriate initial configuration of P 0 reflecting the initial stateof P. This can be done by first ensuring that each configuration of P in the simulation as acontiguous sequence of configurations of P 0 is valid. In particular, the guessed tape content(reflected by the topmost symbols in this sequence of configurations of P 0 ) must be of lengths(n) and has precisely one tape head, which can be easily expressed in LTL(F,X) using asingle operator G and nestings of next operators of depth s(n) (approximately). Recall thats(n) is a polynomial function. Using the same technique, we also express that two representations of consecutive configurations of P in the simulation respect the transition relationof P. Similarly, we enforce the initial configuration in the simulation and that some final
configuration of P is reached.
J

6

Future Work

There are several avenues of future work. E.g., we have no matching upper bound forthe complexity of EF model checking. Walukiewicz has shown the problem to be PSpacecomplete at order-1 [31]. However, his techniques do not easily extend to HOPDS owing to
the subtleties of higher-order stacks. We may also study simpler logics such as LTL(F).
Acknowledgments. We thank Olivier Serre for interesting discussions and the anonymousreferees for their helpful remarks. This work was partly supported by EPSRC (EP/F036361
and EP/E005039), and was done while the second author was a student at the School ofInformatics, University of Edinburgh.
References
1
2

A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR, p. 135–150, 1997.
A. Bouajjani, P. Habermehl, and R. Mayr. Automatic verification of recursive procedureswith one integer parameter. Theor. Comput. Sci. 295:85–106 (2003)

11

12

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

A. Bouajjani and A. Meyer. Symbolic Reachability Analysis of Higher-Order Context-Free
Processes. In FSTTCS, p. 135–147, 2004.
L. Bozzelli. Complexity results on branching-time pushdown model checking. Theor. Comput.
Sci., 379(1-2):286–297, 2007.
C. Broadbent and L. Ong. On global model checking trees generated by higher-order recursion
schemes. In FOSSACS, p. 107–121, 2009.
O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification on infinite structures. In
Handbook of Process Algebra, Elsevier, 1999.
T. Cachat. Higher order pushdown automata, the caucal hierarchy of graphs and parity
games. In ICALP, p. 556–569, 2003.
T. Cachat and I. Walukiewicz. The complexity of games on higher order pushdown automata.
CoRR, abs/0705.0262, 2007.
A. Carayol. Regular sets of higher-order pushdown stacks. In MFCS, p. 168–179, 2005.
A. Carayol and S. Wöhrle. The caucal hierarchy of infinite graphs in terms of logic andhigher-order pushdown automata. In FSTTCS, p. 112–123, 2003.
D. Caucal. On infinite terms having a decidable monadic theory. In Proc. MFCS, p. 165–176,
2002.
E. A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, p.
995–1072, Elsevier, 1990.
J. Engelfriet. Iterated pushdown automata and complexity classes. In STOC, p. 365–373,
1983.
J. Esparza and J. Knoop. An automata-theoretic approach to interprocedural data-flow
analysis. In FoSSaCS, p. 14–30, 1999.
E. M. Gurari. An Introduction to the Theory of Computation. W. H. Freeman & Co., New
York, NY, USA, 1989.
M. Hague. Global Model Checking Higher Order Pushdown Systems. PhD thesis, Oxford
University, 2009.
M. Hague, A. S. Murawski, C.-H. L. Ong, and O. Serre. Collapsible pushdown automata andrecursion schemes. In LICS, p. 452–461, 2008.
T. Knapik, D. Niwinski, and P. Urzyczyn. Higher-order pushdown trees are easy. In FoSSaCS,
p. 205–222, 2002.
T. Knapik, D. Niwinski, P. Urzyczyn, I. Walukiewicz. Unsafe Grammars and Panic Automata.
In ICALP, p. 1450-1461, 2005.
N. Kobayashi. Model-checking higher-order functions. In PPDP, p. 25–36, 2009.
N. Kobayashi. Types and higher-order recursion schemes for verification of higher-orderprograms. In POPL, p. 416–428, 2009.
N. Kobayashi and C.-H. L. Ong. Complexity of model checking recursion schemes for fragments of the modal mu-calculus. In ICALP, p. 223–234, 2009.
N. Kobayashi and C.-H. L. Ong. A type system equivalent to the modal mu-calculus model
checking of higher-order recursion schemes. In LICS, p. 179–188, 2009.
A. N. Maslov. Multilevel stack automata. Probl. Inf. Transm., 15:1170–1174, 1976.
R. Mayr. Strict lower bounds for model checking BPA. Electr. Notes Theor. Comput. Sci.,
18, 1998.
C.-H. L. Ong. On model-checking trees generated by higher-order recursion schemes. In LICS,
p. 81–90, 2006.
A. Seth. An Alternative Construction in Symbolic Reachability Analysis of Second Order
Pushdown Systems. Int. J. Found. Comput. Sci. 19(4): 983-998, 2008.
W. Thomas. Constructing Infinite Graphs with a Decidable MSO-Theory. In MFCS, p.
113–124, 2003.
M. Vardi. A temporal fixpoint calculus. In POPL, p. 250-259, 1988.
I. Walukiewicz. Pushdown processes: Games and model checking. In CAV, p. 62–74, 1996.
I. Walukiewicz. Model checking CTL properties of pushdown systems. In FSTTCS, p. 127–
138, 2000.

M. Hague and A. W. To

A

13

Definition of Collapsible Pushdown Systems

We defineorder-k stores with links in terms of order-k stores over the infinite alphabetΣ = a(i,j) | i, j ∈ N . We define the original set of stack operations [17]. We then define
the rule pushai1 ...aim b used in this paper.
m
1
The set of operations over an order-k store with links isOkc =pushia , rewa , pop1 | 1 ≤ i ≤ k ∧ a ∈ Σ∪ { pushl , popl , collapse | 1 < l ≤ k } .
The semantics of the operations are given below, in terms of the standard order-k pushdown
operators, and an order-k stack γ = [γ1 . . . γm ]. Let γ <k> be the stack γ where eachsuperscript (i, j) with i ≥ k is replaced with (i, j + 1).
pop1 (γ)
rewapushia (γ)= pushε (γ)= pusha(i,j)= pusha(i,1) b(i0 ,j0 ) (γ)
mwhere top1 (γ) = b(i,j)
0 0where top1 (γ) = b(i ,j )collapse(γ) = popji (γ)
where top1 (γ) = b(i,j)<k>pushk [γ1 . . . γm ] = [γ1 γ1 . . . γm ]pushl [γ1 . . . γm ] = [pushl (γ1 )γ2 . . . γm ] where l < k

I Definition 16. An order-k CPDS is a tuple (P, R, Σ, p0 , ⊥) where P is a finite set ofcontrol states, R ⊆ P × Σ × Okc × P is a finite set of rules, Σ is a finite stack alphabet,p0 ∈ P is an initial control state and ⊥∈ Σ is a bottom of stack symbol.
A configuration of a CPDS is a pair hp, γi where p ∈ P and γ is a k-store with links. We
have a transition hp, γi ,→ hp0 , γ 0 i iff we have (p, a, o, p0 ) ∈ R, top1 (γ) is a or a(i,j) for somei, j and γ 0 = o(γ). The initial configuration is hp0 , [⊥]k i.
In this paper we use a slight variation of CPDSs, where
o
n
Okc =
pushai1 ...aim b | ∀1 ≤ z ≤ m.1 ≤ iz ≤ k ∧ az ∈ Σ1m∪ { pushl , popl , collapse | 1 < l ≤ k } .

This is to emphasize the connection to HOPDS. We havepushai1 ...aim b = rewb ; pushiamm ; . . . ; pushia111mThis can easily be simulated by adding (a polynomial number of) intermediate states.
Finally, we observe that a collapsible HOBPA can be simulated by a CPDS of the original
definition with a fixed number of states and a polynomially expanded alphabet. To do so
we expand the alphabet to two kinds of tuples
HOP ush(a, j, b) and CP ush(a, ai11 , . . . , aimm )for all prefixes ai11 , . . . , aimm of some collapsible push rule. For both tuples, a is the top1
character of the stack being simulated. We write hai to denote any character of this form,or simply of the form a.
The first tuple HOP ush(a, j, b) indicates the current top1 character is a, a pushj
is to be performed, then the top1 character is to be replaced by b. We replaceeach rule (a, (b, pushj , c)) with the rules (qnorm , hai, pushHOP ush(b,j,c) , qpush ) for all j 0 ∈{1, . . . , k} and a ∈ Σ, followed by the rule (qpush , HOP ush(b, j, c), pushj , qpushed ) and(qpushed , HOP ush(b, j, c), pushc , qnorm ).

14

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems
The second type of tuples CP ush(a, ai11 , . . . , aimm ) are used to simulate collapsible pushrules. That is, we still need to perform pushia11 ; . . . ; pushiamm . Each rule (a, pushai1 ...aim b ) ism1
replaced by (qnorm , hai, rewCP ush(b,ai1 ,...,aim ),qcpush . Then we add the rulem1

(qcpush , CP ush(b, ai11 , . . . aimm ), pushi1i

i(m−1)CP ush(am ,a11 ,...,a(m−1) ), qcpush )whenever m > 0 for all prefixes of collapsible push rules. Finally we have the rule
(qcpush , CP ush(b), rew(b), qnorm ) .
The remaining rules (a, o) are simply replaced by rules of the form (qnorm , hai, o, qnorm ).

B

Proofs for Branching Time

B.1

Proof of Theorem 8

Theorem 8. Model checking EF over order-k PDS without collapse is (k − 1)-ExpSpacehard, even for a fixed formula.
We will now elaborate our construction of the fixed EF formulas and the order-k PDSs
in more details. Following [8], we could construct in polynomial-time an order-k PDS P
over the stack alphabet Σ≤k+1 with the following pairs (s, ψ) of control states of P and EF
formulas:(counterk , Counterk ) such that (P, hcounterk , γi) |= Counterk iff top2 (γ) ends with ak-counter.
(f irstk , F irstk ) such that (P, hf irstk , γi) |= F irstk iff top2 (γ) ends with a k-counter
representing the number 0.
(lastk , Lastk ) such that (P, hlastk , γi) |= Lastk iff top2 (γ) ends with a k-counter representing the number expk−1 (m) − 1.
(equalk , Equalk ) such that (P, hequalk , γi) |= Equalk iff top2 (γ) ends with two k-countersthat have the same value (separated by one letter from Γk+1 ).
(equalk2 , Equalk2 ) such that (P, hequalk2 , γi) |= Equalk2 iff the two topmost order-1 stacks
in γ ends with k-counters that have the same value.
(succk , Succk ) such that (P, hsucck , γi) |= Succk iff top2 (γ) ends with two k-countersthat are of successive values (the top one is the successor of the lower one).
The EF formulas defined here depend neither on the input word w nor on the Turing machine
M . In fact, [8] defines order-k pushdown game arenas instead of EF formulas. However, one
can easily check that the description translates directly to pairs of EF formulas and HOPDS
as they have a fixed number of rounds (more precisely, the structure of the arena is a treewith no self-loops).
We now describe how to finish the proof. Suppose that M uses expk−1 (p(n)) space andt states. Set m = (log2 (t) + 1) × p(n). A configuration of M can be thought of as a wordfrom {0, 1}∗ of length (log2 (t) + 1) × (expk−1 (p(n)) − 1), where each tape cell of M is now
represented using log(t) + 1 bits as: (1) we need one bit to tell whether head is on topof the current cell, (2) we need one bit to store whether the current tape cell has 0 or 1
(wlog we can assume that the tape alphabet of M is {0, 1}), and (3) assuming that thehead is on top of the current tape cell, we need log2 (t) − 1 bits to describe which state M
is in. In this way, we can represent a configuration of M as a k-counter. Note that the ith
cell in a configuration of M corresponds to the contiguous sequence of bits in the numberM. Hague and A. W. To

represented by this k-counter starting from bit position i × (log2 (t) + 1) to bit position(i + 1) × (log2 (t) + 1) − 1 (starting from least significant bits). Therefore, a computation
sequence of M can be represented by a sequence of k-counters separated by a letter from
Γk+1 . The initial state of the HOPDS is hqstart , [⊥]k i.
We shall describe the proof with games with a fixed number of rounds that can beeasily translated to order-k PDS P and EF formulas φ. The players consist of Player 0(representing EF , EX operators, and ∨) and Player 1 (representing AG, AX operators,and ∧). At the beginning, Player 0 will arbitrarily push1 symbols from Γ≤k+1 which heclaims to represent an accepting computation sequence of M on w. [More precisely, thistranslates to one state s in P, which performs only push1 and at some point might moveto another state s0 (from which s is no longer accessible), and a formula φ of the form
EF (s0 ∧ ψ) for some ψ that we will define shortly.] Player 1 now tries to disprove that theguessed stack content represents an accepting computation. The current stack content looks
like [γ]k , where γ ∈ Γ+
≤k+1 . Player 1 has several choices. First, he could doubt and try todisprove that γ is a sequence of k-counters separated by a letter from Γk+1 . This can beeasily done by repeated applications of pop1 ; each time a letter from Γk+1 is seen, Player 1
may use (counterk , Counterk ). This can be implemented using a single AG operator using
Counterk as a subformula. Second, Player 1 could show that the last configuration is nota final configuration. This could be easily done by checking whether a final state is foundin the last configuration (in between the delimiters from Γk+1 ). Note that since each cell
content is represented as a binary string of length log(t) + 1 (the bits are in Σk ) we willneed a finite-state automaton part that keeps a log(t) + 1 modulo count of the numberof letters from Σk that have been seen thus far when performing pop1 (this can be donein the standard way). Third, Player 1 could show that the first configuration is not an
initial state. For this, we will have to make sure that the first configuration in the sequenceof configurations guessed by Player 0 does not represent q0 w2expk−1 (p(n))−n , where q0 is
the initial state of M . This can be done as follows. We first compute the sequence v of(log(t) + 1)n bits corresponding to q0 w, using ak (resp. bk ) to represent 0 (resp. 1) andhardwire v into P. The system P then performs any number of pop1 operation (making surethat each cell content seen thus far represents 2) and at some point nondeterministicallyguessing the end (rightmost) position of the string that must represent q0 w, after which
P will ensure that precisely v are seen at the beginning (we simply ignore all letters fromΣk−1 and only look at the letter from Σk , noting also that letters from Σk+1 signify theend of the configuration). Fourth, Player 1 could show that some configurations are invalid(e.g. by showing that there are two states in them). This can be done in a similar way(by remembering the first time a state is seen in a configuration and making sure that no
more is seen until we see a letter from Σk+1 ). Fifth, Player 1 could show that there are twoconsecutive configurations Cj and Cj+1 in γ such that Cj is not a predecessor of Cj+1 . To
this end, Player 1 keeps performing pop1 , stops, and picks a position in Cj+1 . Player 1 willthen perform a push2 operation and obtain h[γ 0 ][γ 0 ]i. Player 1 then keeps performing pop1
operations and we will make sure that exactly one letter from Σk+1 is seen. Once Player
1 picks a position in Cj , Player 0 can try to prove that the positions are incorrect. This22
can be done by an application of (equalk−1, Equalk−1). Otherwise, P can remember thecorresponding (at most) four cells in Cj and Cj+1 (using a total of O(log(t)) bits, i.e., weneed 2O(log t) = O(t) extra memory in the control states of P) and check that the positions in
Cj+1 follows the corresponding positions in Cj (according to the transition function of M ).
This can be using pop1 operations interleaved with exactly one application of pop2 , while
remembering the content of eight cells inside the control states of P. This technique was

15

16

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

first used in [1] to encode linear bounded Turing machine as an EF model checking problem(for a fixed formula) over order-1 PDSs. Finally, we can see that the resulting EF-formula
is fixed and the size of the resulting HOPDS is polynomial in |w| and |M | (recall also that
M is fixed). This completes the proof.

B.2

Proof of Theorem 9

Theorem 9. For a fixed order-k HOBPA without collapse, model checking EF is (k − 1)ExpSpace-hard.
We use the notion of i-counters from the previous proof. Fix positive integers n andk > 1. Fix a polynomial function p. For a finite set Q, a (k, Q)-counter is a word of theform σr lr . . . σ0 l0 where
each σi is a letter in Σk ∪ Q,
each li is a (k − 1)-counter representing the number i, andr = expk (p(n)) − 1.
Note that the notions of k-counters and (k, ∅)-counters coincide. We shall now define an order
2-BPA P := P2,Q = (R, Σ, c0 ) that depends only on Q and show that EF model checking
over P is 1-ExpSpace-hard. We will later set Q to be the set of states of a fixed (k − 1)ExpSpace-complete Turing machine. We will then argue that the same construction canbe generalised to show (k − 1)-ExpSpace-hard expression complexity of EF model checking
over k-BPAs.
At the beginning, our 2-BPA must write a sequence of (2, Q)-counters that potentiallygives an accepting computation of a fixed 1-ExpSpace-complete Turing machine. Since
the definition should not depend on the input word of a fixed Turing machine, we define+
the languages L2 := (Σ+and L02 := (L2 Σ3 )+ . Intuitively, L2 is the smallest
1 (Σ2 ∪ Q))“overapproximation” of the notion of (2, Q)-counters that does not depend on n. Hence,
L02 is an overapproximation of all sequences of (2, Q)-counters separated by a letter from
Σ3 . Initially our 2-BPA will be able to guess a word in L02 , i.e., a potential sequence of(2, Q)-counters separated by a letter in Σ3 . The starting configuration c0 is [(guess, 3)]kwhere (guess, 3) is a symbol in Σ. We add the following rules to R:((guess, 3), push((guess, 2)σ3 )) for each σ3 ∈ Σ3 ,((guess, 2), push((guess, 1)σ2 )) for each σ2 ∈ Σ2 ∪ Q,((guess, 1), push((guess, 1)σ1 )) for each σ1 ∈ Σ1 ,((guess, 1), push((guess, 20 )σ1 )) for each σ1 ∈ Σ1 ,((guess, 20 ), push((guess, 3)), and((guess, 20 ), pop1 ) for each σ3 ∈ Σ3 .
The last transition marks the end of the guessing stage as we will no longer see stack symbolof the form (guess, i) afterwards. We now introduce several transitions that will allow us to
use EF formulas to check the correctness of the guess from the previous stage. For i = 1, 2, 3,
let Σ0i := {a0i , b0i } and Σ00i := {a00i , b00i }. Also, let Q0 = {q 0 : q ∈ Q} and Q00 = {q 00 : q ∈ Q}.
S3
S3
Let P rime := Q0 ∪ i=1 Σ0i and DP rime := Q00 ∪ i=1 Σ00i . Add the following rules:
For i = 1, 2, 3, when σi ∈ Σi is seen, we can nondeterministically choose any of thefollowing four choices:push1 (σi0 )push1 (σi00 )(σi0 , push2 , unmarkedi )(σi00 , push2 , markedi )When q ∈ Q is seen, we can nondeterministically choose any of the following four choices:M. Hague and A. W. To

17

push1 (q 0 )push1 (q 00 )(q 0 , push2 , unmarkedQ)(q 00 , push2 , markedQ)
For i = 1, 2, 3, when we see either σi0 ∈ Σ0i ∪ Q0 or σi00 ∈ Σ00i ∪ Q00 , we can only perform
pop2 .
For i = 1, 2, 3, when we see either markedi , unmarkedi , markedQ , or unmarkedQ , we
can only perform pop1 .
To get an intuition, let us look at an example. Suppose that the current stack content is[a3 b1 a1 qb1 b1 a3 ]2 . The following is a snapshot of a run:
a3
q
a1
b1
a3

→

a3
q
a1
b1
a3

marked3
q
a1
b1
a3

→

a3
q
a1
b1
a3

q
a1
b1
a3

→

a3
q
a1
b1
a3

q0
a1
b1
a3

markedQ
a1
b1
a3

→

a3
q
a1
b1
a3

q0
a1
b1
a3

a1
b1
a3

In this way, we obtain a stair-like structure from the stack content [w]2 from the initial
guessing stage. That is, we “unroll” the content of the topmost 1-store.The following are
simple properties that can be established about every reachable configuration c of P2,Q :S3(P1) Every 1-store in c has at most one symbol from (Q0 ∪ Q00 ) ∪ i=1 (Σ0i ∪ Σ00i ), i.e., on
the top of the store.
S3
S3(P2) If c |= (Q0 ∪ Q00 ) ∪ i=1 (Σ0i ∪ Σ00i ) and c →∗ c0 , then c0 |= (Q0 ∪ Q00 ) ∪ i=1 (Σ0i ∪ Σ00i )too.
We now will define several EF formulas that play the roles of Counteri , Equali , etc. in
the previous proof. These formulas shall depend on the parameter n and the polynomial
p(n)
p(n)
p. First, we can easily define Counter1
such that P2,Q , c |= Counter1
iff the topmost
p(n) + 2 symbols on the topmost 1-store of c is of the form σ2 vγ2 for some σ2 , γ2 ∈ Σ2 ∪ Q
and some v ∈ (Σ1 )p(n) . This can be done using nested EX operators, conjunctions, atomic
propositions, and no EF operators, since we have to unroll the topmost 1-store up to p(n)+2
p(n)
p(n)
p(n)
times. Similarly, we can define F irst1(resp. Last1 ) such that P2,Q |= F irst1(resp.
p(n)P2,Q |= Last1 ) iff the topmost p(n) + 2 symbols on the topmost 1-store of c is σ2 vσ20 for
p(n)
p(n)
σ2 , σ20 ∈ Σ2 ∪ Q and v = a1
(resp. v = b1 ).
p(n)
p(n)
We now define the formula Equal1
such that P2,Q , c |= Equal1
iff the topmost 1store of c has a prefix of the form σ2 vγ2 vβ2 such that σ2 , γ2 , β2 ∈ Σ2 ∪ Q and v ∈ (Σ1 )p(n) .
p(n)That is, it has two equal 1-counters on the top. To define Equal1 , we will first define aformula ψ such that P2,Q , c |= ψ iff the topmost 1-store of c has prefix of the form σ2 vγ2 uβ2such that σ2 , γ2 , β2 ∈ Σ2 ∪ Q and v, u ∈ (Σ1 )p(n) but not necessarily v = u. This canp(n)be defined in a similar way as Counter1 . Assuming now that c satisfies ψ (i.e. thatthe topmost 1-store of c is σ2 vγ2 uβ2 as above), we now define the formula ψ 0 such that
P2,Q |= ψ 0 iff u = v. The formula is
!
p(n)

^
_ 
2i
2(p(n)+1)(EX)
σ1 ∧ (EX)σ1i=1

σ1 ∈Σ1

where (EX)i is simply a nesting of i EX operators. Notice that when a configuration
satisfies Σ1 , Σ2 , or Σ3 we may still continue unrolling. Notice also that we use 2i instead ofi because we have “intermediate” configurations (i.e. stacks whose topmost 1-store is of theform [markedi ...] or [unmarkedi ...]) that are needed for the purpose of checking.

18

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems
p(n)

p(n)

Similar to the definition of Equal1 , we can also define an EX formula Succ1
such
p(n)
that P2,Q , c |= Succ1
iff the topmost 1-store of c has prefix of the form σ2 vγ2 uγ2 suchthat σ2 , γ2 , β2 ∈ Σ2 ∪ Q, v, u ∈ (Σ1 )p(n) , and the number represented by v is a successor of
the number represented by v 0 (e.g. v = a1 a1 a1 b1 and v 0 = a1 a1 b1 a1 ).
p(n)We now define a formula Counter2 such that, for any reachable configuration c of P2,Qp(n)(from c0 ), we have P2,Q , c |= Counter2
iff the two following conditions are satisfied:(C1) the topmost 1-store of c has a prefix of the form σ3 vγ3 where σ3 , γ3 ∈ Σ3 and v is a(2, Q)-counter.
(C2) each 1-store in c, except for the topmost, has some symbol from P rime (but not
DP rime) as a topmost symbol.
It is easy to check that a reachable configuration c satisfying top1 (c) ∈ Σ3 must have a prefix
that is in the language top1 (c).L2 in its topmost 1-store. The second condition is introduced
due to the fact that HOBPA lack control states, but that we will have to remember thatexactly one symbol in Σ3 is seen when we try to pinpoint parts of the hypothetical 2-counterthat might be invalid. On the other hand, using EF logic, we must somehow use the EF
operator here as in the worst case we may have to pop1 exponentially many symbols tocheck the first condition. We start by defining a formula U nmarked checking the second
condition:!
3[
U nmarked :=Σi ∪ Q ∧ EX[P rime]AGP rime.
i=1

W
where EX[S](φ) abbreviates EX( a∈S a ∧φ) for any subset S of atomic propositions. It iseasy to check that U nmarked defines the desired formula owing to properties (P1) and (P2).
p(n)
We shall now define the formula Counter2
checking the first condition, assuming that thesecond condition is satisfied. This formula will be the formula Σ3 ∧EX[marked3 ]EX[Σ1 ](θ),
where θ is a conjunction of the following formulas:
Last1 , which we already defined. This is because we expect to see a 1-counter with value
exp1 (p(n)) − 1 on the top of the topmost 1-store.
V alidCounter2 , which we define as





p(n)
p(n)
p(n)
AG Counter1 ∧ Check2 → F irst1 ∧ BottomCounter1 ∨ Succ1.
This formula tries to make sure that the structure of the hypothetical 2-counter is valid.
Intuitively, the formula V alidCounter2 tries to guess two consecutive 1-counters inside
the hypothetical 2-counter that might not proceed in a successive fashion, unless it is
the bottomost 1-counter inside the hypothetical 2-counter which has to be the 1-counter
representing 0. To see this, first notice that we already forced the marking to be applied(i.e. we have operator EX[marked3 ] before θ). To this end, we first make sure that top2
has a prefix that is a 1-counter. The subformula Check2 ensures that the operator AG
does not take it to another 2-counter (i.e. passing a symbol from Σ3 ):Check2 := EX[Σ02 ∪ Q0 ](EF Σ003 ∧ ¬EF (Σ003 ∧ EXEF Σ003 ) ∧ ¬EF (Σ03 ∧ EF Σ003 )).
The formula simply says that precisely one 1-store below the topmost satisfies Σ003 andthis is above any 1-store satisfying Σ03 . Since we know that initially (i.e. in c) U nmarked
is satisfied, we can be sure that the 1-store satisfying Σ003 is the one which we applied themarking meaning that the application of AG operator has not passed any symbol from
Σ3 , i.e., we are still in the same hypothetical 2-counter. Here, BottomCounter1 is an EXformula which makes sure that the guessed 1-counter is the bottomost 1-counter in thisM. Hague and A. W. To

19hypothetical 2-counter. This can be defined without EF as we only need to look forwardp(n)at most 2p(n) + 2 steps using EX and so can be defined in the same way as Counter1 .
p(n)We now define the formula Equal2
such that, for a reachable configuration c, we havep(n)P2,Q , c |= Equal2
iff the condition (C2) above is satisfied and that(C1’) top2 has a prefix of the form σ3 vγ3 vβ3 , where σ3 , γ3 , β3 ∈ Σ3 and v a 2-counter.
To define this formula, we first define the formula 2Counter2 which expresses that top2 hasa prefix of the form σ3 vγ3 uβ3 , where v and u are (not necessarily the same) 2-counters.
p(n)This can be done in the same way as we defined Counter2 , i.e., we need to place anothermarking σ300 ∈ Σ003 immediately after the previous 2-counter. Assuming 2Counter2 is satisfied,p(n)to violate Equal2 , we will locate a position (i.e. 1-counter) inside v and show that thecorresponding position in u contains a different symbol. In order to pick a position, we will
p(n)
p(n)
use the technique of “marking” used for defining Counter2 . Therefore, Equal2
can bedefined asp(n)EX[marked3 ]EX[Σ1 ]EF (θ0 ∧ Rightposn ∧ Counter1p(n)∧ ¬Last1).

Here, Rightposn makes sure that we are in the right position:
Check2 ∧ EX[Σ02 ∪ Q0 ]AG(¬(Σ002 ∨ Q00 )).
This makes sure that we are still inside the current 2-counter v and that we did not marksymbols in Σ2 ∪ Q in the process (i.e. not replace them by symbols in Σ002 ∪ Q00 ). We shall
now mark the current top1 symbol and mark the corresponding position in u. Therefore, θ0is the following formulap(n)EX[{marked2 , markedQ}]EF (θ00 ∧ Rightposn0 ∧ Counter1p(n)∧ ¬Last1).

Here, Rightposn0 makes sure that we are in the right position, i.e., it’s a conjunction of thefollowing formulas:
That we are inside u (it is a modification of Check2 ):EF Σ003 ∧ ¬EF (Σ003 ∧ EXEF Σ003 )∧.
EX[Σ02 ∪ Q0 ]  EF (Σ03 ∧ EF Σ003 )∧¬EF (Σ03 ∧ EXEF (Σ03 ∧ EF Σ003 ))

The first three conjuncts ensure that we have passed the symbol γ3 ∈ Σ3 . The lastconjunct ensures that we have not passed the conjunct β ∈ Σ3 . The reasoning is similar
to how we define the formula Check2 .
That there is only one 1-store below the topmost 1-store satisfying Σ002 ∪ Q00 , i.e., theposition that we marked in θ0 :EX[Σ02 ∪ Q0 ](EF (Σ002 ∨ Q00 ) ∧ ¬EF ((Σ002 ∨ Q00 ) ∧ EXEF (Σ002 ∨ Q00 ))).
Now, the formula θ00 will mark the current position and check that the two marked positions
are the same and the corresponding content of the position (i.e. two symbols from Σ002 ∪ Q00 )are also the same:_EX[Σ002 ∪ Q00 ] Equal10 ∧(α00 ∧ EF α00 ) .
00
α00 ∈Σ00
2 ∪Q

20

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems
Here, the second conjunct tests that the contents are indeed the same. Here, Equal10 isp(n)an easy modification of Equal1
which tests that the two positions marked (i.e. they are
1-counters) are the same.
p(n)Likewise, we can define a formula Succ2 such that, for a reachable configuration c, wep(n)have P2,Q , c |= Succ2
iff the condition (C2) above is satisfied and that(C3’) top2 has a prefix of the form σ3 vγ3 uβ3 , where σ3 , γ3 , β3 ∈ Σ3 and v, u are two successive 2-counters.
Now, we are ready to show that the expression complexity of EF is 1-ExpSpace-hard.
Let us take a fixed exponential space bounded, say exp1 (p(n)), Turing machine T with states
Q. Our fixed 2-BPA is then P2,Q . Combining the technique that we use for establishing
lower bounds for data complexity of EF over HOPDS in the previous subsection and the
p(n)
p(n)
p(n)
p(n)
formulas Counteri , Lasti , F irsti , Equalithat we just defined, it is not hard to
reduce membership of T to model checking EF over P2,Q . There are three extra things that
we will have to ensure, which can be done easily:
The bottomost configuration guessed is an initial configuration. That is, it contains an
encoding of q0 w followed by exp1 (p(n)) − n blank symbols.
The topmost configuration is an accepting configuration, i.e., it has a final state.
In between two consecutive symbols from Σ3 in the initial guess, there is a state symbol,
i.e., symbol from Q.
All these can be defined easily in EF using the marking technique that we used to definep(n)Counter2 , i.e., we have to mark symbols from Σ3 .

Extensions to order-k BPA
We shall briefly sketch this extension to order-3 (this can be easily extended to the general case in the same manner). The guessing stage can be adapted easily to instead
write a sequence of potential (3, Q)-counters on the stack by performing only push1 operations as before. The checking stage is also similar. The idea is to create a “stair-ofstairs” structure for the purpose of checking. We shall elaborate more details on this.
We will now also use symbols from Σ4 , Σ04 := {a04 , b04 }, and Σ004 := {a004 , b004 }. When we
see symbols from Σ1 ∪ Σ2 , we have the same choices as in our previous construction.
On the other hand, when we see a symbol σΣ3 ∪ Σ4 ∪ Q, we can no longer perform(σ 0 , push2 , unmarkedi ) and (σ 00 , push2 , markedi ) operations, but instead we can use theoperations (σ 0 , push3 , unmarkedi ) and (σ 00 , push3 , markedi ) (where i is one of 3, 4, Q as before). In this way, we are building a 3-store whose 2-stores (except the topmost) displays
the projection of a prefix of the guessed configuration [w]3 onto Σ3 ∪ Σ4 ∪ Q as top1 symbols.
Note that we use Σ3 for displaying tape contents of the Turing tape, Q as the states of theTuring machine, and Σ4 as separators of two consecutive configurations. Also, note thateach 2-counter encoding the address of a cell position can be doubly exponentially large andare displayed inside each 2-store (in the same way as the previous construction).

B.3

Proof of Theorem 10

Theorem 10. For a fixed formula, model checking CTL over a given order-k HOPDS without
collapse is k-ExpTime-hard.
Given an alternating order-(k−1) pushdown automaton P augmented with an s(n)-spacebounded two-way work tape, we show that the membership problem can be polynomiallyM. Hague and A. W. To
reduced to the satisfaction of a fixed CTL formula ϕ by an order-k pushdown system PPw .
Here, we take s(n) to be a polynomial.
The reduction is similar to that used by Bozzelli for CTL model checking of pushdown
systems [4] and borrows further ideas from Engelfriet [13].
The idea of the reduction is as follows: an order-k stack is used to navigate a computation
tree of the order-(k − 1) alternating HOPDA in a standard way. To simulate the work tape,at each step, after simulating an operation on the order-(k − 1) stack, a sequence of s(n)work tape symbols (with the head position marked) are pushed on to the top order-1 stack.
After this is done, the system can either check that the guessed work tape is consistent withthe previous tape, or continue the execution. To continue the execution, an order-k push
operation saves the current state (for backtracking), then the work tape is erased. This
process repeats. When an accepting configuration is seen, or the children of the current
node have been fully explored, the automaton backtracks, and checks untested universal
branches. The automaton accepts when the empty stack is reached. That is, all paths havebeen explored, and found to be accepting.
The CTL formula asserts that a path encoding an accepting tree exists, and that after
guessing the work tape, the branches checking consistency all accept. The formula is
ϕ = E ((op ∧ AX(check → AF good)) U f in)where op indicates the current path is simulating a tree, and check indicates a consistency
checking branch. The proposition good indicates that the check has been passed, and f indenotes the (successful) completion of the run.
I Definition 17. Given a word w of length n and an alternating order-(k − 1) pushdown
automaton P augmented with an s(n)-space bounded two-way work tape, we define theorder-k pushdown system PPw . We assume without loss of generality that two rules can beapplied from each configuration, and which can be referred to as the first and second rules
respectively. We also assume the initial state is existential. Finally, let 2 denote an empty
work tape cell, and ⊥P denote the bottom of stack character for P.
We define PPw to have the following transitions. The set of states is defined implicitly.
The initial state is init. To initialise the automaton we have(init, ⊥, (pushf in ; pushk ; pushw ), (continue, 0)) where w describes the initial work tape.
That is, w = E(2, p0 )2s(n)−1 # ⊥P .
Note that the pushw erases f in from the copy of the stack created by pushk .
The main loop of the simulation is given by the continue states, which have the following rules. We store the current word position i on the stack (to aid backtracking) before
performing a pushk to continue the execution. The clear phase then removes the current
work tape from the stack, remembering the important details. We then simulate a movewhich may update the stack. The branch phase is where the automaton can either checkthe consistency of the guessed tape, or continue the execution.
((continue, i), done, pushdone , (back, i))((continue, i), x, (pushix ; pushk ; pop1 ), (clear, i, x)) for x ∈ {E, A1 , A2 }.
((clear, i, x), a, pop1 , (clear, i, x)) for all a ∈ ∆ and x ∈ {E, A1 , A2 }.
((clear, i, x)), (a, p), pop1 , (clear, i, x, a, p)) for all a, b ∈ ∆ and p ∈ P and x ∈ {E, A1 , A2 }.
((clear, i, x, a, p), b, pop1 , (clear, i, x, a, p)) for all a, b ∈ ∆ and p ∈ P and x ∈ {E, A1 , A2 }((clear, i, x, a, p), #, pop1 , (move, i, x, a, p)) for all a ∈ ∆ and p ∈ P and x ∈ {E, A1 , A2 }and p is not accepting or i 6= |w| + 1.
((clear, i, x, a, p), #, pop1 , (back, i)) for all a ∈ ∆ and p ∈ P and x ∈ {E, A1 , A2 } and p
is accepting and i = |w| + 1.

21

22

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems((move, i, x, a, p), γ, (o; pushyw ), (branch, r, i)) for all a ∈ ∆, p ∈ P , x ∈ {E, A1 , A2 },γ ∈ Σ. Furthermore when x = E, r is any rule applicable at p, a, γ, w(i); when x = A1 ,r is the first transition for p, a, γ, w(i); and when x = A2 , r is the second transition forp, a, γ, w(i). The operation o is the pushdown operation of r and y is E when r moves
to an existential state, and A1 when moving to a universal state. Finally, w is any work
tape configuration of length s(n) and with the read head containing state q reached byr. Note that there are an exponential number of w, but we can easily gain all w with alinear number of intermediate states and rules, each guessing the next character of w.
((branch, r, i), a, pusha , (continue, j)) where j = i if r is an ε-transition in the input, or
j = i + 1 otherwise; and ((branch, r, i), a, pusha , (check, r)) for all r and a.
The back phase implements the backtracking, and requires the following rules.
((back, i), a, popk , (back1 , i)).
((back1 , i), f in, pushf in , f in).
((back1 , i), j, pop1 , (back2 , j)).
((back2 , i), E, pushdone , (continue, i)).
((back2 , i), A1 , pushA2 , (continue, i)).
((back2 , i), A2 , pushdone , (continue, i)).
Finally, the check phase has a branch for all 0 ≤ j ≤ s(n) which ensures the jth positionin the work tape is consistent with the previous work tape, given the rule r has been executed.
If there is no previous configuration, the work tape is automatically good.
((check, r), x, pop1 , (check, r, j)) for all x ∈ {E, A1, A2} and 0 ≤ j ≤ s(n).
((check, r, j), a, (pop1 )j , (check1 , r, j)).
((check1 , r, j), a, pop2 , ((check2 , r, j, a)).
((check2 , r, j, a), f in, pushf in , good).
((check2 , r, j, a), x, (pop1 )j+1 , (check3 , r, j, a)) if a is not a pair (b, q), and also the rules((check3 , r, j, a), b, pushb , good) where b = a or b = (b0 , q) where r reads b0 at state q andwrites a to the tape.
((check2 , r, j, (a, q)), x, (pop1 )j , (checkL , r, j, (a, q))) if r moves left, q is moved to by r,0
and ((checkL , r, j, (a, q)), (b, q 0 ), pop1 , (checkL, r, j, (a, q))) where q is moved from by r and0, r, j, (a, q)), a, pusha , good).
b is read by r. Finally, we have the following rule ((checkL
j+1((check2 , r, j, (a, q)), x, (pop1 ) , (checkR , r, j, (a, q))) if r moves right, q is moved to by r,
0, r, j, (a, q))). Finally, we have additional rulesand ((checkR , r, j, (a, q)), a, pop1 , (checkR00((checkR , r, j, (a, q)), (b, q ), push(b,q0 ) , good) where b is read by r and q 0 is moved from byr.
The atomic proposition op is true during the init, continue, clear, move, branch and backphases. The proposition check is true during the check phase, good true at state good andf in at state f in.
I Property 1. A word w is accepted by P iff PPw satisfies the fixed formula ϕ. Furthermore,
PPw is polynomial in the size of w and P.
I Corollary 18. CTL model checking of order-k pushdown systems is k-ExpTime-hard, evenfor a fixed formula ϕ.
S
Proof. Take any language L in d>0 DTIME(expk (ds(n))) for some polynomial s(n). Thereexists a Turing machine M such that M accepts a word w iff w ∈ L. From Theorem 5 weknow that there is an order-(k − 1) alternating pushdown automaton PM with an s(n)-space
auxiliary work tape such that w ∈ L iff w is accepted by P. Then, by Property 1, we have,by a polynomial reduction, that w ∈ L iff PPw satisfies ϕ.
J

M. Hague and A. W. To

B.4

Proof of Theorem 11

Theorem 11. For a fixed order-k HOBPA without collapse, model checking CTL is kExpTime-hard.
We adapt the reduction for CTL to give a k-ExpTime expression complexity for CTL
over HOBPA.
I Definition 19. Given an alternating order-(k−1) pushdown automaton P augmented withan linear-space bounded two-way work tape, we define the order-k pushdown system PP .
We assume without loss of generality that two rules can be applied from each configuration,
and which can be referred to as the first and second rules respectively. We also assume theinitial state is existential. Since there is only one control state, we write (a, o) instead of(q, a, o, q) where o is a pushdown operation. Finally, let 2 denote an empty work tape cell,and ⊥P denote the bottom of stack character for P.
Note, the format of the tape simulation information on the stack is a string, for example,
E0101ab(c, p)d# to indicate an existential position, and word position 0101 with cell contentsab(c, p)d. The structure of the whole stack is an sequence of (k − 1) stacks. The top (k − 1)stack represents the current configuration being simulated. The next (k − 1) stack simply
contains, on its top character, a representation of the rule r used to reach the configuration.
The (k − 1) stack underneath is the previous configuration, and so on.
We define PP to have the following transitions. The set of states is defined implicitly.
To initialise the automaton we have the following rules. Since we cannot use a control state,these rules take care of adding work tape and simulation information to the stack in general.
We use the formula to assert a correct flow. For every character x, we also use x to indicatethat the character has been reached via a pop operation.
(⊥, (f in; pushk ; ⊥0 )) and (⊥0 , push#⊥P ).
(#, pushc# ), (c, pushc0 c ) where c, c0 ∈ ∆ ∪ (∆ × P ).
(c, pushic ), (i, pushi0 i ) where i, i0 ∈ {0, 1} and c ∈ ∆ ∪ (∆ × P ).
(i, pushxi ) where i ∈ {0, 1} and x ∈ {E, A1 , X}.
After writing the work tape we have E, A1 or X on the stack, we continue the execution
with a pushk or check the contents of the work tape. Alternatively, if we reach x forx ∈ {E, A1 , A2 } then we are either checking the tape or backtracking, hence we announce
which before continuing appropriately.
(x, (x; pushk ; continue)) where x ∈ {E, A1 } and (A1 , (A2 ; pushk ; continue)).
(x, push(x,check) ) where x ∈ {E, A1 , A2 , X}.
(x, pushcheck2 ) where x ∈ {E, A1 , A2 , X}.
(x, pushback ) where x ∈ E, A2 , X .
(back, popk ) and (y, pop1 ) for y ∈ {continue, (x, check), check2 }.
(x, pop1 ) for all x 6= #.
(#, pushmove ), (#, pushpop ).
(pop, popk ), (r, popk ) for all rules r.
(move, pop1 ).
To simulate a move we first announce on the stack which move will be executed. Then
we copy the stack to remember the move joining the configurations. Then we fire the ruleand continue the execution. Let op(r) be the stack operation of the rule r and top(r) be the
top of stack character after the rule has fired (which can be obtained from the rule alone),
if the rule is a push rule.

23

24

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems(c, push(c,r) ), ((c, r), (r; pushk ; (c, r)0 )).
((c, r)0 , (c; op(r); (top(r), done)), ((c, done), push#)c ) when op(r) is a push rule, and((c, r)0 , op(r)), (a, push#a ) when op(r) is a pop rule and a is a stack character from thesimulated HOPDA.
We define propositions to be true when forming part of the top of stack character. For
example x will be true when x, x or (x, y) are on the top of the stack. We also use op toindicate all states that are not check declarations.
The corresponding CTL formula is defined below.
I Definition 20. For any w, let n = |w|. We define
ϕw = E ((op ∧ AX(check → ϕgood )) U f in)where ϕgood is of the form
ϕgood = ϕf irst ∨ (ϕAE ∧ ϕf mt ∧ ϕi ∧ ϕr ∧ ϕtape )where each component formula is defined below. Let Bin(i, bm )(j) be the jth bit of thebinary encoding of i. To ease readability we define EAtN ext(ϕ, ϕ0 ) = E((¬ϕ)U (ϕ ∧ ϕ0 )).
That is, at the next time ϕ is true, ϕ0 is also true. We also define ChkN ext(ϕ) that looks
into the next work tape on a check branch and Rule(r) that is used to match the rule r
connecting the configurations. That is,
ChkN ext(ϕ) = EAtN ext #, EX pop ∧ EX 3 (check2 ∧ ϕ)
Rule(r) = EAtN ext (#, EX (pop ∧ EXr)) .
When there is just a single configuration on the stack, we use ϕf irst to ensure it is correct.
Note that, given a correct initialisation, ϕtape (defined below) ensures the tape format iscorrect in following configurations.

Vbm
j
b +1

 E ∧ j=1 EX 0 ∧ EX m (2, p0 )
Vs(n)
bm +j
ϕf irst =.
2∧
j=1 EX
bm +s(n)+1
bm +s(n)+4EX# ∧ EXf in
For the remaining positions ϕAE ensures the placement of E, A1 , A2 and X is correct.
Let ϕtox for x ∈ {E, A1 , A2 , X} denote the disjunction of all rules of leading to a state oftype x.
_
ϕAE =x ∧ EAtN ext #, EX pop ∧ EXϕtoxx∈{E,A1 ,A2 ,X}

The formula ϕf mt ensures the topk stack has yBin(i, bm )w# as the beginning of the first
two top1 stacks, where y ∈ {E, A1 , A2 } and w is a work tape of length s(n).
V
 V

W
s(n)
bm
j
bm +j
ϕ0f mt =j=1 EX (0 ∨ 1) ∧j=1 EXa,(p,a) (a ∨ (p, a))= ϕ0f mt ∧ ChkN ext(ϕ0f mt ) .

ϕf mt

The next formula ϕi ensures that the input position counter is consistent with the previous
counter. Note that this will ensure, when backtracking to a universal position, the second
branch will have the same counter as the first: both must be consistent with the ancestor’scounter.
^ϕi =Rule(r) ⇒ EXϕrir

M. Hague and A. W. To

25

Furthermore, if r is an ε-transition, we defineWnϕri =N um(j) ∧ ChkN ext(EXN um(j))
Vj=0
bm −1
j0
0
N um(j) =j 0 =0 EX Bin(j, bm )(j )otherwise
ϕri =

n 
_
N um(j)∧j=1

ChkN ext(EXN um(j − 1)).

The formula ϕr asserts that the applied rule r matches the claimed input positions. Letinp(r) denote the input character associated with a rule r.
WW
ϕr =r Rule(r) ⇒inp(r)=w(j) ChkN ext(EXN um(j)) .
Finally, ϕtape ensures that the tape contents have been updated accurately. We use, forshorthand, functions N extr (σ1 , σ2 , σ3 ) = d that specifies the contents of the current (jth)cell d with respect to the rule fired r and the contents of the previous configuration’s (j−1)th,
jth and (j + 1)th cells σ1 , σ2 and σ3 respectively. Let #l and #r denote, for the benefit of
N extr (σ1 , σ2 , σ3 ), the left and right boundaries of the tape respectively.
W
bm r
ϕtape =
ϕtaper Rule(r) ∧ EX
ϕrtape = ϕrlef t ∧ ϕrmiddle ∧ ϕrrightW
N extr (#l , σ1 , σ2 )∧ϕrlef t =σ1 ,σ2
ChkN ext(EXbm (σ2 ∧ EXσ2 ))Vs(n)−1 Wr
ϕr
ϕmiddle = j=1 j σ1 ,σ2 ,σ3 σ1 ,σ2 ,σ3EX N extr (σ1 , σ2 , σ3 )∧ϕrσ1 ,σ2 ,σ3 =ChkN ext(EX bm +j−1 (σ1 ∧ EXσ2 ∧ EX 2 σ3 ))WEX s(n) N extr (σ1 , σ2 , #r )∧r.
ϕright =σ1 ,σ2
ChkN ext(EX s(n)−1+bm (σ1 ∧ EXσ2 ))I Property 2. A word w is accepted by P iff PP satisfies the formula ϕw . Furthermore, PP
and ϕw are polynomial in the size of w and P.
I Corollary 21. CTL model checking of fixed order-k HOBPA is k-ExpTime-hard.
S
Proof. Take any language L in d>0 DTIME(expk (ds(n))) for some polynomial s(n). Thereexists a Turing machine M such that M accepts a word w iff w ∈ L. From Theorem 5 weknow that there is an order-(k − 1) alternating pushdown automaton PM with an s(n)-space
auxiliary work tape such that w ∈ L iff w is accepted by P. Then, by Property 2, we have,by a polynomial reduction, that w ∈ L iff PP satisfies ϕw .
J

C

Proof of Theorem 12

Theorem 12. For a fixed order-k HOBPA without collapse, model checking CTL+ is(k + 1)-ExpTime-hard.
We adapt the reduction for CTL to give an (n + 1)-EXPTIME expression complexity
for CTL+ over HOBPA. Will begin with an informal description of the proof for CTL* andexplain how to adapt it for CTL+.
The reduction we use to show CTL* is (k + 1)-ExpTime-hard over order-n pushdown
systems is similar to Bozzelli’s proof for the order-1 case. In fact, only a simple adjustment

26

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

to the HOPDS construction for the k-ExpTime-hard result of CTL has to be made. The
main technical steps of the proof are in the definition of the required CTL* formula, which
was already given by Bozzelli.
We reduce from an order-(k − 1) alternating HOPDA with an exponential space work
tape. The order-k PDS we construct manages the alternation in the same manner as the
reduction for CTL. The only difference is in the generation of work tapes. For the CTL
reduction we could simply output a polynomial number of tape symbols, and check forconsistency using only a polynomial number of states. However, the same strategy foran exponential space bounded tape would require an exponential number of states. The
trick is to output an arbitrary length tape, and use the power of CTL* to reject any tapeconfigurations that are not exponential.
In more detail, the HOPDS represents tape configurations as words of the form
binn (0)c0 binn (1)c1 · · · binn (2n − 1)c2n −1
where binn (i) is the n-digit binary representation of i with the least significant bit first. It
is beyond the power, however, of a polynomially sized HOPDS to output only sequencesthat count correctly from 0 to 2n − 1. Hence, the HOPDS generates, nondeterministically,a word of the form
n∗({0, 1} (∆ ∪ (∆ × Q))) .
One can check whether a configuration of this form is of the correct length as follows: first
assert that the first n-digit binary number is 0n . Then check that every pair bi ci bi+1 ci+1
has bi = bi+1 + 1. Finally, the last number must be all 1s.
The checking phase of the HOPDS now proceeds as follows. One branch simply pops
the configuration from the stack. This branch allows the CTL formula to check the lengthof the configuration.
The remaining branches remove the tape configuration from the stack, but nondeterministically mark one position with the proposition check1 (hence there are a number ofbranches for this step). Next popk s are performed to retrieve the previous work tape. Thenthe HOPDS does the same as before: pops the tape from the stack, nondeterministicallymarking a position with check2 . The CTL* formula can test consistency by checking whether
the two positions correspond to the same position in the work tape. If so, the markers check1
and check2 can be used to test the contents of the cell (and it’s neighbours) to ensure a valid
update has taken place.
To refine the construction to show CTL+ is (k + 1)-ExpTime-hard over order-k pushdown systems, the key restriction of CTL+ that has to be overcome is that the CTL*
formulas may contain nested path operators within a single path quantification. We overcome this adding extra marking information to the HOPDS. For example, we avoid the needto count (n + 2) steps ahead when comparing one cell position with the next by adding acheck2pre and a check2post marker into the HOPDS. That is, before marking the check2
position, the automaton will place a check2pre on the preceding tape character. Then, after
placing check2 , check2post will be placed on the next tape character.
In the case of HOBPA, it is not possible for the system to enforce the expected placing of
the propositions check2pre, check2 and check2post. That is, we can use the until operator
to ensure that the propositions appear in order ((¬check2 U check2pre)) but cannot enforce
that they appear in adjacent cells.
The trick is to encode cell numberings as sequences of tuples (b1j , b2j ) such that the encodednumbers differ by one. That is b2 + 1 = b1 . We can then ensure that the three propositions

M. Hague and A. W. To

are on adjacent cells in the same way we ensured check1 and check2 are on corresponding
cells. Recall that all binary numbers are encoded with the least significant digit first.
The cost of this encoding is that our work tape will contain 2n −2 cells, but this is clearly
not a problem for the complexity result.
I Definition 22. Given an alternating order-(k − 1) pushdown automaton P augmented
with an 2n -space bounded two-way work tape, we define the order-k pushdown system PP .
We assume without loss of generality that two rules can be applied from each configuration,
and which can be referred to as the first and second rules respectively. We also assume theinitial state is existential. Since there is only one control state, we write (a, o) instead of(q, a, o, q) where o is a pushdown operation. Finally, let 2 denote an empty work tape cell,and ⊥P denote the bottom of stack character for P.
Note, the format of the simulation information on the stack is, for example,
E~0~1~0~1(0, 0)(0, 1)(0, 0)a(0, 1)(0, 1)(0, 0)b . . . #to indicate an existential position, and word position ~0~1~0~1 with cell contents ab . . ..
We define PP to have the following transitions. The set of states is defined implicitly.
The initial state is init. To initialise the automaton we have the following rules. Since
we cannot use a control state, these rules take care of adding work tape and simulation
information to the stack in general. We use the formula to assert a correct flow.
(⊥, (f in; pushk ; ⊥0 )) and (⊥0 , push#)⊥P ).
2(#, pushc# ), (c, pushic ), where i ∈ {0, 1} and c ∈ ∆ ∪ (∆ × P ).
22
2(i, pushi0 i ) where i ∈ {0, 1} and i0 ∈ {0, 1} ∪ 0̂, 1̂ .

2(i, pushci ) where i ∈ 0̂, 1̂ and c ∈ ∆ ∪ (∆ × P ).
(c, pushic ), (i, pushi0 i ) where i, i0 ∈ ~0, ~1 and c ∈ ∆ ∪ (∆ × P ).
(i, pushxi ) where i ∈ ~0, ~1 and x ∈ {E, A1 , X}.
After writing the work tape we have E, A1 or X on the stack, we continue the execution
with a pushk or check the contents of the work tape. Alternatively, if we reach x forx ∈ {E, A1 , A2 } then we are either checking the tape or backtracking, hence announce
which before continuing appropriately.
(x, (x; pushk ; continue)) where x ∈ {E, A1 , X} and (A1 , (A2 ; pushk ; continue)).
(x, push(x,check) ) for x ∈ E, A1 , A2 , X, E, A1 , A2 .
(x, pushback ) for x ∈ {E, A2 , X}.
((x, check), push(x,checkf mt )), ((x, check), pushcheckcells ) for x ∈ {E, A1 , A2 , X}.
(y, pop1 ) for y ∈ {continue, (x, checkf mt ), checkcells }.
(back, popk ).
(x, pop1 ) for all x 6= #.
(#, pushmove ), (#, pushpop ).
(pop, popk ) and (r, popk ) for all rules r.
(move, pop1 ).
To simulate a move we first announce on the stack which move will be executed. Then we
copy the stack to remember the move joining the configurations. Then we fire the rule andcontinue the execution. Let op(r) be the stack operation of the rule r and top(r) be the topof stack character after the rule has fired (which can be obtained from the rule alone), if therule is a push rule.
(c, push(c,r) ), ((c, r), (r; pushk ; (c, r)0 )).
((c, r)0 , (c; op(r); (top(r), done)), ((c, done), push#)c ) when op(r) is a push rule, and

27

28

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems((c, r)0 , op(r)), (a, push#a ) when op(r) is a pop rule and a is a stack character from thesimulated HOPDA.
If we announced that we intend the perform a check of the tape contents, then we must
mark positions in the tape with check1 , check2 , check2pre and check2post. Hence, these
options must be available when popping down the tape.
(x, push(x,c) ) for x ∈ 0̂, 1̂ and c ∈ {check1 , check2 , check2pre, check2post}.
((x, c), pop1 ) for i ∈ {1, 2}, c ∈ {check1 , check2 , check2pre, check2post} and x ∈ 0̂, 1̂ .
We define propositions to be true when forming part of the top of stack character. For
example xwill be true when x, x or (x, y) are on the top of the stack. We also define i1 andi2 for i ∈ 0, 1, 0̂, 1̂ to allow us to identify the components of a tuple (i1 , i2 ).
The corresponding CTL+ formula is defined below. Recall bm is the number of digits
required to encode the length of w in binary.
I Definition 23. For any w, let n = |w|. We define
ϕw = E ((op ∧ AX(check → ϕgood )) U f in)where
ϕgood = ϕf irst ∨ (ϕf mt ∧ ϕcells ) .
When there is just a single configuration on the stack, we use ϕf irst to ensure it is correct.
Let EAtN ext(ϕ, ϕ0 ) = E(¬ϕU ϕ ∧ ϕ0 ). Note that the formula is written as if there is asingle path. This is not the case because the automaton may choose to mark a cell position.
However, due to the strict formatting required by the formula, these paths will fail. The
accept either 2 or characters
path that does not mark any cells should accept. Let ϕcell2that are not part of the tape (i.e. the cell numberings).
Vb m
E ∧ j=1
EX j~0 ∧AX checklen ⇒  EX bm +n+1 (2 ∧ EXE(ϕcells¬2 U #))∧  ∧ϕf irst =
ϕ0f mt
2
EAtN ext(#, EX f in)










where ϕ0f mt is defined below, and asserts the tape is of the correct format.
We now define ϕf mt which checks that the format of the tape is correct, that the correct
rule has been fired, &c., but does not check the cell contents. Let EXϕj ϕ0 abbreviate EX(ϕ∧EX(ϕ ∧ . . . EX(ϕ ∧ ϕ0 ))) and ¬c abbreviate the negation of any check propositions. Finally,
we define for convenience,
ChkN extF mt(ϕ) = EAtN ext(#, EX(pop ∧ EX 4 (checkf mt ∧ ϕ)))M. Hague and A. W. To

29

and the required formula is
ϕf mt = AX checkf mt ⇒ ϕ0f mt ∧ ChkN extF mt(ϕ0f mt ) ∧ ϕi ∧ ϕr ∧ ϕAE
ϕ0f mtlen= ϕif mt ∧ ϕtape
f mt ∧ ϕf mt

ϕif mt

=

ϕtape
f mt




bm
= EX¬cE b ⇒ ϕnum
f mt U #Vnj=
j=1 EX¬c (0 ∨ 1)

ϕlen
f mt



Vn−1
1
(b ∧ f ) → EX¬c(0, 1) ∧ j=2 (EX)j¬c (0, 0) ∧


 

 (b ∧ l) → EX 1 (1, 0) ∧ Vn−1 EX j (1, 1) ∧
¬c
¬c


j=3





(b ∧ ¬f ) →= EX bm EG 




j
n+2


 
EX
(0
∧
EX
1
)∧
l
l
¬c
 
  V2 Wn−1 V ¬c
i
n+2


 

 i>j EX¬c
(1
∧
EX
0
)∧
l
l
¬c
l=1
j
V
i
n+2
i<j EX¬c (1c ⇐⇒ EX¬c 1l )

ϕnum
f mt

Vbm

j ~
~
j=1 EX¬c (0 ∨ 1) 

and ϕAE ensures the placement of E, A1 , A2 and X is correct. Let ϕtox for x ∈ {E, A1 , A2 , X}
denote the disjunction of all rules of leading to a state of type x.
_

ϕAE =
x ∧ EAtN ext #, EX pop ∧ EXϕtoxx∈{E,A1 ,A2 ,X}and ϕi checks that the word positions are updated correctly.
Vr
ϕi =r Rule(r) ⇒ EXϕiN um(j)=Vbm

j 0 =0 EX

j0Bin(j, bm )(j 0 )and, if r is an ε-transition, then
ϕri =

n
_

N um(j) ∧ ChkN extF mt(EXN um(j))

j=0

and otherwisen_N um(j) ∧ ChkN extF mt(EXN um(j − 1))

j=1

The next formula ϕr ensures that the fired rule is applicable at the current word position.
Let inp(r) denote the input character associated with a rule r.
WW
ϕr =r Rule(r) ⇒inp(r)=w(j) ChkN extF mt(EXN um(j)) .
Finally ϕcells takes advantage of the fact that there is no branching while popping binary
blocks to avoid nesting temporal operators.
ϕcellsϕ0cells==

AX(checkcells → ϕ0cells )EAtN ext(#, EX 3 f in) ∨ AG((check1 ∧ b) → E(θ1 ∧ θ2 ))where θ1 asserts that the checks are placed correctly, and θ2 tests the consistency of thetape. As well as asserting that the propositions are in the right position, θ1 must also assert

30

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

that there is only one copy of each check proposition. We require check2pre and check2post
to hold at the beginning of the binary blocks.
pos
one
one
pos
∧ θpre∧ θ2one ∧ θpost= θpre∧ θ2pos ∧ θpost

θ1
θ2pos

=

pos
θpre

=

pos
θpost

=

one
θpre
θ2one
one
θpost

=
=
=


j
j
EX¬c
12 ⇒ F (check2 ∧ EX¬c
12 )∧
j
j
j=0
EX¬c
02 ⇒ F (check2 ∧ EX¬c
02 )
 

j
j
Vn−1
F (check2pre ∧ EX¬c 12 ) ⇒ F (check2 ∧ EX¬c11 ) ∧jj
j=0
F (check2pre ∧ EX¬c02 ) ⇒ F (check2 ∧ EX¬c01 ) 
jj
Vn−1
F (check2 ∧ EX¬c 12 ) ⇒ F (check2post ∧ EX¬c11 ) ∧jj
j=0
F (check2 ∧ EX¬c02 ) ⇒ F (check2post ∧ EX¬c
01 )

Vj=0
j
j
¬
F
(check2pre
∧
EX
0
)
∧
F
(check2pre
∧
EX
1
¬c
¬c 11 )

Vn−1
j=0
j
j
¬ F (check2 ∧ EX¬c01 ) ∧ F (check2 ∧ EX¬c
11 )

Vn−1
j=0
j
j
n−1 ¬ F (check2post ∧ EX¬c 01 ) ∧ F (check2post ∧ EX¬c 11 )Vn−1

To define θ2 , we use, for shorthand, functions N extr (σ1 , σ2 , σ3 ) = d that specifies thecontents of the current (jth) cell d with respect to the rule fired r and the contents of theprevious configuration’s (j − 1)th, jth and (j + 1)th cells σ1 , σ2 and σ3 respectively. Let #l
and #r denote, for the benefit of N extr (σ1 , σ2 , σ3 ), the left and right boundaries of the taperespectively.
_θ2 =Rule(#, r) ∧ (f → θfr ) ∧ ((¬f ∧ ¬l) → θir ) ∧ (l → θlr )
r

where
θfr

θir

θlr

=

=

=



W
σ1 ,σ2W

F (check2 ∧ EX n σ1 ) ∧F (check2post ∧ EX n σ2 )→ N extr (#l , σ1 , σ2 )F (check2pre ∧ EX n σ1 ) ∧ F (check2 ∧ EX n σ2 ) ∧ → N extr (σ1 , σ2 , σ3 )σ1 ,σ2 ,σ3nF (check2post ∧ EX σ3 )W
σ1 ,σ2F (check2pre ∧ EX n σ1 ) ∧F (check2 ∧ EX n σ2 )→ N extr (σ1 , σ2 , #r ) .

I Property 3. A word w is accepted by P iff PP satisfies the formula ϕw . Furthermore, PP
and ϕw are polynomial in the size of w and P.
I Corollary 24. CTL model checking of fixed order-k HOBPA is (k + 1)-ExpTime-hard.
S
Proof. Take any language L in d>0 DTIME(expk+1 (ds(n))) for some polynomial s(n).
There exists a Turing machine M such that M accepts a word w iff w ∈ L. From Theorem 5
we know that there is an order-(k − 1) alternating pushdown automaton PM with an 2n space auxiliary work tape such that w ∈ L iff w is accepted by P. Then, by Property 3, wehave, by a polynomial reduction, that w ∈ L iff PP satisfies ϕw .
J

D

Proofs For Linear Time

D.1

Proof of Theorem 13

Theorem 13. Model checking µLTL against order-k CPDSs is in k-ExpTime for a non-fixed
formula, and (k − 1)-ExpTime for a fixed formula.

M. Hague and A. W. To

It is well known that any formula of µLTL has a Büchi automaton representation. We
form the product of the CPDS and the Büchi automaton corresponding to the negationof the µLTL formula ϕ. This gives us a Büchi CPDS; that is, a CPDS with a set F of
accepting control states. Thus, model checking reduces to the non-emptiness problem for
Büchi CPDSs.
The non-emptiness problem for Büchi CPDSs is a special case of determining the winner
in a parity game played over a CPDS. In particular, it is a single-player game with a fixed
number (two) of colours. It is known that an order-k game can be reduced to an order(k − 1) game with an exponential blow-up [17]. This leads to a recursive algorithm resulting
in a finite-state parity game of k-exponential size, and since known finite-state algorithms
are polynomial in the number of states (and exponential in the number of colours), thealgorithm runs in k-ExpTime.
We demonstrate, in this simple case, the single-player order-k game can be reduced toa two-player order-(k − 1) game with only a polynomial blow-up. This order-(k − 1) gameis then solved as above, giving, an overall algorithm in (k − 1)-ExpTime in the size of the
Büchi CPDS. That is, (k − 1)-ExpTime for a fixed formula, and k-ExpTime for a non-fixed
formula.
We begin by recalling some definitions.
I Definition 25. Let P = (P, R, Σ, p0 , ⊥) be an order-k CPDS. Then G = (P, PE , PA , Ω) isan order-k CPDS parity game, where PE ] PA = P is a partitioning of the control statesand Ω : P → Col is a function assigning to each control state a colour in the set Col ⊂ N ofcolours.
A play Λ of a parity game between two players, Éloïse and Abelard, proceeds as follows.
Play begins with the initial configuration hp0 , [⊥]k i. If the control state of the current
configuration is is PE , then Éloïse chooses an applicable rule in R. Otherwise Abelardchooses a rule. If a player cannot move, they lose the game. The cycle repeats until a player
loses, or, in the case of an infinite play, the winner is determined by the colouring functionΩ. If the minimal colour occurring infinitely often is even, Éloïse wins the game. Otherwise
Abelard wins.
An important part of the reduction is the notion of collapse rank-aware.
I Definition 26 ([17]). Consider a partial play Λ in G ending in a configuration hp, γisuch that top1 (γ) has an k-link. Hence there is in Λ at least one configuration of the form
hp0 , collapse(γ)i for some p0 ∈ P . Then the closest to hp, γi is called the collapse ancestor of
hp, γi. The collapse rank of hp, γi is the minimal colour of a state occurring in Λ between thecollapse ancestor of hp, γi and hp, γi. Note that these notions are not defined if top1 (γ) has aj-link for some j < k: indeed it may happen that no configuration of the form hp, collapse(γ)i
was visited in Λ, and therefore the collapse ancestor notion can not be adapted.
I Definition 27 ([17]). An k-CPDS equipped with a colouring function is collapse rankaware iff there exists a function ColRnk : Σ → N such that, when defined, the collapse rankof every configuration hp, γi is equal to ColRnk(top1 (γ)). On other words, the collapse rank
is stored in the top1 -element of the stack.
Beginning with a Büchi CPDS, we must first make the CPDS collapse rank-aware. Thiscan be done using the following known results. Note that, since both the size of Col and k
are fixed, the transformation to a collapse rank-aware CPDS costs only a constant blow up.
I Lemma 28 ([17], Lemma 14, Remark 6.6). For any order-k CPDS P and parity game G
played over it, one can construct a collapse rank-aware order-k CPDS P 0 and order-k parity

31

32

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems
game G 0 such that Éloïse wins in G iff she wins in G 0 . Moreover, P 0 has O(|P ||Col|O(k) )control states and a stack alphabet of size O(|Σ||Col|O(k) ).
We are now ready to give the main reduction.
I Lemma 29. Given an order-k Büchi CPDS P, one can construct an order-(k − 1) CPDS
parity game G of size polynomial in the size of P such that P has an accepting run iff Éloïse
wins the game G.
Proof. We will describe G somewhat informally. The formal definition should be clear fromthe description. Control states of the game are of the form (p, pr , f ) for control states p andpr and the boolean flag f . We also allow pr = null. Intuitively, p is the current control
state of the configuration being simulated, pr is a promise to reach the control state pr whena popk , and f is an obligation to visit a final state before the popk . Similarly, the stackcharacters are either simply characters a, or, when simulating a character with a k-link, ofthe form (a, pr , f ), which play the same role as (p, pr , f ) does, but in the case of a collapse
over a k-link.
We describe how each rule application is simulated. Except when stated, Éloïse makes
all moves. Consider the rule (p, a, o, p0 ). In cases:
When o is a pushdown command that is not pushk , popk , pushka , or collapse when the
top1 character contains a k-link, the simulation is direct: o is simply applied and wereach the control state (p0 , pr , f 0 ) where f 0 is true iff f is true and p was not final.
When o is popk , play proceeds to a winning (sink) state for Éloïse if p0 = pr and f isfalse. Otherwise we reach a winning state for Abelard. The stack is not changed.
When o is collapse and the top1 character is (p, pr , f ), play proceeds to a winning (sink)state for Éloïse if p0 = pr and ColRnk(p, pr , f ) indicates a final state has been seen if f
is true. Otherwise we reach a winning state for Abelard. The stack is not changed.
When o is pushk , Éloïse declares a pair p0r and f 0 , indicating that, when the order-(k − 1)stack to be created is finally popped (if it is popped), then play will reach the state p0r ,and f 0 indicates whether a final state will have been seen on the way. Abelard can accept
the declaration and move play to (p0r , pr , f 00 ) without changing the stack, where f 00 istrue only if f is true and f 0 is not. Alternatively, Abelard may question the declarationand move play to (p0 , p0r , f 0 ) (without changing the stack).
When o is pushka we proceed as follows. We apply push1(a,pr ,f ) and move to (p0 , pr , f ).

The idea is that Éloïse’s commitments are saved to the stack in place of the k-link. If
following the collapse link is simulated, it must be in line with her previous declarations.
The final states are all control states where the first component p is final in the original
game. It is also the case that, when Abelard accepts a declaration by Éloïse that she canpass through a final state, we ensure that, in the simulation, an intermediate final state ispassed through. The initial state is (p, null, f alse) and stack bottom is ⊥.
Observe that, since there are no order-k stack operations in the simulation, the resulting
game is order-(k − 1).
To see why the simulation is correct, first consider an accepting run of the Büchi CPDS.
At each pushk , then either the current stack contents appear again on the run, in whichcase Éloïse simply declares the control state at this return, and whether a final state was
encountered en-route. Otherwise, she declares null and play proceeds to simulate the pushk .
Since the stack contents below the new top stack are never encountered again, they can besafely forgotten.
In the other direction, take a winning strategy for Éloïse. This strategy can be linearised,
constructing a run as follows: at each pushk , play has two branches. On the first, Abelard

M. Hague and A. W. To

33

questions Éloïse’s declaration, on the second, he accepts it. We recursively compute the runfrom the first branch and append to it the run from the second branch. This leads to an
infinite run with a infinite number of final states seen.
J

D.2

Proof of Theorem 15

Theorem 15. Model checking LTL(F, X) and LTL(U) against a fixed HOBPA without
collapse is k-ExpTime-hard.
We give proofs for the two logics in turn.

D.2.1

Lower Bound for LTL(F, X)

Given a fixed k-EXPTIME complete language L, Theorem 5 implies that there exists a fixedorder-k pushdown automaton P = (P, R, Σ, Γ ∪ {ε} , ∆, p0 , ⊥, F) augmented with an s(n)space bounded two-way work tape that accepts precisely the language L from hp0 , [⊥]k i. We
now construct an order-k BPA P 0 = (R0 , Σ, c00 ) and later show that there is a reduction of
the membership problem for L(P) to LTL model checking over P 0 , which shall imply that
expression complexity of order-k BPA is k-ExpTime-hard.
Let ∆0 = ∆ × {h, h̄} (h stands whether head is in this position or not). For an alphabetΩ, we let Ω? = Ω ∪ {?} assuming that ? ∈/ Ω. Similarly, we let Ω# be Ω ∪ {#} assumingthat # ∈/ Ω. Let W = R ∪ {sink}. Let Σ0 = (P? × W? × Σ) ∪ Σ ∪ (Σ × ∆0 ). The initialconfiguration c00 is h[(p0 , ?, ⊥)]k i. We now add the following rules to R0 :1. for each p ∈ P , a ∈ Σ, and r ∈ R where r is of the form ((p, ∗, a, ∗), o, ∗)1 , add((p, ?, a), push(p, r, a)).
and add((p, r, a), fa (o)).
where fa : Ok → Ok is defined as fa (o0 ) = o0 , if o0 ∈ O1 or of the form popj , andfa (o0 ) = (pusha ; pushj ; pusha ), if o0 = pushj for some j > 1.
2. for each a ∈ Σ and x ∈ ∆0 , add (a, push((a, x))).
3. for each x, y ∈ ∆0 and a ∈ Σ, add ((a, x), push((a, y))).
4. for each x ∈ ∆0 and p ∈ P , add ((a, x), push((p, ?, a))).
5. we add “sink” transitions: ((p, ?, a), push(p, sink, a)) and ((p, sink, a), push(p, sink, a))for any p ∈ F and a ∈ Σ.
Intuitively, each run of P 0 will have valuations of the form[(P × {?} × Σ) · (P × R × Σ) · Σ · (Σ × ∆0 )+ ]∗ · (F × {sink} × Σ)∗(∗)

or of the form[(P × {?} × Σ) · (P × R × Σ) · Σ · (Σ × ∆0 )+ ]ω .
We will now enforce the correct form via LTL formulas.
1Here, we use the wildcard ∗ to match a symbol or a tuple of symbols.

(∗∗)

34

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems
Given a word w = α1 . . . αn ∈ Γ∗ , we now construct an LTL formula ϕw using only F
and X temporal operators such that w ∈ L(P) iff P 0 , c00 6|= ¬φw . We first define a formulaψ that makes sure that precisely the word w is consumed during a guessed run:
ψ = ψ1 ∧ ψ2 ∧ ψ3 .
Let V be precisely the subset of P × R × Σ, where the rule component is of the following
form ((∗, α, ∗, ∗), ∗, ∗), for some α ∈ Γ; in other words, these are rules which “consume” aninput letter. The formula ψ1 states that at least n letters are consumed in the run; let
ψ10
ψ1i+1
ψ1

:= T rue:= XF (V ∧ ψ1i ):= ψ1n .

The formula ψ2 states that at most n letters are consumed in the run:
ψ2 := ¬ψ1n+1 .
To define ψ3 , let Vα be subset of V where the rule component is the form ((∗, α, ∗, ∗), ∗, ∗).
The formula ψ3 states that the ith letter consumed in the run is wi :
ψ30
ψ3i+1
ψ3

:= T rue:= XF (Vαn−i+1 ∧ ψ3i ):= ψ3n .

We now ensure that after each occurrence of (P × R × Σ) in the run (as in (*) and (**)),
we see precisely a stack symbol in Σ, followed by precisely s(n) symbols from Σ × ∆0 , which
are in turn followed by a symbol (p, ?, a) of the “right” form. Notice that this would meanthat we may partition each run as a contiguous sequence of blocks of size m := 3 + s(n)according to (*) and (**). More formally, define θ as follows:_θ :=G((p, r, a) → P × {?} × Σ.
(p,r,a)∈P ×R×ΣIf r is not of the form ((p, ∗, a, ∗), ∗, ∗), then we define θ(p,r,a) = F alse. Otherwise, lettingr = ((p, ∗, a, ∗), o, (∗, ∗, p0 )), we define θ(p,r,a) as follows:


s(n)
^
θ(p,r,a) := (p, r, a) ∧ 
X i+1 Σ × ∆0  ∧ X s(n)+2 (p0 , ?, a).
i=1

Each block of size s(n) (note: Σ is always followed by such a block) encoding the tapecontent needs to have exactly one head:



s(n)
_
^
Headi ∧Onehead := G Σ →¬Headj  ,i=1

1≤j≤s(n),j6=iwhere Headj := X j Σ × (∆ × {h}). Furthermore, two consecutive blocks encoding tapecontents, each of size s(n), must follow in the correct way:
T apef ollow :=^(p,r,a)∈P ×R×Σs(n)G((p, r, a) → XX(^

i=1

F ollowi,r )).

M. Hague and A. W. To

35

Here, F ollowi,r means that the ith cell of the subsequent tape content follows from theith cell of the current tape content using rule r. This formula can be easily defined bynoticing that the ith cell of the subsequent tape content can be uniquely defined from
cells i − 1, i, i + 1 of the current tape content and rule r. More formally, suppose thatr = ((∗, ∗, ∗, x), ∗, (y, d, ∗)). We define the formula for the case when d = l and 1 < i < s(n)(the remaining cases being similar). In this case, the formula F ollowi,r can be defined as aconjunction of four formulas:First formula assumes that head is not in cells i − 1, i, i + 1:^


X i−1 (x0 , h̄) ∧ X i (y 0 , h̄) ∧ X i+1 (z 0 , h̄) → X i+m (y 0 , h̄).

x0 ,y 0 ,z 0 ∈∆in which case the ith cell of the subsequent tape content is the same as the ith content
of the current tape content.
Second formula assumes that head is in cell i − 1. This case can be defined in the same
way as the previous case (ith cell remains the same).
Third formula assumes that head is in cell i:
X i (x, h) → X i+m (y, h̄) ∧^X i (z, h) → F alse .

z∈∆\{x}This formula forces that the tape symbol read by the head is x, in which case the ith
symbol of the subsequent block becomes (y, h̄), i.e., x is rewritten to y and the head is
no longer in the ith cell.
Fourth formula assumes that the head is in cell i + 1:^
X i (z, h̄) ∧ X i+1 (x, h) → X i+m (z, h).

z∈∆That is, the head moves from i + 1st cell to ith cell.
The first tape content needs to be initialized to (⊥, h)(⊥, h̄)s(n)−1 , i.e., all blank symbols
and the head on the leftmost cell:s(n)−1

T apeinit := X 3 (⊥, h) ∧^X 2+i (⊥, h̄).

i=2Finally, we need to define the formula Sink stating that the run needs to eventually end up
in a “sink” state;
Sink := F (P × {sink} × Σ).
The formula ϕw can now be defined asϕw := ψ ∧ θ ∧ Onehead ∧ T apef ollow ∧ T apeinit ∧ Sink.
It is easy to see that the formula ϕw ensures the existence of a correct run of P on input w.
That is, we have P 0 , c00 6|= ϕw iff w ∈ L(P). This gives us the following theorem.
I Theorem 30. The expression complexity of LTL(F,X) over order-k BPA is k-ExpTimehard

36

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

D.2.2

Lower Bound for LTL(U)As in the previous subsection, we shall give a sketch on how to show the same expression
complexity for the fragment LTL(U). The basic idea is quite simple: weakly simulate X
operators with U operators, while making sure (in the system) that each position in eachrun alternately satisfy/unsatisfy some new atomic proposition p0 . We may start with theorder-k BPA P 0 that we defined in the previous subsection and replace rule (3) above by
the following rule (3’): for x, y ∈ ∆0 and a ∈ Σ, add the rules ((a, x), push(a, !)) and((a, !), push(a, y)) to R0 .
We shall now show how to modify some of these subformulas that we previously defined(the idea works in general). We can redefine ψ1i+1 as (¬VU (VU ψ1i )); the reason we do thisbeing that V cannot hold true in two consecutive points in each run of P 0 . Let us now
consider how to modify θ(p,r,a) . Notice that due to new rule (3’), Σ × ∆0 and Σ × {!} must
alternate. This allows us to replace nestings of X operators by nestings of U operators, e.g.,
X 2 Σ × ∆0 becomes((p, r, a)U (Σ × ∆0 U (Σ × {!}U Σ × ∆0 ))).
In fact, it is easy to check that all uses of X operators can be replaced by U in this way.
We therefore have the following theorem.
I Theorem 31. The expression complexity of LTL(U) over order-k BPA is k-ExpTime-hard.

E

MSO over Collapsible HOBPA

A order-k collapsible HOBPA defines an MSO structure (CkΣ , R, (a)a∈Σ ), where CkΣ is theset of all order-k stores with links, R(c1 , c2 ) holds if there is a transition from configuration
c1 to c2 and a(c) holds for a ∈ Σ if top1 (c) = a.
We show that MSO over this structure is undecidable. We give an order-2 collapsible
HOBPA P such that the infinite half-grid is MSO-interpretable in the configuration graphof P.
Theorem 1. There exists a fixed collapsible order-2 BPA which generates a graph with anundecidable MSO theory.
Proof. Let P be the order-2 collapsible HOBPA with the following commands(⊥, pushx⊥ )(x, (x, push2 , x0 ))(a, (a, push2 , b)) (a, pushcol )(b, pusha2 b )(c, pushcol )(c, pushpop )(pop, pushε )(col, collapse)(x0 , pusha2 x0 )(a, pushpop )(a, pushc )The configuration graph is shown in Figure 3. Note that transitions to · · · may represent
more than one transition.
An MSO interpretation consists of a formula defining which nodes appear in the interpretation, and formulas defining the predicates of the interpretation. We will define an MSO
interpretation that restricts the graph to only the configurations shown in Figure 3 (except
the pop and x configurations at the bottom of each hanging branch). We will then define
two MSO relations A(x, y) and B(x, y) denoting an A- or B-edge from node x to node y.

M. Hague and A. W. To

•

37

A

•

A

B

•

A

B
•

A

•

A

B
•

A

B

B
•

A

B
•

A

• ···

• ···
B

•

A

B

• ···
B

•

A

• ···
B
• ···

Figure 2 The infinite half-grid.

With the given domain restriction and interpretation of A and B, we obtain the infinite
half-grid in Figure 2. Since decidability is preserved by MSO interpretation, we obtain theundecidability of MSO over collapsible HOBPA.
The domain restriction allows any node appearing on a path satisfying the following
regular expression rdom . The paths are paths of stack symbols. A path in the graph satisfies
this expression if the projection to its top1 elements does. This expression can be translated
to MSO using standard techniques. We define
rdom = ⊥ x x0 (a b)∗ c (col ∪ ((pop a)∗ col)) .
Similarly, we define A and B in terms of regular expressions. For X ∈ {A, B}, X(x, y) holds
if there is a path (which may take some edges backwards) from x to y satisfying the regularexpression rX . We write ab to mean that the transition from the node satisfying a to thenode satisfying b is a backwards edge. We define
rA
1
rA
2
rA

1
2
= rA
∩ rA
= (a pop)∗ c a b a c (pop a)∗= (c ∪ a) col ((⊥ x x0 ) ∪ (a b)) a col (c ∪ a) .

1
In this definition rA
takes configurations with top1 character a or c in a hanging branch to2
any configuration with top1 character a or c in the next branch along. The expression rA
uses the collapse operations to make sure that the only available node in the next hanging
branch is at the same depth. Finally,rB = (c ∪ a) pop a[x ⊥]

col(2,1) x ⊥ [⊥][x′ ⊥] [x ⊥]Figure 3 The configuration graph of P.

[⊥]





 (2,2)x ⊥ a(2,1) x ⊥ [⊥]col  (2,1)ax ⊥ [⊥][x ⊥] a(2,1) x ⊥ [⊥]pop(2,2) x ⊥ (2,2)x ⊥ a(2,1) x ⊥ [⊥]a[x ⊥] [⊥]

 (2,1) (2,2)
ca
x ⊥ a(2,1) x ⊥ [⊥] (2,1) (2,2)
aa
x ⊥ a(2,1) x ⊥ [⊥] (2,1) (2,2)


pop
a
x ⊥ a(2,1) x ⊥ [⊥]··· (2,1) (2,2)


col
a
x ⊥ a(2,1) x ⊥ [⊥] (2,2)bx ⊥ a(2,1) x ⊥ [⊥]
pop(2,1) x ⊥ [⊥] (2,1)cx ⊥ [⊥]

 (2,1)ax ⊥ [⊥]

col(2,3) x ⊥  (2,1) (2,2)
aa
x ⊥ a(2,1) x ⊥ [⊥]··· (2,2) (2,3)



col
a
x ⊥ a(2,1) a(2,2) x ⊥ a(2,1) x ⊥ [⊥]··· (2,1) (2,2) (2,3)



col
a
a
x ⊥ a(2,1) a(2,2) x ⊥ a(2,1) x ⊥ [⊥] (2,2) (2,3)



b
a
x ⊥ a(2,1) a(2,2) x ⊥ a(2,1) x ⊥ [⊥]  (2,1) (2,2)
aa
x ⊥ a(2,1) x ⊥ [⊥][x ⊥] a(2,1) a(2,2) x ⊥ a(2,1) x ⊥ [⊥] (2,3)pop
x ⊥ a(2,1) a(2,2) x ⊥ a(2,1) x ⊥ [⊥] (2,3)ax ⊥ a(2,1) a(2,2) x ⊥ a(2,1) x ⊥ [⊥]pop(2,2) a(2,3) x ⊥ a(2,1) a(2,2) x ⊥ a(2,1) x ⊥ [⊥] (2,2) (2,3)



a
a
x ⊥ a(2,1) a(2,2) x ⊥ a(2,1) x ⊥ [⊥]pop(2,1) a(2,2) a(2,3) x ⊥ (2,1) (2,2) (2,3)



c
a
a
x ⊥ a(2,1) a(2,2) x ⊥ a(2,1) x ⊥ [⊥] (2,1) (2,2) (2,3)



a
a
a
x ⊥ a(2,1) a(2,2) x ⊥ a(2,1) x ⊥ [⊥]

···

···

···

···

38
The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

M. Hague and A. W. To

and, to finish the definition of B(x, y), we add the further constraint that the node x isreachable from the initial configuration via a path of the form ⊥ x x0 a (b a)∗ c (pop a)∗ .
The above interpretation gives the infinite half-grid, shown in Figure 2.
J39