Reachability in Higher-Order-Counters

Higher-order counter automata (\HOCS) can be either seen as a restriction of higher-order pushdown automata (\HOPS) to a unary stack alphabet, or as an extension of counter automata to higher levels. We distinguish two principal kinds of \HOCS: those that can test whether the topmost counter value is zero and those which cannot. We show that control-state reachability for level $k$ \HOCS with $0$-test is complete for \mbox{$(k-2)$}-fold exponential space; leaving out the $0$-test leads to completeness for \mbox{$(k-2)$}-fold exponential time. Restricting \HOCS (without $0$-test) to level $2$, we prove that global (forward or backward) reachability analysis is $\PTIME$-complete. This enhances the known result for pushdown systems which are subsumed by level $2$ \HOCS without $0$-test. We transfer our results to the formal language setting. Assuming that $\PTIME \subsetneq \PSPACE \subsetneq \mathbf{EXPTIME}$, we apply proof ideas of Engelfriet and conclude that the hierarchies of languages of \HOPS and of \HOCS form strictly interleaving hierarchies. Interestingly, Engelfriet's constructions also allow to conclude immediately that the hierarchy of collapsible pushdown languages is strict level-by-level due to the existing complexity results for reachability on collapsible pushdown graphs. This answers an open question independently asked by Parys and by Kobayashi.

In the setting of classical pushdown automata it is well known that restricting the stack alphabet to one single symbol, i.e., reducing the pushdown storage to a counter, often makes solving algorithmic problems easier. For instance, control state reachability for pushdown automata is P-complete whereas it is NSPACE(log(n))-complete for counter automata. Then again, results from counter automata raise new insights to the pushdown case by providing algorithmic lower bounds and important subclasses of accepted languages separating different classes of complexity. In this paper we lift this idea to the higher-order setting by investigating reachability problems for higher-order counter automata (HOCA), i.e., HOPA over a one-element stack alphabet. Analogously to counter automata, we introduce level k HOCA in two variants: with or without 0-tests. Throughout this paper, we write k-HOCA − for the variant without 0-tests and k-HOCA + for the variant with 0-tests. Transferring our results' constructions back to HOPA will then allow to answer a recent open question [16,13].
To our knowledge, the only existing publication on HOCA is by Slaats [17]. She proved that (k + 1)-HOCA + can simulate level k pushdown automata (abbreviated k-HOPA). In fact, even (k + 1)-HOCA − simulate k-HOPA. Slaats conjectured that L(k-HOCA + ) L(k-HOPA) where L(X) denotes the languages accepted by automata of type X. We can confirm this conjecture by combining the proof ideas of Engelfriet [7] with our main result on control-state reachability for HOCA in Theorems 13 and 14: control state reachability on k-HOCA + is complete for DSPACE( d∈N exp k−2 (n d )) and control state reachability on k-HOCA − is complete for DTIME( d∈N exp k−2 (n d )). These results are obtained by adapting a proof strategy relying on reductions to bounded space storage automata originally stated for HOPA by Engelfriet [7]. His main tool are auxiliary SPACE(b(n)) P k automata where P k denotes the storage type of a k-fold nested pushdown (see Section 2 for a precise definition). Such a (two-way) automaton has an additional storage of type P k , and a Turing machine worktape with space b(n). His main technical result shows a trade off between the space bound b and the number of iterated pushdowns k. Roughly speaking, exponentially more space allows to reduce the number of nestings of pushdowns by one. Similarly, at the cost of another level of pushdown, one can trade alternation against nondeterminism. Here, we also restate reachability on k-HOCA + as a membership problem on alternating auxiliary SPACE(exp k−3 (n)) Z+ automata (where Z+ is the new storage type of a counter with 0-test). For our DSPACE( d∈N exp k−2 (n d ))-hardness proof we provide a reduction of DSPACE( d∈N exp(exp k−3 (n d ))) to alternating auxiliary SPACE(exp k−3 (n)) Z+ automata that is inspired by Jancar and Sawa's PSPACE-completeness proof for the non-emptiness of alternating automata [10]. For containment we adapt the proof of Engelfriet [7] and show that membership for alternating auxiliary SPACE(exp k−3 (n)) Z+ automata can be reduced to alternating reachability on counter automata of size exp k−2 (n), where n is the size of the original input, which is known to be in DSPACE( d∈N exp k−2 (n d )) (cf. [8]).
For the case of k-HOCA − the hardness follows directly from the hardness of reachability for level (k − 1) pushdown automata and the fact that the latter can be simulated by k-HOCA − . For containment in DTIME( d∈N exp k−2 (n d )) the mentioned machinery of Engelfriet reduces the problem to the case k = 2.
The proof that control-state reachability on 2-HOCA − is in P is implied by Theorem 5 which proves a stronger result: both the global regular forward and backward reachability problems for 2-HOCA − are P-complete. The backward reachability problem asks, given a regular set C of configurations, for a (regular) description of all configurations that allow to reach one in C. This set is typically denoted as pre * (C). Note that there is no canonical way of defining a regular set of configurations of 2-HOCA − . We are aware of at least three possible notions: regularity via 2-store automata [2], via sequences of pushdown-operations [4], and via encoding in regular sets of trees. We stick to the latter, and use the encoding of configurations as binary trees introduced in [11]: We call a set C of configurations regular if the set of encodings of configurations {E(c) | c ∈ C} is a regular set of trees (where E denotes the encoding function from [11]). Note that the other two notions of regularity are both strictly weaker (with respect to expressive power) than the notion of regularity we use here. Nevertheless, our result does not carry over to these other notions of regularity as they admit more succinct representations of certain sets of configurations. See Appendix E for details.
Besides computing pre * (C) in polynomial time our algorithm also allows to compute the reachable configurations post * (C) in polynomial time. Thus, 2-HOCA − subsumes the well-known class of pushdown systems [1] while still possessing the same good complexity with respect to reachability problems.

Storage Types and Automata
An elegant way for defining HOCA and HOPA is the use of storage types and operators on these (following [7]). For simplicity, we restrict ourselves to what Engelfriet calls finitely encoded storage types. Definition 1. For X some set, we call a function t : X → {true, f alse} an Xtest and a partial function f : X → X an X-operation. A storage type is a tuple S = (X, T, F, x 0 ) where X is the set of S-configurations, x 0 ∈ X the initial S-configuration, T a finite set of X-tests and F a finite set of X-operations containing the identity on X, i.e., id X ∈ F .
We define the storage type counter without 0-test Z = P {⊥} , which is the pushdown storage over a unary pushdown alphabet. We define the storage type counter with 0-test Z+ exactly like Z but we add the test empty? to the set of tests where empty?(x) = true if x = ⊥ (the plus in Z+ stands for "with 0-test"). In other words, empty? returns false iff the operation pop is applicable.
Definition 2. For a storage type S = (X, T, F, x 0 ) we define an S automaton as a tuple A = (Q, q 0 , q f , ∆) where as usual Q is a finite set of states with initial state q 0 and final state q f and ∆ is the transition relation. The difference to a usual automaton is the definition of ∆ by ∆ = Q × {true, f alse} T × Q × F .
For q ∈ Q and x ∈ X, a transition δ = (q, R, p, f ) is applicable to the configuration (q, x) if f (x) is defined and if for each test t ∈ T we have R(t) = t(x), i.e., the result of the storage-tests on the storage configuration x agree with the test results required by the transition δ. If δ is applicable, application of δ leads to the configuration (p, f (x)). The notions of a run, the accepted language, etc. are now all defined as expected.
The Pushdown Operator We also consider P Σ as an operator on other storage types as follows. Given a storage type S = (X, T, F, x 0 ) let the storage type pushdown of S be P Σ (S) = (X ′ , T ′ , if f is defined on x (and undefined otherwise), -stay f (x ′ ) = β(σ, f (x)) if f is defined on x (and undefined otherwise), and pop(x ′ ) = β if β is nonempty (and undefined otherwise). Note that stay idX = id X ′ whence F ′ contains the identity. As for storages, we define the operator P to be the operator P {⊥,0,1} .

HOPA, HOCA, and their Reachability Problems
We can define the iterative application of the operator P on some storage S as follows: let P 0 (S) = S and P k+1 (S) = P(P k (S)). A level k higher-order pushdown automaton is a P k−1 (P) automaton. We abbreviate the class of all these automata with k-HOPA. A level k higher-order counter automaton with zero-test is a P k−1 (Z+) automaton and k-HOCA + denotes the corresponding class. 4 . Similarly, k-HOCA − denotes the class of level k higher-order counter automata without zero-test which is the class of P k−1 (Z) automata. Obviously, for any level k it holds that L(k-HOCA − ) ⊆ L(k-HOCA + ) ⊆ L(k-HOPA) where L(X) denotes the languages accepted by automata of type X.
We next define the reachability problems which we study in this paper.
Definition 3. Given an S automaton and one of its control states q ∈ Q, then the control state reachability problem asks whether there is a configuration (q, x) that is reachable from (q 0 , x 0 ) where x ∈ X is an arbitrary S-configuration.
Assuming a notion of regularity for sets of S configurations (and hence for sets of configurations of S automata), we can also define a global variant of the control state reachability problem.
Definition 4. Given an S automaton A and a regular set of configurations C, the regular backwards reachability problem demands a description of the set of configurations from which there is a path to some configuration c ∈ C.
Analogously, the regular forward reachability problem asks for a description of the set of configurations reachable from a given regular set C. In the following section, we consider the regular backwards (and forwards) reachability problem for the class of 2-HOCA − only.

Regular Reachability for 2-HOCA −
The goal of this section is to prove the following theorem extending a known result on regular reachability on pushdown systems to 2-HOCA − : Theorem 5. Reg. backwards/forwards reachability on 2-HOCA − is P-complete.

Returns, Loops, and Control State Reachability
Proving Theorem 5 is based on the "returns-&-loops" construction for 2-HOPA of [11]. As a first step, we consider the simpler case of control-state reachability: Proposition 6. Control state reachability for 2-HOCA − is P-complete.
In [11] it has been shown that certain runs, so-called loops and returns, are the building blocks of any run of a 2-HOPA in the sense that solving a reachability problem amounts to deciding whether certain loops and returns exist. Here, we analyse these notions more precisely in the context of 2-HOCA − in order to derive a polynomial control state reachability algorithm. Using this algorithm we can then also solve the regular backwards reachability problem efficiently.
For this section, we fix a P(Z)-automaton A = (Q, q 0 , F, ∆). Recall that the P(Z)-configurations of A are elements of (Σ × {⊥} + ) + . We identify ⊥ m+1 with the natural number m and the set of storage configurations with (Σ × N) + .
One of the underlying reasons why control state reachability for pushdown systems can be efficiently solved is the fact that it is always possible to reach a certain state without increasing the pushdown by more than polynomially many elements. In the following, we prove an analogue of this fact for P(Z). For a given configuration, if there is a return or loop starting in this configuration, then this return or loop can be realised without increasing the (level 2) pushdown more than polynomially. This is due to the monotonic behaviour of Z: given a Z configuration x, if we can apply a sequence ϕ of transitions to x then we can apply ϕ to all bigger configurations, i.e., to any configuration of the form push n ⊥ (x). Note that this depends on the fact that Z contains only trivial tests (the test top ⊥ always returns true). In contrast, for Z+, if ϕ applies a couple of pop operations and then tests for zero and performs a transition, then this is not applicable to a bigger counter because the 0-test would now fail.
For a P(Z) configuration x = (σ 1 , n 1 )(σ 2 , n 2 ) . . . (σ m , n m ), let |x| = m be its height. Let r be some run starting in (q, x) for some q ∈ Q. The run r increases the height by at most k if |x ′ | ≤ |x| + k for all configurations (q ′ , x ′ ) of r.
Definition 8. Let s ∈ ({⊥} × N) + . We write ret k (s) and lp k (s), resp., for the set of pairs of initial and final control states of returns or loops starting in s and increasing the height by at most k. We write ret ∞ (s) and lp ∞ (s),resp., for the union of all ret k (sw) or lp k (s).
The existence of a return (or loop) starting in sw (or s ′ w) (with s ∈ ({⊥} × N) + , s ′ ∈ ({⊥} × N) * and w ∈ {⊥} × N) does not depend on the concrete choice of s or s ′ . Thus, we also write ret k (w) for ret k (sw) and lp k (w) for lp k (s ′ w).
By induction on the length of a run, we first prove that P(Z) is monotone in the following sense: let s ∈ (Σ × N) * , t = (σ, n) ∈ Σ × N, q, q ′ ∈ Q and r a run starting in (q, st) and ending in state q ′ . If the topmost counter of each configuration of r is at least m, then for each n ′ ≥ n−m there is a run r ′ starting in (q, s(σ, n ′ )) and performing exactly the same transitions as r. In particular, for all k ∈ N ∪ {∞}, σ ∈ Σ and m 1 ≤ m 2 ∈ N, ret k ((σ, m 1 )) ⊆ ret k ((σ, m 2 )) and lp k ((σ, m 1 )) ⊆ lp k ((σ, m 2 )).
We next show that the sequence (ret k ((σ, m))) m∈N stabilises at m = |Σ||Q| 2 . From this we conclude that ret ∞ = ret |Σ| 2 |Q| 4 , i.e., in order to realise a return with arbitrary fixed initial and final configuration, we do not have to increase the height by more than |Σ| 2 |Q| 4 (if there is such a return at all).
The proof uses the fact that we can find an m ′ ≤ |Σ||Q| 2 with ret k ((σ, m ′ )) = ret k (σ, m ′ + 1) for all σ by the pigeonhole-principle. Using monotonicity of P(Z) we conclude that ret k (σ, m ′ ) = ret k (σ, m) for all m ≥ m ′ . A similar application of the pigeonhole-principle shows that there is a k ≤ |Σ| 2 · |Q| 4 such that ret k ((σ, i)) = ret k+1 ((σ, i)) for all σ and all i ≤ |Σ||Q| 2 (or equivalently for all i ∈ N). By induction on k ′ ≥ k we show that ret k ′ = ret k because any subreturn that increases the height by k + 1 can be replaced by a subreturn that only increases the height by k. Thus, we obtain the following lemma.
Proof (of Proposition 6). Since 2-HOCA − can trivially simulate pushdown automata, hardness follows from the analogous hardness result for pushdown automata. Containment in P uses the following ideas: 1. We assume that the input (A, q) satisfies that q is reachable in A iff (q, (⊥, 0)) is reachable and that A only uses instructions of the forms pop, push σ,id , and stay f . Given any 2-HOCA − A ′ and a state q, it is straightforward to construct (in polynomial time) a 2-HOCA − A that satisfies this condition such that q is reachable in A ′ iff it is reachable in A. 2. Recall that ret ∞ (w) = ret k0 (w) for k 0 = |Σ| 2 · |Q| 4 and for all w ∈ Σ × N. Set h 0 = |Σ| · |Q 2 |. We want to compute a table (a σ,p,q ) σ,p,q∈Σ×Q 2 with values in {∞, 0, 1, 2, . . . , h 0 } such that a σ,p,q = min{i | (p, q) ∈ ret k0 ((σ, i))} (where we set min{∅} = ∞). Due to Lemmas 9 and 10 such a table represents ret ∞ in the sense that (p, q) ∈ ret ∞ ((σ, i)) iff i ≥ a σ,p,q . 3. With the help of the table (a σ,p,q ) (σ,p,q)∈Σ×Q 2 we compute in polynomial time a P automaton A ∞ which executes the same level 1 transitions as A and simulates loops of A in the following sense: if there is a loop of A starting in (q, (σ, i)) performing first a push τ,id operation and then performing a return with final state p, we allow A ′ to perform an id-transition from (q, (σ, i)) to (p, (σ, i)). This new system basically keeps track of the height of the pushdown up to h 0 by using a pushdown alphabet {⊥ 0 , . . . , ⊥ h0 , ⊥ ∞ } where the topmost symbol of the pushdown is ⊥ i iff the height of the pushdown is i (where ∞ stands for values above h 0 ). After this change of pushdown alphabet, the additional id-transitions are easily computable from the table (a σ,p,q ) (σ,p,q)∈Σ×Q 2 . The resulting system has size O(h 2 0 · (|S| + 1)), i.e., is polynomial in the original system A.
In fact, for step 2 we already use a variant of steps 3 and 4: we compute ret ∞ = ret |Σ| 2 |Q| 4 by induction starting with ret 0 . If we remove all level 2 operations from A and store the topmost level 2 stack-symbol in the control state we obtain a pushdown automaton B such that (q, Thus, the results of polynomially many reachability queries for B determine the table for ret 0 . Similarly, we can use the table of ret i to compute the table of ret i+1 as follows. A return extending the height of the pushdown by i + 1 decomposes into parts that do not increase the height at all and parts that perform a push τ,id followed by a return increasing the height by at most i. Using the table for ret i we can easily enrich B by id-transitions that simulate such push operations followed by returns increasing the height by at most i. Again, determining whether (q, q ′ ) ∈ ret i+1 (σ, k) reduces to one reachability query on this enriched B for each pop-transition of A. With these ideas in mind, it is straightforward to check that algorithm ReachHOCA-in Figure 2 (using algorithm GeneratePDA of Figure 1 as subroutine for step 3) solves the reachability problem for 2-HOCA − (of the form described in step 1) in polynomial time. In this algorithm, ReachPDA (A ′ , c, q) refers to the classical polynomial time algorithm that determines whether in the (level 1) pushdown automaton A ′ state q is reachable when starting in configuration c; a transition (q, (σ, τ ), f, p) refers to a transition from state q to state p applying operation f that is executable if the (level 2) test top σ and the (level 1) test test(top τ ) both succeed. ⊓ ⊔
If v 1 = 0, we set p l = ∅ and p r = (σ 2 , v 2 ) . . . (σ m , v m ). Otherwise, there is a maximal 1 ≤ j ≤ m such that v 1 , . . . , v j ≥ 1 and we set p l = ( The tree-encoding E of p is given as follows: where ⊥(t 1 , t 2 ) is the tree with root ⊥ whose left subtree is t 1 and whose right subtree is t 2 . For a configuration c = (q, p) we define E(c) to be the tree q(E(p), ∅). The picture beside the definition of E shows the encoding of the configuration (q, (a, 2)(a, 2)(a, 0)(b, 1)). Note that for each element (σ, i) of p, there is a path to a leaf l which is labelled by σ such that the path to l contains i + 2 left successors. Moreover, the inorder traversal of the tree induces an order of the leaves which corresponds to the left-to-right order of the elements of p. We call a set C of configurations regular if the set {E(c) | c ∈ C} is a regular set of trees.
E turns the reachability predicate on 2-HOCA − into a tree-automatic relation [11], i.e., for a given 2-HOCA − A, there is a tree-automaton T A accepting the convolution of E(c 1 ) and E(c 2 ) for 2-HOCA − configurations c 1 and c 2 iff there is a run of A from c 1 to c 2 . This allows to solve the regular backwards reachability problem as follows. On input a 2-HOCA − and a tree automaton T recognising a regular set C of configurations, we first compute the tree-automaton T A . Then using a simple product construction of T A and T and projection, we obtain an automaton T pre which accepts pre * (C) = {E(c) | ∃c ′ ∈ C and a run from c to c ′ }.
The key issue for the complexity of this construction is the computation of T A from A. The explicit construction of T A in [11] involves an exponential blow-up. In this construction the blow-up is only caused by a part of T A that computes ret ∞ (σ, m) for each σ ∈ Σ on input a path whose labels form the word ⊥ m . Thus, we can exhibit the following consequence. Corollary 11 ([11]). Given a 2-HOCA − A with state set Q, we can compute the tree automaton T A in P, if we can compute from A in P a deterministic word automaton T ′ with state set Q ′ ⊆ σ∈Σ (2 Q×Q ) 2 such that for all m ∈ N the state of T ′ on input ⊥ m is (ret ∞ (σ, m), lp ∞ (σ, m)) σ∈Σ .
Thus, the following lemma completes the proof of Theorem 5.
Proof. Let n 0 = 2 · |Σ| · |Q| 2 . Recall algorithm ReachHOCA-of Figure 2. In this polynomial time algorithm we computed a matrix A = (a σ,p,q ) (σ,p,q)∈Σ×Q 2 representing ret ∞ and a pushdown automaton A ∞ (of level 1) simulating A in the sense that A ∞ reaches a configuration ((q, σ)p) for a pushdown p of height n if and only if A reaches (q, (σ, n)). It is sufficient to describe a polynomial time algorithm that computes M i = (ret ∞ ((σ, n)), lp ∞ ((σ, n))) σ∈Σ for all n ≤ n 0 . A ′ is then the automaton with state set {M i | i ≤ n 0 }, transitions from M i to M i+1 for each i < n 0 and a transition from M n0 to M n0 . The correctness of this construction follows from Lemma 9.
Let us now describe how to compute M i in polynomial time. Since A ∞ simulates A correctly, there is a loop from (q, (σ, i)) to (q ′ , (σ, i)) of A if and only if there is a run of A ∞ from ((q, σ), p i ) to ((q ′ , σ), p i ) for p i = ⊥ 0 ⊥ 1 . . . ⊥ i (where we identify ⊥ j with ⊥ ∞ for all j > h 0 ). Thus, we can compute the loop part of M i by n 0 many calls to an algorithm for reachability on pushdown systems. Note that (p, q) ∈ ret ∞ ((σ, i)) with respect to A if there is a state r and some τ ∈ Σ such that (r, τ, pop, q) is a transition of A and (r, τ ) is reachable in A ∞ from ((q, σ), i). Thus, with a loop over all transitions of A we reduce the computation of the returns component of M i to polynomially many control state reachability problems on a pushdown system. ⊓ ⊔ 4 Reachability for k-HOCA − and k-HOCA + Using slight adaptations of Engelfriet's seminal paper [7], we can lift the result on reachability for 2-HOCA − to reachability for k-HOCA − (cf. Appendix B ).
Theorem 13. For k ≥ 2, the control state reachability problem for k-HOCA − is complete for DTIME( d∈N exp k−2 (n d )). For k ≥ 1, the alternating control state reachability problem for k-HOCA − is complete for DTIME( d∈N exp k−1 (n d )).
Hardness follows from the hardness of control state reachability for (k − 1)-HOPA [7] and the trivial fact that the storage type P k−1 of (k − 1)-HOPA can be trivially simulated by the storage type P k−1 (Z) of k-HOCA − . Containment for the first claim is proved by induction on k (the base case k = 2 has been proved in the previous section). For k ≥ 3, we use Lemma 7.11, Theorems 2.2 and 2.4 from [7] and reduce reachability of k-HOCA − to reachability on (exponentially bigger) (k − 1)-HOCA − . For the second claim, we adapt Engelfriet's Lemma 7.11 to a version for the setting of alternating automata (instead of nondeterministic automata) and use his Theorems 2.2. and 2.4 in order to show equivalence (up to logspace reductions) of alternating reachability for (k − 1)-HOCA − and reachability for k-HOCA − . We can also reduce reachability for k-HOCA + to reachability for (k − 1)-fold exponentially bigger 1-HOCA + . Completeness for NSPACE(log(n)) of reachability for 1-HOCA + (cf. [8]) yields the upper bounds for reachability for k-HOCA + . The corresponding lower bounds follow by applications of Engelfriet's theorems and an adaptation of the PSPACE-hardness proof for emptiness of alternating finite automata by Jancar and Sawa [10].

Back to HOPS: Applications to Languages
Engelfriet [7] also discovered a close connection between the complexity of the control state reachability problem for a class of automata and the class of languages recognised by this class. We restate a slight extension (cf. AppendixD ) of these results and use them to confirm Slaat's conjecture from [17].
Proposition 15. Let S 1 and S 2 be storage types and C 1 , C 2 complexity classes such that C 1 C 2 . If control state reachability for nondeterministic S i automata is complete for C i , then there is a deterministic S 2 automaton accepting some language L such that no nondeterministic S 1 -automaton accepts L.
In fact, Engelfriet's proof can be used to derive a separating language. For a storage type S = (X, T, F, x 0 ), we define the language of valid storage sequences VAL(S) as follows. For each test t ∈ T and r ∈ {true, f alse} we set t r := id↾ {x∈X|t(x)=r} and set Σ = F ∪ {t r | t ∈ T, r ∈ {true, f alse}}. For s ∈ Σ * such that s = a 1 . . . a n , and x ∈ X we write s(x) for a n (a n−1 (. If the previous proposition separates the languages of S 2 automata from those of S 1 automata, then it follows from the proof that VAL(S 2 ) is not accepted by any S 1 automato (cf. AppendixD ).
The crucial underlying construction detail of the proof of Proposition 15 is quite hidden within the details of Engelfriet's technical and long paper. Its usefulness in other contexts -e.g., for higher-order pushdowns or countershas been overseen so far. Here we give another application to collapsible pushdown automata: reachability for collapsible pushdown automata of level k is DSPACE(exp k−1 (n))-complete (cf. [3]). Thus, Proposition 15 trivially shows that the language of valid level (k + 1) collapsible pushdown storage sequences separates the collapsible pushdown languages of level k + 1 from those of level k. This answers a question asked by several experts in this field (cf. [16,13]). In fact, [16] uses a long and technical construction to prove the weaker result that there are more level 2k collapsible pushdown languages than level k collapsible pushdown languages. From Proposition 15 one also easily derives the level-bylevel strictness of the collapsible pushdown tree hierarchy and the collapsible pushdown graph hierarchy (cf. [12,13]).

Future Work
Our result on regular reachability gives hope that also complexity results on model checking for logics like the µ-calculus extend from pushdown automata to 2-HOCA. 2-HOCA − probably is a generalisation of pushdown automata that retains the good complexity results for basic algorithmic questions. It is also interesting whether the result on regular reachability extends to the different notions of regularity for k-HOCA mentioned in the introduction. HOCA also can be seen as a new formalism in the context of register machines as currently used in the verification of concurrent systems. HOCA allow to store pushdown-like structures of register values and positive results on model checking HOCA could be transferred to verification questions in this concurrent setting.
Note that there is an additional bibliographic reference section at the end of the appendix; we use capital letters to refer to these works, e.g., [A].
1. If r never visits a configuration of the form r(j) = (q j , s j (σ j , 0)), we obtain by monotonicity of P(Z) a run r ′ witnessing (q, q ′ ) ∈ ret k+1 ((σ, n − 1)) \ ret k+1 ((σ, m k+1 )) contradicting minimality of n. 2. Otherwise, there is a maximal j such that r(j) = (q j , s j (σ j , 0)). Since any operation alters the value of the topmost counter by at most 1, we find a maximal j 1 ≤ j such that r(j 1 ) = (q j1 , s j1 (σ j1 , m k+1 + 1)). Since r is a return and j 1 is not the last position in r, there is a j 2 ≥ j such that r(j 2 ) = (q j2 , s j1 ), i.e., the restriction of r to [j 1 , j 2 ] is a return witnessing Due to monotonicity of P(Z), we can lift a return from (q j1 , s j1 (σ j1 , m k+1 )) to state q j2 to a return r ′ from (q j1 , s j1 (σ j1 , m k+1 + 1)) to state q j2 such that the topmost counter of all configurations are at least 1. Now replace in r the subrun r↾ [j1,j2] by r ′ and repeat this case distinction on the resulting run again.
In the second case, we always choose a maximal j such that the topmost counter is 0. We then replace all occurring configurations by others that do not assume 5 We use as the symbol for the disjoint union.
the counter value 0 on the topmost counter. Thus, if we iterate this process, the number j in each step strictly decreases. Since the run is finite, after some iterations, we must reach the contradiction to the first case.
Thus, we conclude that ret k ((σ, m)) = ret k ((σ,m)) for all k ∈ N and all m ≥m. This immediately implies the analogous result for k = ∞.
The claim for loops is proved completely analogous: there is a value m ∞ between |Σ||Q| 2 and 2 · |Σ||Q| 2 such that By a similar case distinction as in the return case, also from this point on the loops stabilise. The only difference now is that a counter value 0 can occur within a return starting with a topmost counter value m ∞ + 1 or within a loop starting with topmost counter value m ∞ + 1. Nevertheless either the first part of the lemma or (1) allow to replace this subrun by one not visiting configurations with topmost counter value 0.
Similar to the previous proof we now show that ret k0 = ret k for all k ≥ k 0 . For k ≤ k 0 + 1, this is already guaranteed by choice of k 0 . Assume that there are σ ∈ Σ, k > k 0 + 1 and i ∈ N such that (q, q ′ ) ∈ ret k ((σ, i)) \ ret k0 ((σ, i)) and that r is a return witnessing this fact. We assume that k is minimal whence Thus, r is a run that increases the height by k. It decomposes as where each m i is a subrun only using stay f -operations (whence all configurations have the same height as the initial one), p i is a subrun performing only one push σi,fi , r i is a return, and s is a subrun performing only one pop-operation. Now, some of the r i increase the height by k − 1. By (2), we can replace each such r i by some return r ′ i that increases the height by at most k 0 . This shows (q, q ′ ) ∈ ret k−1 ((σ, i)) = ret k0 ((σ, i)) contradicting our assumption.
The proof for lp ∞ = lp |Σ| 2 ·|Q| 4 +1 follows because whenever a loop increases the height of the stack, it continues with some return. By the result for returns, this subreturn can be replaced by one that only increases the height by |Σ| 2 ·|Q| 4 .

B.1 Auxiliary Storage Automata
Following Engelfriet's approach [7], we use Auxiliary SPACE(b(n)) S automata (where b : N → N is some function) for the analysis of S automata. The former are a general model for computing. An instance is given by 1. a finite control structure with control states Q, 2. an initial state q 0 ∈ Q, 3. transition rules ∆, 4. a two-way read-only input tape, 5. a worktape (like for Turing machines) of size b(n) where n is the size of the input, and 6. a storage S.
The storage S can be any known storage type used for automata, e.g., stacks, pushdowns, or counters. As usual, the above introduced automata can be deterministic, nondeterministic, or alternating. We refer to [7] for a detailed formal introduction, the connection to Turing-machine based notions of time and space complexity, as well as for references to the classical literature on these machine models.
Note, that a 1-way auxiliary SPACE(b(n)) S automaton is defined analogously whereas the input tape is only read one-way. Most classical automata models can be directly rendered into this framework, e.g., nondeterministic 1way S automata where S is the trivial storage correspond to nondeterministic finite automata; 2-way auxiliary SPACE(b(n)) S automata where S is the trivial storage are the classical b(n)-space bounded Turing machines; 1-way S automata where S is a pushdown correspond to pushdown automata.
The configuration of an auxiliary SPACE(b(n)) S automaton is the tuple containing the current finite state q ∈ Q, the contents of the auxiliary work tape, i.e., a word w of size bounded in SPACE(b(n)), as well as the configuration x ∈ X of S. As usual, we define a run of an automaton as a sequence of configurations that is conform with the underlying transition rules and the semantics of the storage type. The applicable transition rules depend on the outcome of the storage tests applied to the current storage configuration, the current control state and the next input symbol.

B.2 Technical Results
Before we analyse control-state reachability on k-HOCA + and k-HOCA − , we recall and extend some results of Engelfriet. The following results are Theorems 2.2 and 2.4 of [7].
Lemma 17. Let b be some function satisfying b(n) ≥ log(n) for all n ∈ N and let S be a storage type. In polynomial time, we can translate an alternating auxiliary SPACE( d∈N exp(db(n))) S automaton into an alternating auxiliary SPACE(b(n)) P(S) automaton such that both automata accept the same language and vice versa.
Lemma 18. For b(n) ≥ log(n) and every storage type S, there are polynomial time algorithms that translate a nondeterministic auxiliary SPACE(b(n)) P(S) automaton into an alternating auxiliary SPACE(b(n)) S automaton accepting the same language and vice versa.
A detailed look on Engelfriet's proof of Lemma 7.11 in [7] reveals that its analogue for alternating automata holds if we replace the role of nonemptyness by the role of control state reachability. Moreover, the logspace reduction of membership for auxiliary SPACE(log(n)) S automata to control state reachability for 1-way S automata extends to an b(n) space-bounded reduction of membership for auxiliary SPACE(b(n)) S automata to control state reachability for S automata (which now may have size exp(b(n)) when starting with an input of size n). Before we prove these claims, let us first define alternating reachability in our setting.
Definition 19. Let A be an alternating auxiliary SPACE(b(n)) S automaton. For a set C of configurations of A we define pre * (C) as the set of configurations c such that there is a computation tree T of A 1. the root of T is labelled by c, 2. all leaves of T are labelled by configurations c ′ ∈ C, 3. for each inner node t of T labelled by an existential configuration c there is exactly one successor t ′ in T and t ′ is labelled by a successor c ′ of c (w.r.t A), and 4. for each inner node t of T labelled by a universal configuration c there is, for For a state q of A, we say that q is alternatingly (control state) reachable in A if the initial configuration of A belongs to pre * ({(q, x) | x is an S-configuration}).
Remark 20. Note that we disallow that the computation tree T may contain a leaf labelled by some universal state c not in C such that no transition of A is applicable to c. This restrictive definition is necessary for the results provided in the following.
Definition 21. The alternating control state reachability problem for some class C of automata is the following. Input: A ∈ C, q a state of A Output: Is q alternatingly reachable in A.
The following lemmas extend Engelfriet's result on the connection between emptiness (or equivalently, control state reachability) of nondeterministic S automata and membership for nondeterministic auxiliary SPACE(log(n)) S automata to the setting of alternating automata.
Lemma 22. Let S be a storage type. Alternating (or nondeterministic, respectively) control state reachability of (1-way) S automata reduces to membership of alternating (nondeterministic, respectively) auxiliary SPACE(log(n)) S automata via logspace reductions.
Proof. Let A(S) denote the set of 1-way alternating S automata and fix an effective encoding A(S) of this set as binary strings. We write M ∈Ā(S) for the encoding of the automaton M ∈ A(S). Analogously, we write q for the encoding of some state q. We define an auxiliary SPACE(log(n)) S automaton which we call A such that L(A) = {M#q | M ∈ A(S), q a state of M and q alternating reachable by M}. Given an input string s, A first checks that s = M#q for some M ∈ A(S) and some state q of M. Now A simulates M storing two pointers on its tape, one called state pointer and one called transition pointer.
As initialisation the state pointer is set to the position of the input where the initial state of M is encoded.
We now iterate the following case distinction. If the state pointer points to (the encoding of) q, A accepts. Otherwise, the state pointer points to some state q ′ . Scanning the input string we determine whether q ′ is an existential state of M. If this is the case, we do an existential simulation step, otherwise we do a universal simulation step.
-Existential simulation step. The state pointer points to some state q ′ . Now we guess a transition applicable to the current configuration of M (which is (q ′ , x) for x the current storage configuration of A. This is done by setting the transition pointer to some value i such that at position i in the input string the encoding of a transition δ = (p, t, f, r) starts. A now checks that p = q ′ . Then it checks that the test formula t is satisfied by the current storage configuration. If this is not the fact, A rejects. Otherwise it applies f to the storage and changes the state pointer such that it points to the encoding of r. -Universal simulation step. The state pointer points to some universal state q ′ = q and the current S configuration (of A and of M) is x. Recall that q is alternatingly reachable from (q ′ , x) if there is a computation tree where the root is labelled by (q ′ , x) and is not a leaf (because q = q ′ ) and q is alternatingly reachable from every successor of (q ′ , x) in the computation tree.
In order to guarantee that (q ′ , x) has a successor configuration with respect to M, we universally spawn a subprocess that performs an existential simulation step. If this branch accepts, we still have to show that for any applicable transition, q is alternatingly reachable from the resulting configuration. For this purpose the transition pointer iterates over all positions in the encoding M of M. As soon as this iteration has been finished, this main process accepts. During the iteration it may spawn subprocesses as follows.
If the current position of the pointer points to a transition δ = (p, t, f, r) we check whether q ′ = p. In this case we universally spawn a subprocess. It checks whether the test formula t is satisfied by the current storage configuration. If not, the process accepts. Otherwise, A universally branches to an accepting branch and another branch by first applying f to the current storage configuration and then setting the state pointer to the position of the encoding of r and starting the next simulation step. It is straightforward to see that one of the following holds.
1. f is not applicable to the current storage configuration, thus δ does not provide a successor of the current configuration of M. In this case, the universal branching only spawns one accepting branch whence the subprocess dealing with δ accepts. 2. f is applicable to the current storage configuration. Then the subprocess applying f accepts if and only if q is alternatingly reachable from the δ-successor of the current configuration.
It is straightforward to prove that A accepts M#q if and only if q is alternatingly reachable by M. Moreover, A only needs universal states for the universal simulation step. Thus, restricting the input to nondeterministic S automata, the simulating machine A will also be nondeterministic instead of alternating. ⊓ ⊔ Engelfriet also provided a logspace reduction in the other direction in the nondeterministic case. We extend this result again to the alternating case and to auxiliary SPACE(b(n)) S automata for arbitrary space bound b.
Lemma 23. Let b(n) ≥ log(n) and M be an alternating (or nondeterministic) auxiliary SPACE(b(n)) S automaton. The membership problem for M is reducible to alternating (nondeterministic, respectively) control state reachability for S automata via a DSPACE(b(n))-computation.
Proof. Let Γ be the tape alphabet with blank symbol , Σ the input alphabet, Q the state set and q 0 ∈ Q the initial state of M. Without loss of generality M has only 1 accepting state and it enters this state if and only if the tape is completely blank and the heads of the input and the reading tape are on the first cell.
On input a word w, we construct an automaton A with state set Q×Γ b(|w|) × {1, 2, . . . b(|w|)} × {1, 2, . . . , |w|}. Note that each configuration fits into space O(b(|w|)). The initial state is (q 0 , w b(|w|)−|w| , 1, 1). Some state c = (q, γ 1 . . . γ b(|w|) , i, j) represents the configuration of M where the work tape contains the letters γ 1 . . . γ b(|w|) , M is in state q the head of the work tape is at position i and the head of the input tape is at position j. This state is an existential one if and only if q is an existential state of M. A has a transition (c, t, f, c ′ ) to state c ′ = (q ′ , γ ′ 1 . . . , γ ′ b(|w|) , i ′ , j ′ ) if and only if M has a transition with test-formula t and storage operation f whose application would translate configuration c to configuration c ′ (for all storage configurations where t is satisfied and f is appli- It is straightforward to prove that c f is alternatingly reachable by A if M accepts w. Note that A contains universal states if and only if M contains universal states.
⊓ ⊔ Analogously to Engelfriet's proof that a pushdown can replace alternation, we now investigate tradeoffs concerning the storage type Z+. This proof is inspired by the PSPACE-hardness proof for emptiness of alternating finite automata recently published by Jancar and Sawa [10].
Lemma 24. Let b(n) = exp k (n) for some k ≥ 0. Let M be a deterministic auxiliary SPACE(b(n)) automaton, i.e., a deterministic SPACE(b(n)) Turingmachine. We can compute in logspace an alternating auxiliary SPACE(log(b(n))) Z+ automaton A such that M accepts w iff A accepts w for all w ∈ Σ * .
Proof. Assume that M has state set Q, initial state q 0 ∈ Q, final state q f ∈ Q and tape alphabet Γ . The main states of A come from the set Z = Γ ∪ (Γ × Q). Moreover the state set Q ′ of A contains p(|Z|) many auxiliary states for some polynomial p. For simplicity of the presentation we omit the formal specification of these states. Our goal is to construct an automaton A whose configurations are of the form (z, t, i) ∈ Z × {0, 1} log(b(n)) × N where z is the current state of A, t is the content of its tape (which we identify with a binary encoded natural number between 0 and b(n)) and i is the current counter value.
Our goal is to define A in such a way that A accepts from configuration (z, t, i) on input w if at time step i of the computation of M at the t-th cell of M's tape, the content is z (where we say that the t-th cell content is (q, γ) ∈ Q × Γ if the cell contains γ and M is reading this cell in state q). Let preds(z) be the set of triples (z 1 , z 2 , z 3 ) such that the one-step computation of M on the tape described by z 1 z 2 z 3 leads to the replacement of z 2 by z. If A is in some configuration (z, t, i) with 0 < t < b(n) and i > 0, it nondeterministically chooses the hopefully correct triple (z 1 , z 2 , z 3 ) ∈ preds(z) and universally branches to configurations (z 1 , t − 1, i − 1), (z 2 , t, i − 1), (z 3 , t + 1, i − 1). Note that a finite amount of auxiliary states suffices to calculate the tape content t + 1 and t − 1 from t. We now specify the acceptance condition. Configurations ( , 0, i) and ( , b(n), i) are accepting (for all i ∈ N) while all other configurations with tape t = 0 or t = b(n) are rejecting (again, only finitely many states are needed to check whether we are in one of these configurations). Assuming that the input is w = a 1 . . . a n , let configuration ((q 0 , a 1 ), 1, 0), configurations (a i , i, 0) for 2 ≤ i ≤ n, and configurations ( , j, 0) for j > n be all accepting. All other configurations with counter value 0 are rejecting. Note that this acceptance condition relies on the input and can be checked with finitely many auxiliary states. In a configuration (z, t, 0) we parse the input word to the t-th letter and compare z to this letter (if w ended before, then z has to be the blank symbol ).
An easy induction on i shows that there is an accepting computation of A starting in (z, t, i) with input w if and only if in the computation of M on w the t-th letter of the i-th configuration is z (where as before z = (q, γ) ∈ Q × Γ means that the content of the t-th cell is γ, M's head is positioned at the t-th cell and M is in state q). Now we add to A an initialisation phase that, on input w, guesses a letter γ ∈ Γ , a number t ≤ b(|w|) and some number i ∈ N switching to configuration ((q f , γ), t, i). Now A accepts w if and only if the computation of M on w is accepting.

B.3 Control-State Reachability on k-HOCA +
We prove the part of Theorem 14 on reachability. The claim for alternating reachability follows directly from this result as we will explain in Section B.5. We determine the exact complexity of reachability on k-HOCA + . For the base case we use a result mentioned by Göller [8].
Proposition 26. Control state reachability for k-HOCA + is DSPACE( d∈N exp k−2 (n d ))complete for all k ≥ 2.
Proof. For containment, let us first consider the case k = 2. Given a 2-HOCA + A and a state q, control state reachability reduces by Lemma 22 to a membership problem for a (nondeterministic) auxiliary (2-way) SPACE(log(n)) P(Z+) automaton. Due to Lemma 18 this automaton can be translated into an alternating auxiliary SPACE(log(n)) Z+ automaton. Due to Lemma 23, membership for this machine is logspace reducible to alternating control state reachability on alternating (1-way) Z+ automata which by Lemma 25 is solvable in PSPACE = DSPACE( d∈N exp 0 (n d )). Now we proceed by induction on k. Given a k-HOCA + A (k ≥ 3) and a state q, control state reachability reduces by Lemma 22 to a membership problem for a (nondeterministic) auxiliary (2-way) SPACE(log(n)) P k−1 (Z+) automaton. Due to Lemma 18 this machine can be translated into an alternating auxiliary SPACE(log(n)) P k−2 (Z+) automaton. We apply Lemma 17 and obtain an equivalent alternating auxiliary SPACE(n d ) P k−3 (Z+) automaton (for some d ∈ N). Again with Lemma 18 this is translated to a nondeterministic auxiliary SPACE(n d ) P k−2 (Z+) automaton. Using the polynomial-space reduction from Lemma 23 we obtain a state q ′ and a (k − 1)-HOCA + A ′ of size exp(O(|A| d )) such that q is reachable in A if and only if q ′ is reachable in A ′ . By induction hypothesis the latter is decidable in space exp k−3 (|A ′ | d ′ ) for some d ′ ∈ N. Thus, in terms of |A| the space is bounded by This completes the containment proof.
We now prove hardness. Recall that Lemma 24 provided a reduction of any membership problem in DSPACE(exp k−2 (n d )) (d ∈ N) to a membership problem for an alternating auxiliary SPACE(exp k−3 (n d )) Z+ automaton. Due to Lemma 17 this can be reduced to a membership problem for an alternating auxiliary SPACE(log(n d )) P k−2 (Z+) automaton. Furthermore, by Lemma 18 this reduces to a membership problem for a nondeterministic auxiliary SPACE(log(n d )) P k−1 (Z+) automaton. Finally, due to Lemma 23, there is a polynomial time reduction of this problem to a control state reachability problem for a (1-way) P k−1 (Z+) automaton of size O(n d ), i.e., reachability for k-HOCA + .

B.4 Control-State Reachability on k-HOCA −
Based on our result that control state reachability for 2-HOCA − is in P (Proposition 6), Engelfriet's machinery allows to determine the complexity of reachability in n-HOCA − inductively. This proves the first half of Theorem 13. The claim on alternating reachability is proved in the following section.
Proposition 27. For k ≥ 2, the control state reachability problem for k-HOCA − is in DTIME( d∈N exp k−2 (n d )).
Proof. We use Engelfriet's machinery and induction: the case reachability for 2-HOCA − ∈ P has already been shown in Proposition 6. Given a k-HOCA − A of level k ≥ 3 and a state q, control state reachability reduces by Lemma 22 to a membership problem for some nondeterministic auxiliary SPACE(log(n)) P k−1 (Z) automaton. Due to Lemma 18 this automaton can be translated into an alternating auxiliary SPACE(log(n)) P k−2 (Z) automaton. We apply Lemma 17 and obtain an alternating auxiliary SPACE(dn) P k−3 (Z) automaton for some d ∈ N. Again with Lemma 18 this is translated to a nondeterministic auxiliary SPACE(dn) P n−2 (Z) automaton. Finally, we use the polynomialspace reduction from Lemma 23 and obtain a state q ′ and a (k − 1)-HOCA − A ′ of size exponential in that of A such that q is reachable in A if q ′ is reachable in A ′ . By induction hypothesis, we can decide this in time exp n−3 (p ′ (|A ′ |)) = exp n−2 (p(|A|)) for some polynomials p and p ′ . ⊓ ⊔

B.5 Alternating Control State Reachability
We derive our results on alternating reachability by use of a much more general relation between the pushdown operator and alternation.
Proposition 28. Given any storage type S, alternating control state reachability for S automata is logspace reducible to control state reachability of P(S) automata and vice versa.
Proof. Let A be an alternating S automaton and q some state. By Lemma 22 the alternating control state reachability problem for (A, q) reduces to a membership problem for an alternating auxiliary SPACE(log(n)) S automaton. This reduces by Lemma 18 to a membership problem for a nondeterministic auxiliary SPACE(log(n)) P(S) automaton. Finally, using Lemma 23 this problem reduces to a control state reachability problem for a nondeterministic P(S) automaton. Using the 'nondeterminism' variant of Lemma 22, the other direction of Lemma 18 and the 'alternation' variant of Lemma 23, the control state reachability problem for P(S) automata similarly reduces to the alternating control state reachability problem for alternating S automata.

C Equivalence of Storages
In [17] the notion of a level k counter automaton with 0-test was defined differently from our notion of k-HOCA + as follows. Basically Slaats uses the storage type P k−1 {⊥} (Z+) instead of P k−1 {⊥,0,1} (Z+). In the following we show that both variants lead to equivalent automata. Let us first recall the notion of equivalence of storage types (cf. [7]).
Definition 29. Let S and S ′ be storages. S can simulate S ′ , denoted as S ′ S, if for every one-way deterministic S ′ transducer there is a one-way deterministic S transducer defining the same transductions.
S and S ′ are equivalent, denoted as S ≡ S ′ , if S S ′ and S ′ S.
Remark 30. As pointed out by Engelfriet, for storage types S, S ′ such that S S ′ , for t ∈ {nondeterministic, alternating, deterministic} t S automata can be simulated by t S ′ automata.
Recall that we defined the storage type Z = P {⊥} . In the following, we also use Z as the operator P {⊥} acting on other storage types. We call Z(S) the storage type counter of S.

Proof. The direction from left to right is clear because P is an extension of Z.
We show how Z k−1 (Z+) can simulate P k−1 (Z+).
We first show that S := P(Z k−2 (Z+)) can be simulated by S ′ := Z k−1 (Z+). The idea is to encode the pushdown symbol of level k, by the level 1 counter value modulo 3 (recall that P uses the pushdown alphabet {⊥, 0, 1}). For this purpose we first replace in the P(Z k−2 (Z+)) every push ⊥ of level 1(i.e. a push applied to Z+) by 3 push ⊥ operations and each level 1 pop-operation by 3 popoperations of level 1. This results in an equivalent S automaton where the level 1 counter value is always 0 mod 3. Next, without loss of generality we assume that the S automaton only uses instructions of the form pop, push σ,id and stay f . For the rest of this simulation, we identify ⊥ with the number 2. We want to represent a pushdown symbol σ ∈ {0, 1, ⊥} by σ mod 3 on the level 1 counter. We initialise S ′ by applying 2 push ⊥ on level 1 (this results in the counter value 2, which is 2 mod 3 representing the initial symbol ⊥. Now we simulate the operations on S by S ′ -operations as follows (where we assume that the current S-configuration x is simulated by S ′ -configuration x ′ . 1. The top γ test for γ ∈ {0, 1, ⊥} can be simulated as follows. apply push ⊥,id , then determine the topmost symbol γ ′ ∈ {0, 1, ⊥} by level 1 pop-operations (while the 0-test fails) determining the value of the topmost level 1 counter modulo 3. After finishing the test we restore the pushdown by a pop operation and just have to compare γ with γ ′ . 2. The empty? test on level 1 is simulated by first determining which top γ test applies for γ ∈ {0, 1, ⊥} as in the simulation of top γ . Then we perform γ many pop-operations of level 1, then the empty? test of S ′ coincides with the empty? of S. We restore the pushdown by γ many push ⊥ operations of level 1. 3. A pop operation is simulated by pop. 4. A push γ,id operation is simulated by the following program: first determine the topmost symbol γ ′ ∈ {0, 1, ⊥} of x ′ . Then apply push ⊥,id , then apply γ ′ many level 1 pop-operations. No we apply γ many level 1 push ⊥ operations. 5. A stay f operations is simulated by stay f if f is not an operation of level 1.
If it is of level 1 we just duplicate it 3 times.

⊓ ⊔
Readers interested in a more throughout comparison of different possible definitions of higher-order one-couter automata are invited to have a look at Appendix F.

D Separation of Languages of Higher-Order Counter Automata With or Without 0-test
Under the assumption that our results on the reachability problem for HOCA implies a strict separation of the languages of higher-order counters and higher-order pushdowns. We first recall some results of Engelfriet that allows to shift results on 2-way auxiliary automata down to 1-way automata. We recall his proofs in order to extract the constructive content.
Let N-aux-SPACE(log(n)) − S-L denote the languages accepted by nondeterministic auxiliary SPACE(log(n))S automata. Let T be the class of nondeterministic logspace transducers. Let T −1 (L) := τ −1 (L) | τ ∈ T, L ∈ L be the class of languages obtained by application of transductions from T to languages from L.
Recall that VAL(S) is the language of valid storage sequences for storage type S. It is accepted by a deterministic S automaton with only 1 state q and no ε-transitions that works as follows. Transitions on input an S-operation f are of the form (q, f, ∅, f, q), i.e., S on input f applies f unconditionally and transitions on input a test (t = r) are of the form (q, (t = r), (t, r), id X , q)< i.e., computation continues if test t results in r and the storage remains unchanged. Proof (sketch). Given a nondeterministic auxiliary SPACE(log(n))−S automaton A we can split it into two devices as follows. First we use a nondeterministic logspace transducer T that simulates A but instead of performing S-tests oroperations it writes these on the output tape (tests are written together with the expected test result). Then we use the deterministic S automaton S recognising VAL(S) and check whether the output of T is a valid sequence of operations and tests of S.
For the other direction, given a transducer and an S-automaton, the language of their composition is recognised by a nondeterministic auxiliary SPACE(log(n))− S automaton which is a simple product of the two automata.

⊓ ⊔
A straightforward extension of Engelfriet's Corollary 7.2 from [7] is the following.
Corollary 33. Let S and S ′ be storage types.
Due to Lemmas 22 and 23, complexity results on control state reachability for S-automata help to separate the classes N-aux-SPACE(log(n)) − S-L for different storage types S as follows.
Lemma 34. Let S be some storage type and C a complexity class closed under DSPACE(log(n)) reductions. If control state reachability for S-automata is complete C (under DSPACE(log(n))-reductions), then N-aux-SPACE(log(n))− S-L= C.
Proof. Assume that A is a nondeterministic auxiliary SPACE(log(n))S automaton accepting some language L. Then L ∈ C because Lemma 23 provides a DSPACE(log(n))-reduction from L to control state reachability for S-automata which is in C by assumption. Thus, we conclude that N-aux-SPACE(log(n))−S-L⊆ C.
Now let L be some language in C. There is a DSPACE(log(n))-reduction ϕ such that for all words w, ϕ(w) is an encoding of a nondeterministic S-automaton A and a state q such that q is reachable in A if and only if w ∈ L. Due to Lemma 22, there is a DSPACE(log(n))-reduction ψ and a nondeterministic auxiliary SPACE(log(n))S-automaton A ′ such that A ′ accepts ψ(ϕ(w)) if and only if q is reachable in A if and only if w ∈ L. Recall that logspace reducibility is a transitive relation because the i-th symbol of a logspace reduction can be recomputed on the fly in logspace. Using the very same trick, we can define a nondeterministic auxiliary SPACE(log(n))S-automaton A ′′ that, given the input w simulates a run of A ′ on ψ(ϕ(w)). Hence, A ′′ accepts w if and only if w ∈ L. This shows that L ∈ N-aux-SPACE(log(n)) − S-L. ⊓ ⊔ The previous two lemmas directly imply Proposition 15. As a corollary of this proposition, our results on reachability for higher-order counters imply the language separations stated in Corollary 16. Moreover, if Proposition 15 separates the languages of S 1 -automata from those of S 2 -automata, then VAL(S 2 ) is an example language that separates the two classes.
Recall that the languages of auxiliary SPACE(log(n))P k−1 (P) are exactly those in DTIME( d∈N exp k−1 (n d )) (cf. [7]), -the languages of auxiliary SPACE(log(n))P k−1 (Z+) are exactly those in DSPACE( d∈N exp k−2 (n d )) due to Theorem 14 and Lemmas 22 and 23, -the languages of auxiliary SPACE(log(n))P k−1 (Z) are exactly those in DTIME( d∈N exp k−2 (n d )) due to Theorem 13 and Lemmas 22 and 23.

⊓ ⊔
Correspondingly, VAL(P k+1 ) is a (collapsible) higher-order pushdown language of level k + 1 recognised by a deterministic automaton with 1 state and no ε-transitions which is not recognised by any (collapsible) higher-order pushdown automaton of level k.

E Comparing Notions of Regularity
In this section, we compare the expressive power and succinctness of different notions of regularity for sets of configurations of P(Z) automata. Recall that we introduced in Section 3.2 a notion of regularity via the encoding in binary trees. From now on we write E-regularity for this notion.

E.1 2-Store Alternating Finite Automata
We will first compare E-regularity with the notion of regularity via 2-store alternating finite automata [2]. Since we introduce E only for P(Z) configurations, we restrict our presentation of 2-store automata also to this setting. Nevertheless the ideas presented here have straightforward extensions to the general setting of P(P) configurations.
Definition 35. Let A ′ be a P(Z) automaton with state set Q ′ . An alternating 2-store automaton A (with respect to A ′ ) is an alternating automata A = (Q, ρ, F, Σ, ∆) where Q ′ ⊆ Q is a finite set of states, ρ : Q → {∃, ∀} splits Q into existential and universal states, F ⊆ Q the set of final states, Σ ⊆ {0, 1, ⊥} × A a set of transition labels such that A is a finite set of alternating finite automata over input alphabet {⊥}, and ∆ ⊆ Q × Σ × Q An accepting computation of A on a P(Z) configuration is defined inductively. Let x = x ′ (τ, m) with x ′ ∈ ({0, 1, ⊥} × N) * , τ ∈ {0, 1, ⊥}, and m ∈ N, and let q ∈ Q be a state. There is an accepting computation from q on x if one of the following holds.
For x a P(Z)-configuration and q ∈ Q a state of A ′ , we say A accepts (q, x) if there is an accepting computation of A from q on x.
We call a set C of configurations of a P(Z) automaton 2-store-regular if there is a 2-store automaton that accepts (q, x) if and only if (q, x) ∈ C.
Remark 36. It is not difficult to adapt the usual powerset construction in order to obtain a deterministic 2-store automaton A ′ equivalent to a given alternating 2-store automaton. By deterministic, we mean that for any state q and any pushdown symbol τ ∈ {0, 1, ⊥} there is exactly one deterministic automaton B and one state q ′ such that (q, (τ, B), q ′ ) is a transition of A. Of course this determinisation comes at the price of a blow-up of the state set.
Note that 2-store automata process the counter values stored in a P(Z) configuration sequentially. Thus, these automata cannot compare the values of different counters stored in the pushdown. To the contrary, in the tree-encoding of a configuration two adjacent counter values can be compared by just looking at the position where the two corresponding branches split up. Thus, we can define E-regular sets whose members satisfy certain restrictions with respect to the comparison of adjacent counter values. This idea can be translated into a proof that there is a E-regular set which is not 2-store-regular. After giving this proof, we show that 2-store-regular sets are always E-regular. These two results show that the expressive power of 2-store-regularity is strictly weaker than that of E-regularity.
Proposition 37. There is a set C of configurations such that C is E-regular but not 2-store regular.
C is clearly E-regular because E(C) contains a tree T if and only if there is some m such that the only leaves of T are 0 m+1 and 0 m 10. It is straightforward to design a tree-automaton for this set of trees.
Heading for a contradiction, assume that C is accepted by some alternating 2-store automaton A. There are two numbers m 0 = m 1 such that the accepting runs of A on (q, (⊥, m 0 )(⊥, m 0 )) and (q, (⊥, m 1 )(⊥, m 1 )) use the same transitions of A. In particular, both computations spawn the same alternating finite automata A 1 , . . . , A m to accept ⊥ m0 or ⊥ m1 , respectively. But then A also accepts (q, (⊥, m 0 )(⊥, m 1 )) / ∈ C which is a contradiction.
Lemma 38. Let C be a 2-store-regular set. Then C is E-regular.
Proof. Let A be a 2-store automaton that recognises C. As explained in Remark 36, we may assume that A is deterministic. Let B 1 , . . . , B n be the deterministic finite automata appearing in the transition labels of A. Assume that B is the product automaton of B 1 , . . . , B n and assume that the state sets of all B i are pairwise disjoint. A tree-automaton accepting E(C) works as follows. It basically simulates all the B k in parallel along all branches. Moreover, at every branching point of the tree it guesses the transition of A that connects the element of the pushdown encoded in the rightmost branch of the left subtree with the leftmost branch of the right subtree. The precise procedure is as follows. Let c := (q, (τ 1 , c 1 ) . . . (τ n , c m )). For each node d of E(c) the subtree of nodes comparable to d encodes some subpart (q, (τ i , c i ) . . . (τ j , c j )) for 1 ≤ i ≤ j ≤ m. An accepting run on E(c) will label this node d with a tuple (q, p, r, s) where q, s are states of A, p a state of B and r a state of some B k (1 ≤ k ≤ n) such that there is a run of A from state q to state s on (τ i , c i ) . . . (τ j , c j ) such that the first transition of this run spawns a copy of B k along the word ⊥ ci . This labelling is carried out in such a way that the labels of different nodes are compatible in the sense that the runs witnessed by the labels can be composed to an accepting run of A on c.
For this purpose, the left successor of the root is labelled by L 0 := (q 0 , p 0 , r 0 , s 0 ) where q 0 = q, s 0 is a final state of A, p 0 is the initial state of some B k and r 0 is the initial state of B. Now the states are propagated as follows: -If a node d with label L d = (q d , p d , r d , s d ) has only a left successor (which is not a leaf, i.e., the tree label of d0 is ⊥), then set L d0 := (q d , p d0 , r d0 , s d ) such that p d0 is the unique state such that Similarly r d0 is the successor of r d with respect to B. -If a node d with label L d = (q d , p d , r d , s d ) has a left successor (which is not a leaf, i.e., the tree label of d0 is ⊥) and a right successor, then set L d0 := (q d , p d0 , r d0 , s d0 ) and L d1 := (s d0 , p d1 , r d , s d ) such that the following holds. p d0 is the unique state such that (p d , ⊥, p d0 ) is a transition of B k . Similarly r d0 is the successor of r d with respect to B. s d0 is some state of A and p d1 is one of the components of r d , i.e., a state of one of the B k ′ as simulated by B up to this position. -If the left successor of d is a leaf, and d's label is L d = (q d , p d , r d , s d ) then we first compute L d0 and (if necessary) L d1 as in the steps before. If the right successor exists, it is labelled by L d1 , the left successor is labelled by an accepting state if p d is an accepting state of B k such that (q d , (τ, B k ), s d0 ) is a transition of A where τ denotes the tree-label of the leaf at d0.
It is tedious but straightforward to prove that this tree-automaton accepts an encoding of a configuration if and only if it is in C. By taking a product with a tree-automaton recognising only valid encodings of configurations the claim is proved.
Unfortunately, the previous result that E-regularity is more expressive that 2-store-regularity does not imply that our result on the backwards or forward reachability carries over to 2-store-regular sets of configurations. The translation from the previous proof causes a blow-up of the state spaces. In the next lemma, we show that this blow-up is inevitable even if we start with deterministic 2-store automata.
Lemma 39. There is a sequence (A n ) n∈N of deterministic 2-store automata such that there is no polynomial p and a sequence (B n ) n∈N of tree automata such that |B n | ≤ P (|A n |) and B n accepts the same language as A n (modulo translation with E. Proof. It is easy to design a deterministic 2-store multi-automaton A n that accepts a configuration (⊥, v 1 )(⊥, v 2 ) . . . This is the automaton that goes from q 1 to q 2 to . . . to q n+1 spawning in the i-th step an automaton checking the length of the input modulo p i . This automaton can be realised with n + 1 + Assume that there is a B n with less than 2 n many states accepting E(C) for C the configurations accepted by A n .
Set m := n i=1 p i . There is an accepting run of B n on T := E(q, (⊥, m)(⊥, m) . . . (⊥, m)) where the height of the encoded pushdown is n. Note that m > 2 n and the leaves of T are the nodes 0 m+1 , 0 m 10, 0 m 1 2 0, . . . , 0 m 1 n−1 0. Application of the pumping lemma for tree-automata yields that there is some 0 < k < m and a tree whose leaves are 0 k+1 , 0 k 10, 0 k 1 2 0, . . . 0 k 1 n−1 0 accepted by B n . But this tree encodes (q, (⊥, k)(⊥, k) . . . (⊥k)) where k is not divisible by all primes p 1 , . . . , p m . This contradicts the assumption that B n accepts E(c) if and only if A n accepts c.

E.2 Regularity via Sequences of Operations
Carayol [4] introduced a notion of regularity based on sequences of pushdown operations. He proved a normal form for this kind of regular sets which we present in the next definition. His notion also extends to higher-level pushdowns but for our purpose it suffices to restrict the presentation to sets of P(Z) configurations. In the following we write Reg(A) for the set of regular expressions over alphabet A and we write L(r) for the languages L ⊆ A * defined by some regular expression r ∈ Reg(A).
Definition 40. Let t, s ∈ Reg({⊥}) and σ ∈ {0, 1, ⊥}. Then we define a binary relation test(t)σs The main observation of this section is that the sets of sequence-regular sets are a strict subset of the set of tree-regular sets via E. For our proof we assume the reader to be familiar with pebble automata (cf. [C] for a survey). Moreover, we use the following results. Remark 43. We thank Mikołaj Bojańczyk for pointing out that the separating example can be easily adapted to be a set of trees T such that T = E(C) for a set of configurations C. Basically, one first translates the example into a set of unlabelled trees by encoding the labels as certain subtrees and then one adds the labels necessary to make the trees encodings of configurations.
Theorem 44. The following holds: -For each sequence-regular set C of configurations, C is E-regular.
-There is an E-regular set which is not sequence-regular.
Proof. In fact, if P is sequence-regular, then E(P ) is defined by a positive cutting caterpillar expression. This is due to the fact that the inorder traversal of E(c) for some configuration c visits the maximal paths in the order in which they appear as elements of the pushdown. Assume that P is described by r = n i=1 r i s i . We translate r by structural induction into a (positive cutting) caterpillar expression r ′ recognising E(P ). Since caterpillar expressions are closed under finite unions, it suffices to translate r i s i . Fix a P(Z) configuration c = (⊥, m 0 )(σ 1 , m 1 )(σ 2 , m 2 ) . . . (σ n , m n ) and let T = E(c). In order to check that c ∈ L(r i s i ) we first have to check that m 0 ∈ L(r i ). But this is equivalent to check that the leftmost branch of T is of the form m 0 ⊥. Thus, we modify r i to r ′ i by inserting a move to the left child before any letter occurring in r i and add a final move to the left child and a check that the leaf is labelled by ⊥.
Next we describe how to translate s i into a caterpillar expression s ′ i which leads to acceptance from the leftmost leaf of T if and only if c ∈ L(r i s i ) and the path to this leaf satisfies r ′ i . Recall that s i is a regular expression over relations e →. In order to satisfy s i , we need to find a sequence of relations In order to obtain the expression cp(e) for any relation e → we make a case distinction on the form of e.
-Assume that e = test(t)σs. In this case cp(e) first uses the nesting operator in order to spawn a subexpression t ′ where every occurrence of ⊥ in t is replaced by an arbitrary sequence of moves from a right successor to its parent and then one move from a left successor to a ⊥ labelled parent. Afterwards, the main expression checks that we are at a leaf that is a left child, we move to the parent, then to the right child and then as in the translation of r i we execute s along the leftmost branch of this subtree. Additionally, we check that the leaf of this leftmost branch is labelled by σ. -Assume that e = stest(t)σ. In this case cp(e) goes to the parent node until coming from a left child the node has a right child. Then it spawns a subexpression to the left child which evaluates s along the rightmost branch of this subtree. It also spawns a subexpression t ′ as in the previous case. Finally it goes to the right child and then to the left child. There it checks that this node is a leaf labelled σ.
Finally, when cp(e) reaches the rightmost leaf, it accepts the whole tree. Now using the expression cp(e) instead of e → in the s i we can translate r = n i=1 r i s i into r ′ = n i=1 r ′ i s ′ i and obtain a positive cutting caterpillar expression that recognises E(P ) for P the sequence-regular set we started with.
Remark 45. Similarly to our construction, it is easy to translate 2-store automata (after determinisation) into caterpillar expressions or sequence-regular expression. Thus, we have a strict hierarchy with respect to expressive power from 2-store-regularity via sequence-regularity to E-regularity.
As in the case of 2-store-regularity, sequence-regularity may provide more succinct descriptions of regular sets.
Lemma 46. There is a sequence of sequence-regular expressions r n of size polynomial in n such that there is no sequence of tree-automata A n of size polynomial in n such that A n recognises E(L(r n )) for each n ∈ N.
Proof. Let C be the set of configurations (q, (⊥, c 1 )(⊥, c 2 ) . . . (⊥, c n )) such that c 1 = c 2 = · · · = c n and c i is divisible by the i-th prime. It is straightforward to write down a sequence-regular expression of polynomial size in n that describes C: → is the identity function on all (⊥, ⊥ m ) such that m is divisible by the i-th prime (which basically amounts to spawning the test test((⊥ pi ) * )).
To the contrary, as we have seen in the proof of Lemma 39, a tree-automaton recognising E(C) needs at least 2 n many states.

F Comparison of Expressive Power
In the last decades several equivalent definitions of higher-order pushdowns were used. Each of these can be restricted to unary stack alphabets resulting in a priori different kinds of storage types that could be called higher-order counters. In the following we show that most of these variants lead to storage types that lead to equivalent notions of nondeterministic higher-order counter automata. Note that our definition of higher-order counters leads to the most expressive variant of deterministic higher-order counter automata among those that we consider in the following.
First we consider higher-order pushdowns where only level 1 pushdowns contain stack symbols. By this we mean that a level k pushdown is not a list of pairs of stack symbols and level k − 1 pushdowns but only a list of level k − 1 pushdowns. We will show that this definition is equivalent to our definition in the case of higher-order pushdowns (which is well-known and straightforward) as well as for higher-order counters with 0-test. For higher-order counters without 0-test, we do not know whether the two versions are equivalent. At least it is clear that our version can simulate the more restricted version without higher-level pushdown symbols. Thus, our upper bounds, in particular the polynomial time algorithm for reachability on level 2, carry over to this setting. In fact, a simple adaptation of Slaat's proof [17] that k-HOCA + can simulate (k − 1)-HOPA shows that nondeterministic (k − 1)-HOPA can be simulated by this restricted version of nondeterministic k-HOCA − the lower bounds also holds.
Finally, we also consider higher-order pushdown automata with inverse pushoperations (cf. [5,A]). In these systems the level k pop-operation is replaced by a restricted version which is only applicable if the two topmost level k − 1 pushdowns coincide. Carayol and Woehrle [5] have shown that this kind of higherorder pushdown storage is equivalent to the usual one for nondeterministic automata (see [A] for a proof). We show that this carries over to higher-order counters. In particular, even when we replace pop by the inverse push-operation and do not allow pushdown symbols on higher levels, the resulting nondeterministic higher-order counter automata with 0-test (without 0-test, respectively) is still equivalent to our notion of nondeterministic higher-order counter automata with 0-test (without 0-test, respectively). Some of these results carry over to deterministic automata as well. Before we go into the details we summarise our results in the following two theorems. We say S automata simulate S ′ automata if for each S ′ automaton there is a S automata recognising the same language and generating the same configuration graph after ε-contraction.
Theorem 47. The following holds: 1. For any of the following storage types the nondeterministic r-way automata of one type can simulate the nondeterministic r-way automata of another type for (r ∈ {1, 2}): -P k (P), i.e., level k pushdown automata with pushdown symbols on each level (Engelfriet's definition of level k pushdown automata), -Z k (P), i.e., level k pushdown automata with pushdown symbols only on level 1 (used for instance in [9]), -Z k inv (P), i.e., level k pushdown automata with pushdown symbols only on level 1 and inverse push operations (introduced in [5]), -P k inv (P), i.e., level k pushdown automata with pushdown symbols on each level and with inverse push operations. 2. The analogous statement for nondeterministic higher-order counter automata with 0-test also holds. For any of the following storage types the nondeterministic r-way automata of one type can simulate the nondeterministic r-way automata of another type (for r ∈ {1, 2}): -P k (Z+), i.e., level k counter automata (with 0-test) with pushdown symbols on each level, -Z k (Z+), i.e., level k counter automata (with 0-test) with pushdown symbols only on level 1, -Z k inv (Z+), i.e., level k counter automata (with 0-test) with pushdown symbols only on level 1 and inverse push operations, -P k inv (Z+), i.e., level k counter automata (with 0-test) with pushdown symbols on each level and with inverse push operations. 3. For nondeterministic higher-order counter automata without 0-test we can only prove a weaker result. For any of the following storage types the nondeterministic r-way automata of one type can simulate the nondeterministic r-way automata of another type (for r ∈ {1, 2}): -P k (Z), i.e., level k counter automata (without 0-test) with pushdown symbols on each level, -Z k inv (Z), i.e., level k counter automata (without 0-test) with pushdown symbols only on level 1 and inverse push operations, -P k inv (Z), i.e., level k counter automata (without 0-test) with pushdown symbols on each level and with inverse push operations. Moreover, nondeterministic Z k (Z) automata can be simulated by each of the above mentioned automata.
Remark 48. All results of this theorem carry over to alternating automata analogously. Moreover, we can also add an auxiliary tape of size SPACE(b(n)) for arbitrary function b.
1. For any of the following storage types the deterministic r-way automata of one type can simulate the deterministic r-way automata of another type (for r ∈ {1, 2}): -P k (P), i.e., level k pushdown automata with pushdown symbols on each level, -Z k (P), i.e., level k pushdown automata with pushdown symbols only on level 1, -P k inv (P), i.e., level k pushdown automata with pushdown symbols on each level and with inverse push operations. Moreover deterministic Z k inv (P) automata can be simulated by any of the above mentioned automata types. 2. The analogous statement for deterministic higher-order counter automata with 0-test also holds. For any of the following storage types the deterministic r-way automata of one type can simulate the deterministic r-way automata of another type (for r ∈ {1, 2}): -P k (Z+), i.e., level k counter automata (with 0-test) with pushdown symbols on each level, -Z k (Z+), i.e., level k counter automata (with 0-test) with pushdown symbols only on level 1, -P k inv (Z+), i.e., level k counter automata (with 0-test) with pushdown symbols on each level and with inverse push operations. Moreover deterministic Z k inv (Z+) automata can be simulated by any of the above mentioned automata types. 3. Deterministic P k (Z) automata can simulate deterministic P k inv (Z) automata and vice versa. Moreover, deterministic Z k inv (Z) automata and deterministic Z k (Z) automata are strictly weaker that P k (Z) automata in the sense that every automaton of one of the former types can be simulated by some automaton of the latter type but not vice versa.
Remark 50. The proof of this theorem will be based on Engelfriet's notion of equivalent storages. Thus, the statement remains valid, if we replace deterministic automata by any other kind of deterministic/nondeterministic/alternating r-way auxiliary SPACE(b(n)) automata. It even carries over to the corresponding classes of transducers.
We conclude the presentation of the results of this section by pointing the reader to the open problems concerning equivalence of storage types.
Problem 51. 1. Is there some nondeterministic P k (Z) automaton that cannot be simulated by any nondeterministic Z k (Z) automaton? 2. Can we determinise the storage simulations that we so far only realised nondeterministic? In other words, can deterministic Z k (S) automata be simulated by deterministic Z k inv (S) automata for S one storage type of the set {P, Z+, Z}?

F.1 Simulation of Deterministic Automata
We first prove our claims about the deterministic case. Note that the nontrivial claims of Theorem 49 will be proved in Propositions 54 and 56, and in Corollary 62. Let us first recall the notion of equivalence of storage types (cf. [7]).
Definition 52. Let S and S ′ be storages. S can simulate S ′ , denoted as S ′ S, if for every one-way deterministic S ′ transducer there is a one-way deterministic S transducer defining the same transductions.
S and S ′ are equivalent, denoted as S ≡ S ′ , if S S ′ and S ′ S.
Remark 53. As pointed out by Engelfriet, this notion of equivalence implies that if S S ′ , then for t ∈ {nondeterministic, alternating, deterministic}, r ∈ {1, 2}, the t r-way auxiliary SPACE(b(n)) S automata can be simulated by the t r-way auxiliary SPACE(b(n)) S' automata Recall that we defined the storage type Z = P {⊥} . In the following, we also use Z as the operator P {⊥} acting on other storage types. We call Z(S) the storage type counter of S. Apparently, the (first) ⊥ component of every entry in the elements of Z(S) is redundant. Identifying (⊥, c 1 )(⊥, c 2 ) . . . (⊥, c n ) with (c 1 )(c 2 ) . . . (c n ) one sees easily that Z k−1 (P) automata are equivalent to the higher-order pushdown automata variant (of level k) used for instance in [9].
2. The empty? test on level 1 is simulated by first determining which top γ test applies for γ ∈ {0, 1, ⊥} as in the simulation of top γ . Then we perform γ many pop-operations of level 1, then the empty? test of S ′ coincides with the empty? of S. We restore the pushdown by γ many push ⊥ operations of level 1. 3. A pop operation is simulated by pop. 4. A push γ,id operation is simulated by the following program: first determine the topmost symbol γ ′ ∈ {0, 1, ⊥} of x ′ . Then apply push ⊥,id , then apply γ ′ many level 1 pop-operations. No we apply γ many level 1 push ⊥ operations. 5. A stay f operations is simulated by stay f if f is not an operation of level 1.
If it is of level 1 we just duplicate it 3 times.
The equivalence P k (P) ≡ Z k (P) is obtained completely analogous.
We now want to discuss the variants of pushdown systems and counters with inverse push-operations. For reasons of simplicity, we now consider the operator P to be restricted to push σ,id , stay f and pop operations. Let P inv and Z inv be the variants of (the restricted) P and Z with inverse push-operations, i.e., P inv is defined as P but instead of the operation pop we have the operation push Carayol and Woehrle [5] already showed that nondeterministic Z k inv (P) automata can simulate nondeterministic Z k (P) automata and that Z k inv (P) Z k (P). The latter simulation uses the fact that for every Z k inv (P)-configuration there is a unique shortest sequence of operations that generates this configuration from the initial one. Moreover, a sequence s of operations translates one configuration x 1 into another configuration x 2 if and only if the following holds. Let s i be the unique sequence generating x i , then s 2 results from s 1 s by removing all adjacent pairs of inverse operations. Here, the inverse of push γ,id is push −1 γ and the inverse of level 1 push σ is pop σ and the inverse of stay f is stay f −1 where f −1 is the inverse of f (pop σ denotes a pop operation that is applied to a pushdown with topmost symbol σ). We next prove a similar result for P k inv (S) and P k (S) for S ∈ {P, Z, Z+} that even work deterministically in both directions.
Lemma 55. For all k ∈ N P inv (P k inv (S)) ≡ P(P k inv (S)) for S ∈ {P, Z, Z+}. Proof. We first show P inv (P k inv (S)) P(P k inv (S)). This proof adapts the one of [A] and uses the level k symbols on the pushdown to store the minimal sequence that generated the current pushdown. For this purpose we replace the operations on P inv (P k inv (S)) as follows.
Example 58. Z k (Z) and Z k inv (Z) are test-free whereas P is not test-free. In the following, we show that test-free storage types cannot deterministically compute any unbounded function f in the sense that the language L f := a n b f (n) | n ∈ N is not recognised by any deterministic S automaton where S is a test-free storage type. In particular, test-free deterministic S automata do not accept {a n b n | n ∈ N} whence Z+ S. The crucial observation is that the storage configuration has no influence on the next transition except for the fact that it can abort a computation.
Lemma 59. Let S be a test-free storage type and A a deterministic S automaton. For each input letter σ and all states q, the set of storage-configurations X splits into two disjoint sets X = X b ⊔ X t such that for all configurations (q, x) with x ∈ X b no transition is applicable to (q, x), and there is a unique state p and a unique S-operation o such that the unique successor configuration on reading ε or σ for each (q, x) with x ∈ X t is (p, o(x)).
By induction on the length of a run we obtain the following corollary.
Corollary 60. Let S be a test-free storage type and A a deterministic S automaton. For each state q there is a unique state p and a S-operation o such that for each configuration (q, x) that admits a run on σ k , the unique successor configuration after reading σ or ε is (p, o(x)). In particular, if (q, x) and (q, x ′ ) both allow a run reading σ k these runs both end in the same state p ′ .
Proposition 61. Let f : N → N be an unbounded function and S a test-free storage type. L f = a n b f (n) | n ∈ N is not recognised by any deterministic S automaton.
Proof. Since f is unbounded, there is a state q and numbers n 1 , n 2 ∈ N with f (n 1 ) < f (n 2 ) such that the run on a ni ends in (q, x i ) for storage configurations x 1 , x 2 of S. By assumption there is a run from (q, x 1 ) reading b f (n1) and ending in an accepting state p. Since (q, x 2 ) admits a run reading b f (n2) , it also a admits a run reading b f (n1) . Due to the previous corollary, this run ends in state p, whence a n2 b f (n1) is accepted. But this contradicts the fact that a n2 b f (n1) / ∈ L f because f (n 1 ) < f (n 2 ).

Corollary 62. Z+
S for any test-free storage type S. In particular, Z+ Z k (Z) and Z+ Z k inv (Z) for all k ∈ N. Proof. There is a deterministic Z+ automaton recognising L id = {a n b n | n ∈ N} which (by the previous proposition) is not recognised by any deterministic S automaton A.
Since obviously Z+ P k (Z) for all k ≥ 1, P k (Z) is not equivalent to Z k (Z) or Z k inv (Z). Corollary 63. Z k (Z) ≺ P k (Z) and Z k inv (Z) ≺ P k (Z) for all k ≥ 1.

F.2 Simulation of nondeterministic automata
We now define a 'nondeterministic' version of the notion of equivalence of storage types. This allows to prove those parts of Theorem 47 that are not already implied by the results from the previous section.
Definition 64. Let S = (X, T, F, x 0 ) and S ′ = (X ′ , T ′ , F ′ , x ′ 0 ) be storage types. We say S can be nondeterministically simulated by S ′ and write S N S ′ if there is a map ϕ : X → X ′ such that the following holds.
1. There is a sequence f 1 , f 2 , . . . , f n ∈ F ′ such that ϕ(x 0 ) = f 1 (f 2 (. . . f n (x ′ 0 ) . . . )). 2. For each f ∈ F there is a nondeterministic S ′ automaton A f with initial state q i and final state q f such that for all x ∈ X there is a run of A f from (q i , ϕ(x)) to (q f , y ′ ) if and only if f (x) is defined and y ′ = ϕ(f (x)). 3. For each t ∈ T there are two nondeterministic S ′ automaton A t ,Ā t with initial states q i andq i , and final states q f andq f , respectively, such that for all x ∈ X there is a run of A t from (q i , ϕ(x)) to (q f , y ′ ) if and only if t(x) = true and y ′ = ϕ(x), and for all x ∈ X there is a run ofĀ t from (q i , ϕ(x)) to (q f , y ′ ) if and only if t(x) = f alse and y ′ = ϕ(x).
As in the case of , we write S ≡ N S ′ if S N S ′ and S ′ N S.
Proposition 65. Let S N S ′ , b(n) : N → N, r ∈ {1, 2} and t ∈ {nondeterministic, alternating}. Every r-way t auxiliary SPACE(b(n)) S automaton A is simulated by some r-way t auxiliary SPACE(b(n)) S' automaton A ′ in the sense that the configuration graphs of A and A ′ coincide after ε-contraction and both automata accept the same language.
Proof. By a straightforward product construction of A and the (A f ) f ∈F , (A t ) t∈T and (Ā t ) t∈T . Instead of executing S-tests or -operations the automaton guesses the correct test result and then checks its guess and simulates the operation by executing first the corresponding A t /Ā t and the the corresponding A f from its initial to its final state.
As in the deterministic case, the pushdown operator is monotone with respect to N .
Proposition 66. Let S N S ′ . We have P(S) N P(S ′ ), P inv (S) N P inv (S ′ ), Z(S) N Z(S ′ ), Z inv (S) N Z inv (S ′ ), Proof. It suffices to provide simulations of the test test(t) for each test t of S and simulations for the operations stay f (note that push γ,f can be replaced by push γ,id ; stay f ).
The automaton A test(t) that checks that test(t) = true is equal to A t but executes test test(t ′ ) whenever A t executes t ′ and performs stay f ′ whenever A t performs S ′ -operation f ′ . Analogously we defineĀ test(t) and A stay f . Note that all storage types S = (X, T, F, x 0 ) we consider are strongly connected in the sense that for any x, x ′ ∈ X there is a sequence f 1 , f 2 , . . . , f n of S-operations such that x ′ = f 1 (f 2 (. . . f n (x) . . . )). As Carayol and Woehrle already noticed, pop of P(S) can be simulated nondeterministically by inverse push of P inv (S) if S is strongly connected by simply guessing the right S configuration and restoring it before simulating the pop by an inverse push.
Lemma 67. For strongly connected storage types S, Z(S) N Z inv (S). Moreover, these storage types are again strongly connected.
Induction on the previous lemma directly yields the following proposition.
Proposition 68. For k ∈ N and S ∈ {P, Z+, Z} we have Z k (S) N Z k inv (S). Proof. Inductively, Z k (S) N Z(Z k−1 inv (S)) N Z inv (Z k−1 inv (S)) = Z k inv (S). The last claim we have to prove is that Z k inv (Z) ≡ N P k inv (Z). Again we first prepare the proof by induction with a simple lemma.
Lemma 69. P inv (Z k−1 inv (Z)) ≡ N Z inv (Z k−1 inv (Z)) for all k ≥ 1. Proof. The N direction is trivial. For the other direction, we first do the case k = 1 and then the case k ≥ 2.
A P inv (Z) configuration (σ 1 , m 1 ) . . . (σ n , m n ) is identified with the Z inv (Z) configuration (⊥, m 1 + σ 1 )(⊥, m 1 )(⊥, m 2 + σ 2 )(⊥, m 2 ) . . . (⊥, m n + σ n )(⊥, m n ) (where we again identify ⊥ with 2). In this representation a test for the topmost symbol is simple: the topmost symbol is σ if we can apply stay push ⊥ σ many times follows by inverse push, push and σ many stay pop operations. The corresponding negative test is by guessing the symbol τ ∈ {⊥, 0, 1} \ {σ} and applying the positive test for τ . With the ability to test for the encoded topmost symbol, it is then easy to simulate any of the P inv (Z) operations.
For the case k ≥ 3 we use basically the same idea but we have to take care that we only encode one topmost symbol in the topmost level k − 1 counter. For this purpose we define an auxiliary notation let σ ∈ {0, 1, ⊥}, and m a Z k−1 inv (Z) configuration. We write m + σ for the result of applying to m the level 2 operation push ⊥,id followed by the level 1 push ⊥ for σ many times (level n means that we put the mentioned operation into a (k − n)-fold application of stay). We then encode a P inv (Z k−1 inv (Z)) configuration (σ 1 , m 1 ) . . . (σ n , m n ) as the Z k inv (Z) configuration (⊥, m 1 + σ 1 ) . . . (⊥, m n + σ n ). Simulation is now carried out similar to the case k = 2. The simulation of the test top σ is by doing the right number of level 1 pop operations followed by a inverse push of level 2 and then again restoring the initial storage configuration. If we want to apply a storage operation (different from push σ,id and push −1 σ ) to (⊥, m 1 + σ 1 ) . . . (⊥, m n + σ n ), we first restore the configuration (⊥, m 1 + σ 1 ) . . . (⊥, m n ) then apply the configuration and afterwards restore the encoding of σ n . For the push σ,id we just apply push ⊥,id and subsequently replace the topmost m n + σ n by m n + σ. For the inverse push, we first have to guess σ n−1 , replace m n + σ n by m n + σ n−1 and then apply the inverse push.
Again it is straightforward to prove that this simulation is correct.