C-SHORe: Higher-Order Verification via Collapsible Pushdown System Saturation

TL;DR

C-SHORe introduces a scalable, automata-theoretic model-checking approach for higher-order recursion schemes using collapsible pushdown systems, enhancing verification efficiency and providing counter-examples.

Contribution

It presents the first practical model-checking algorithm for CPDS, integrating backward saturation, forward guidance, pruning, and counter-example extraction.

Findings

Effective backward saturation algorithm for CPDS

Guided model-checking using forward reachability information

Competitive performance compared to state-of-the-art tools

Abstract

Higher-order recursion schemes (HORS) have received much attention as a useful abstraction of higher-order functional programs with a number of new verification techniques employing HORS model-checking as their centrepiece. We give an account of the C-SHORe tool, which contributed to the ongoing quest for a truly scalable model-checker for HORS by offering a different, automata theoretic perspective. C-SHORe implements the first practical model-checking algorithm that acts on a generalisation of pushdown automata equi-expressive with HORS called collapsible pushdown systems (CPDS). At its core is a backwards saturation algorithm for CPDS. Additionally, it is able to use information gathered from an approximate forward reachability analysis to guide its backward search. Moreover, it uses an algorithm that prunes the CPDS prior to model-checking and a method for extracting counter-examples in negative instances. We provide an up-to-date comparison of C-SHORe with the state-of-the-art verification tools for HORS. The tool and additional material are available from http://cshore.cs.rhul.ac.uk.

Equations

$$N\varphi x\hookrightarrow t$$

$$\begin{array}[]{rcl}main&\hookrightarrow&M\ nil\\ M\ x&\hookrightarrow&or\ (commit\ x)\ (A\ x\ M)\\ A\ y\ \phi&\hookrightarrow&or\ (\phi\ error)\ (\phi\ (cons\ y))\end{array}$$

$$[[[\text{rnode}aa\text{rnode}bb\text{pnode}(0.0pt,0.0pt)d2{]}_1{]}_2\text{pnode}(0.0pt,0.0pt)d1[[\text{rnode}cc{]}_1\text{pnode}(0.0pt,0.0pt)d3[\text{rnode}dd\text{pnode}(0.0pt,0.0pt)d4\text{rnode}ee\text{pnode}(0.0pt,0.0pt)d5{]}_1{]}_2{]}_3.$$

$$\begin{array}[]{rcll}{top_{n}}\mathord{\left({[{w_{1}\ldots w_{\ell}}]_{n}}\right)}&=&w_{1}&\text{when $\ell>0$}\\ {top_{k}}\mathord{\left({[{w_{1}\ldots w_{\ell}}]_{n}}\right)}&=&{top_{k}}\mathord{\left({w_{1}}\right)}&\text{when $k<n$ and $\ell>0$}\end{array}$$

$$\begin{array}[]{rcll}{bot^{i}_{n}}\mathord{\left({[{w_{1}\ldots w_{\ell}}]_{n}}\right)}&=&[{w_{\ell-i+1}\ldots w_{\ell}}]_{n}&\text{when $i\leq\ell$}\\ {bot^{i}_{k}}\mathord{\left({[{w_{1}\ldots w_{\ell}}]_{n}}\right)}&=&[{{bot^{i}_{k}}\mathord{\left({w_{1}}\right)}w_{2}\ldots w_{\ell}}]_{n}&\text{when $k<n$ and $\ell>0$}\ .\end{array}$$

$$\begin{array}[]{rcll}{u}:_{k}{v}&=&[{uv_{1}\ldots v_{\ell}}]_{n}&\text{when $k=n$}\\ {u}:_{k}{v}&=&[{({u}:_{k}{v_{1}})v_{2}\ldots v_{\ell}}]_{n}&\text{when $k<n$ and $\ell>0$}\\ \end{array}$$

$$\begin{array}[]{rcl}\mathcal{O}_{n}&=&\left\{{pop_{1},\ldots,pop_{n}}\right\}\cup\left\{{push_{2},\ldots,push_{n}}\right\}\ \cup\\ &&\left\{{collapse_{2},\ldots,collapse_{n}}\right\}\cup\left\{{push^{2}_{a},\ldots,push^{n}_{a},rew_{a}}\ \left|\ {a\in\Sigma}\right.\right\}\end{array}$$

$$\begin{array}[]{rcl}{\rm Phys.~{}Rev.~{}E}{0}{\mathcal{C}}{C_{f}}&=&C_{f}\\ {\rm Phys.~{}Rev.~{}E}{\alpha+1}{\mathcal{C}}{C_{f}}&=&\left\{{\langle{p},{w}\rangle}\ \left|\ {\begin{array}[]{l}\exists\langle{p},{w}\rangle\longrightarrow\langle{p^{\prime}},{w^{\prime}}\rangle\in{\rm Phys.~{}Rev.~{}E}{\alpha}{\mathcal{C}}{C_{f}}\ \lor\\ \exists\langle{p},{w}\rangle\longrightarrow C\subseteq{\rm Phys.~{}Rev.~{}E}{\alpha}{\mathcal{C}}{C_{f}}\end{array}}\right.\right\}\cup{\rm Phys.~{}Rev.~{}E}{\alpha}{\mathcal{C}}{C_{f}}\ .\end{array}$$

$$A=\left({\mathbb{Q}}_n,\dots ,{\mathbb{Q}}_1,\Sigma ,{\Delta }_n,\dots ,{\Delta }_1,{\mathcal{F}}_n,\dots ,{\mathcal{F}}_1\right)$$

$$q\stackrel{q}{\to }\left(\right).$$

$$Q\underset{Q_{col}}{\overset{a}{\to }}\left(Q_1,\dots ,Q_k\right)$$

$${\mathrm{Top}}_1\left(\tau \right)=t$$

$$A=\left({\mathbb{Q}}_n,\dots ,{\mathbb{Q}}_1,\Sigma ,{\Delta }_n,\dots ,{\Delta }_1,{\mathcal{F}}_n,\dots ,{\mathcal{F}}_1\right).$$

$$\begin{array}[]{rcl}{\mathrm{Proj}}\mathord{\left({{\left({a,T}\right)}^{\left({k,i}\right)}}\right)}&=&{a}^{\left({k,i}\right)},\text{\ and}\\ {\mathrm{Proj}}\mathord{\left({{w}:_{k}{w^{\prime}}}\right)}&=&{{\mathrm{Proj}}\mathord{\left({w}\right)}}:_{k}{{\mathrm{Proj}}\mathord{\left({w^{\prime}}\right)}}\ .\end{array}$$

$$[[\left(a,\left\{t_1^{\prime }\right\}\right){]}_1[\left(b,\left\{t_2^{\prime }\right\}\right){]}_1[\left(c,\left\{t_3^{\prime }\right\}\right){]}_1{]}_2.$$

$$A=\left({\mathbb{Q}}_n,\dots ,{\mathbb{Q}}_1,\Sigma ,{\Delta }_n,\dots ,{\Delta }_1,{\mathcal{F}}_n,\dots ,{\mathcal{F}}_1\right).$$

$$\begin{array}[]{rcl}{\mathrm{Contained}}\mathord{\left({{\left({a,T}\right)}^{\left({k,i}\right)},{\left({a,T^{\prime}}\right)}^{\left({k,i}\right)}}\right)}&\iff&T\subseteq T^{\prime}\\ {\mathrm{Contained}}\mathord{\left({{u^{\prime}}:_{k}{u^{\prime\prime}},{v^{\prime}}:_{k}{v^{\prime\prime}}}\right)}&\iff&{\mathrm{Contained}}\mathord{\left({u^{\prime},u^{\prime\prime}}\right)}\land{\mathrm{Contained}}\mathord{\left({v^{\prime},v^{\prime\prime}}\right)}\ .\end{array}$$

$$\tau =\left(q_p\underset{\varnothing }{\overset{a}{\to }}\left(\varnothing ,\dots ,\varnothing ,\left\{q_k\right\},Q_{k+1},\dots ,Q_n\right)\right)$$

$$\tau^{\prime}=\left({{q_{p}}\xrightarrow[Q_{col}\cup Q^{\prime}_{col}]{a}\left({{\begin{array}[]{c}Q_{1}\cup Q^{\prime}_{1},\ldots,Q_{k-1}\cup Q^{\prime}_{k-1},\\ Q^{\prime}_{k},\\ Q_{k+1},\ldots,Q_{n}\end{array}}}\right)}\right)$$

$${\tau }^{\prime }=\left(q_p\underset{Q_{col}^{\prime }}{\overset{a}{\to }}\left(Q_1^{\prime },Q_2,\dots ,Q_k\cup Q_{col},\dots ,Q_n\right)\right),$$

$$\begin{gathered} ⟨p_1,[[b{]}_1[c{]}_1[d{]}_1{]}_2⟩\stackrel{pus{h}_a^2}{\to }⟨p_2,[[\text{rnode}A1ab{]}_1\text{pnode}(0.0pt,0.0pt)S1[c{]}_1[d{]}_1{]}_2⟩\stackrel{pus{h}_2}{\to }⟨p_3,[[\text{rnode}A2ab{]}_1[\text{rnode}A22ab{]}_1\text{pnode}(0.0pt,0.0pt)S2[c{]}_1[d{]}_1{]}_2⟩ \\ \stackrel{collaps{e}_2}{\to }⟨p_4,[[c{]}_1[d{]}_1{]}_2⟩\stackrel{po{p}_2}{\to }⟨p_5,[[d{]}_1{]}_2⟩. \end{gathered}$$

Full text

1. Introduction

Functional languages such as Haskell, OCaML and Scala strongly encourage the use of higher-order functions. This represents a challenge for software verification, which usually does not model recursion accurately, or models only first-order calls (e.g. SLAM [BR02] and Moped [S02]). However, there has recently been much interest in a model called higher-order recursion schemes (HORS) (see e.g. [O06]), which offers a way of abstracting functional programs in a manner that precisely models higher-order control-flow.

The execution trees of HORS enjoy decidable $\mu$-calculus theories [O06]. Even ‘reachability’ properties (subsumed by the $\mu$-calculus) are very useful in practice. As a simple example, the safety of incomplete pattern matching clauses could be checked by asking whether the program can ‘reach a state’ where a pattern match failure occurs. More complex ‘reachability’ properties can be expressed using a finite automaton and could, for example, specify that the program respects a certain discipline when accessing a particular resource (see [K09]). Despite even reachability being $(n-1)$-EXPTIME complete, recent research has revealed that useful properties of HORS can be checked in practice.

Kobayashi’s TRecS [K09b] tool, which checks properties expressible by a deterministic trivial Büchi automaton (all states accepting), was the first to achieve this. It works by determining whether a HORS is typable in an intersection-type system characterising the property to be checked [K09]. In a bid to improve scalability, a number of other algorithms have subsequently been designed and implemented such as Kobayashi et al.’s GTRecS(2) [K11b, gtrecs2] and Neatherway et al.’s TravMC [NRO12] tools, all based on intersection type inference. A recent overview of HORS model-checking was given by Ong [O15].

This work is the basis of various techniques for verifying functional programs. In particular, Kobayashi*et al.*have developed MoCHi [KSU11] that checks safety properties of (OCaML) programs, and EHMTT Verifier [Unno10APLAS] for tree processing programs. Both use a recursion schemes model-checker as a central component. Similarly, Ong and Ramsay [OR11] analyse programs with pattern matching employing recursion schemes as an abstraction.

Achieving scalability while accurately tracking higher-order control-flow is a challenging problem. This article offers an automata-theoretic perspective on this challenge, providing a fresh set of tools that contrast with previous intersection-type approaches.

Collapsible pushdown systems (CPDS) [HMOS08, HMOS17] are an alternative representation of the class of execution trees that can be generated by recursion schemes (with linear-time mutual-translations between the two formalisms [HMOS08, HMOS17, CS12]). While pushdown systems augment a finite-state machine with a stack and provide an ideal model for first-order programs [JM77], collapsible pushdown systems model higher-order programs by extending the stack of a pushdown system to a nested “stack-of-stacks” structure. The nested stack structure enables one to represent closures. Indeed the reader might find it helpful to view a CPDS as being a Krivine’s Abstract Machine in a guise making it amenable to the generalisation of techniques for pushdown model-checking. Salvati and Walukiewicz have studied in detail the connection with the Krivine abstract machine [SW12, SW16].

For ordinary (‘order-$1$’) pushdown systems, a model-checking approach called saturation has been successfully implemented by tools such as Moped [S02] and PDSolver [HO10b]. Given a regular set of configurations of the pushdown system (represented by a finite automaton $A$ acting on stacks), saturation can solve the ‘backward reachability problem’ by computing another finite automaton recognising a set of configurations from which a configuration in $\mathcal{\mathcal{L}}(A)$ can be reached. This is a fixed-point computation that gradually adds transitions to $A$ until it is ‘saturated’. If $A$ recognises a set of error configurations, one can determine whether the pushdown system is ‘safe’ by checking if its initial configuration is recognised by the automaton computed by saturation.

The first contribution of this article was first presented in ICALP 2012. We extend the saturation method to a backward reachability analysis of collapsible pushdown systems [BCHS12]. This runs in PTIME when the number of control states is bounded. Crucially, this condition is satisfied when translating from recursion schemes of bounded arity with properties represented by automata of bounded size [HMOS08, HMOS17]. Whilst the HORS/intersection-type based tool GTRecS(2) also enjoys this fixed-parameter tractability, it times out on many benchmarks that our tool solves quickly. We remark also Ramsay*et al.*introduced a third fixed-parameter tractable algorithm in 2014 underlying their tool [RNO14].

In this work, we revisited the foundations of higher-order verification tools and introduced C-SHORe [cshore] — the first model-checking tool for the (direct) analysis of collapsible pushdown systems. This work was presented in ICFP 2013 [BCHS13]. To achieve an efficient implementation, some substantial modifications and additions were made to the algorithm, leading to several novel practical and theoretical contributions:

1. (1)

An approximate forward reachability algorithm providing data

1. (a)

…allowing the CPDS to be pruned so that saturation receives a smaller input. 2. (b)

…employed by a modified saturation algorithm to guide its backward search.

This is essential for termination on most of our benchmarks. 2. (2)

A method for extracting witnesses to reachability. 3. (3)

A complete rework of the saturation algorithm to speed up fixed-point computation. 4. (4)

Experimental results comparing our approach with other tools.

We remark that the tools mentioned above propagate information forwards WRT the evaluation of the model. In contrast, the raw saturation algorithm works backwards, but we also show how forward and backward propagation can be combined.

Here we give a full account of the C-SHORe tool. This covers the saturation algorithm presented at ICALP 2012 as well as efficient algorithms implemented by C-SHORe in ICFP 2013. To prove soundness, we diverge from the ICALP 2012 proof, and instead base our proof on the witness generation algorithm presented in ICFP 2013. In particular, we present novel generalisations of witness generation, the forwards analysis, and the efficient fixed-point calculation to alternating CPDSs. These were only given for non-alternating CPDSs in ICFP 2013. The tool is available at http://cshore.cs.rhul.ac.uk.

Since C-SHORe was released, two new tools were released. Broadbent*et al.introduced HorSat, which is an application of the saturation technique and initial forward analysis directly to intersection type analysis of HORS [BK13]. Recently HorSat2 improved the forwards analysis and made other algorithmic improvements [horsat2]. Secondly, in POPL 2014, Ramsayet al.*introduced  [RNO14]. This is a type-based abstraction-refinement algorithm that attempts to simultaneously prove and disprove the property of interest. Both HorSat2 and perform significantly better than previous tools.

Even though both and HorSat2 both outperform C-SHORe, we consider the CPDS approach to offer a different perspective by providing a link between successful pushdown model-checking tools and higher-order model-checking. Moreover, CPDS have been instrumental in proving a number of results about higher-order languages. Hence, it is very natural to consider the implementation of a model-checker using these automata techniques and the challenges and opportunities therein. This article provides an account of a significant effort to extend pushdown model-checking to the higher-order case, and therefore we hope it will be instructive to readers interested in building verification tools for higher-order programming languages.

Section 2 is an informal introduction to HORS and CPDS. In Section 3 we describe CPDS and how to represent sets of their configurations. The basic saturation algorithm introduced in ICALP 2012 is presented in Section 4 and proven correct in Section 5. Section LABEL:sec:counter-egs gives our generalised witness generation algorithm (that also implies soundness of saturation). We describe two optimisations to the saturation algorithm used by C-SHORe: an initial forwards analysis in Section LABEL:section:optimisations and an efficient fixed point computation in Section LABEL:sec:fastalgorithm. Experimental results are in Section LABEL:sec:experiments.

2. Modelling Higher-Order Programs

In this section we give an informal introduction to the process of modelling higher-order programs for verification. In particular, we show how a simple example program can be modelled using a higher-order recursion scheme, and then we show how this scheme is evaluated using a collapsible pushdown system. For a more systematic approach to modelling higher-order programs with recursion schemes, we refer the reader to work by Kobayashiet al. [KSU11]. This section is for background only, and can be safely skipped.

For this section, consider the toy example below.

Main = MakeReport Nil MakeReport x = if * (Commit x) else (AddData x MakeReport) AddData y f = if * (f Error) else (f Cons(_, y))

In this example, * represents a non-deterministic choice (that may, for example, be a result of some input by the user). Execution begins at Main which aims to make a report which is a list. It sends an empty report to MakeReport. Either MakeReport finishes and commits the report somehow, or it adds an item to the head of the list using AddData, which takes the report so far, and a continuation. AddData either detects a problem with the new data (maybe it is inconsistent with the rest of the report) and flags an error by passing Error to the continuation, or extends the report with some item. In this case, since there is no error handling in MakeReport, an Error may be committed.

2.1. Higher-Order Recursion Schemes

We introduce, informally, higher-order recursion schemes. These are rewrite systems that generate the computation tree of a functional program. A rewrite rule takes the form

[TABLE]

where $N$ is a (simply) typed non-terminal with (possibly higher-order) arguments $\phi$ and $x$. A term $N\ t_{\phi}\ t_{x}$ rewrites to $t$ with $t_{\phi}$ substituted for $\phi$ and $t_{x}$ substituted for $x$. Note that recursion schemes require $t$ to be of ground type. We illustrate recursion schemes and their use in analysis using the toy example from above. We can directly model our example with the scheme

[TABLE]

where $M$ is the non-terminal associated with the MakeReport function, and $A$ is the non-terminal associated with the AddData function; $nil$, $or$, $commit$, $error$ and $cons$ are terminal symbols of arity 0, 2, 1, 0 and 1 respectively (e.g. in the second rule, $or$ takes the two arguments $(commit\ x)$ and $(A\ x\ M)$). The scheme above begins with the non-terminal $main$ and, through a sequence of rewrite steps, generates a tree representation of the evolution of the program. Figure 1, described below, shows such a sequence.

Beginning with the non-terminal $main$, we apply the first rewrite rule to obtain the tree representing the term $(M\ nil)$. We then apply the second rewrite rule, instantiating $x$ with $nil$ to obtain the next tree in the sequence. This continues ad infinitum to produce a possibly infinite tree labelled only by terminals.

We aim to show the correctness of the program. I.e. the program never tries to $commit$ an $error$. The rightmost tree in Figure 1, has a branch labelled $or,or,or,commit,error$. Note, $commit$ is being called with an $error$ report. In general we define the regular language $\mathcal{L}_{err}=or^{\ast}commit\ or^{\ast}error$. If the tree generated by the HORS contains a branch labelled by a word appearing in $\mathcal{L}_{err}$, then we have identified an error in the program.

2.2. Collapsible Pushdown Automata

Previous research into the verification of HORS has used intersection types (e.g. [K11, NRO12]). Here we investigate a radically different approach exploiting the connection between HORS and an automata model called collapsible pushdown automata (CPDA). These two formalisms are, in fact, equivalent.

Theorem 1** (Equi-expressivity [HMOS08, HMOS17]).**

For each order-$n$ recursion scheme, there is an order-$n$ collapsible pushdown automaton generating the same tree, and vice-versa. Furthermore, the translation from recursion schemes to collapsible pushdown automata is linear, and the opposite translation is polynomial. ∎

We describe at a high level the structure of a CPDA and how they can be used to evaluate recursion schemes. In our case, this means outputting a sequence of non-terminals representing each path in the tree. More formal definitions are given in Section 3. At any moment, a CPDA is in a configuration $\langle{p},{w}\rangle$, where $p$ is a control state taken from a finite set $\mathcal{P}$, and $w$ is a higher-order collapsible stack. In the following we will focus on the stack. Control states are only needed to ensure that sequences of stack operations occur in the correct order and are thus elided for clarity.

In our toy example, we have an order-$2$ HORS and hence an order-$2$ stack. An order-$1$ stack is a stack of characters from a finite alphabet $\Sigma$. An order-$2$ stack is a stack of order-$1$ stacks. Thus $\left[{\left[{main}\right]}\right]$ denotes the order-$2$ stack containing only the order-$1$ stack $\left[{main}\right]$; $\left[{main}\right]$ is an order-$1$ stack containing only the character $main$. In general $\Sigma$ will contain all subterms appearing in the original statement of our toy example recursion scheme. The evolution of the CPDA stack is given in Figure 2 and explained below.

The first step is to rewrite $main$ using $main\hookrightarrow M\ nil$. Since $(M\ nil)$ is a subterm of our recursion scheme, we have $(M\ nil)\in\Sigma$ and we rewrite the stack $\left[{\left[{main}\right]}\right]$ to $\left[{\left[{M\ nil}\right]}\right]$. Next, we call $M$. As usual, a function call necessitates a new stack frame. In particular, we push the body of $M$ (that is $(or\ (commit\ x)\ (A\ x\ M))$) onto the stack, giving the third stack in Figure 2. Note, we do not instantiate the variable $x$, hence we use only the subterms appearing in the recursion scheme.

Recall that we want to obtain a CPDA that outputs a sequence of terminals representing each path in the tree. To evaluate $or\ (\cdots)\ (\cdots)$ we output the terminal $or$ and then (non-deterministically) choose a branch of the tree to follow. Let us choose $(A\ x\ M)$. Hence, the CPDA outputs $or$ and rewrites the top term to $(A\ x\ M)$. Next we call $A$, pushing its body to the stack, then pick out the $(\phi\ error)$ branch of the $or$ terminal. This takes us to the beginning of the second row of Figure 2.

To proceed, we evaluate $(\phi\ error)$. To do this, we have to know the value of $\phi$. We can obtain this information by inspecting the stack and seeing that the second argument of the call of $A$ is $M$. However, since we can only see the top of a stack, we would have to remove the character $(\phi\ error)$ to determine that $\phi=M$, thus losing our place in the computation.

However, an order-$2$ stack is able — via a $push_{2}$ operation — to create a copy of its topmost order-$1$ stack. After this copy (note that the top of the stack is written on the left) we delve into the copy of the stack to find the value of $\phi$. Simultaneously we create a collapse link, pictured as an arrow from $M$ to the stack with the term $(\phi\ error)$ on top. This collapse link points from $M$ to the context in which $M$ will be evaluated. In particular, if we need to know the value of $x$ in the body of $M$, we need to know that $M$ was called with the $error$ argument, within the term $(\phi\ error)$; the collapse link points to this information (i.e. encodes a closure in the stack). We can access this information via a collapse operation. These are the two main features of a higher-order collapsible stack, described formally in the next section.

To continue, we push the body of $M$ on to the stack, output the $or$ symbol and choose the $(commit\ x)$ branch. Since $commit$ is a terminal, we output it and evaluate $x$. To compute $x$, we look into the stack and follow the collapse link from $M$ to the stack with $(\phi\ error)$ on top. We do not create a copy of the stack here because $x$ is an order-[math] variable and thus represents a self-contained execution. Since $x$ has value $error$, we output it and terminate. This completes the execution corresponding to the error branch identified in Figure 1.

2.3. Collapsible Pushdown Systems

The CPDA output $or,or,or,commit,error$ in the execution above. This is an error sequence in $\mathcal{L}_{err}$ and should be flagged. In general, we take the finite automaton $A$ representing the regular language $\mathcal{L}_{err}$ and form a synchronised product with the CPDA. This results in a CPDA that does not output any symbols, but instead keeps in its control state the progression of $A$. Thus we are interested in whether the CPDA is able to reach an accepting state of $A$, not the language it generates. We call a CPDA without output symbols a collapsible pushdown system (CPDS), and the question of whether a CPDS can reach a given state is the reachability problem. This is the subject of the remainder of the paper.

3. Preliminaries

3.1. Collapsible Pushdown Systems

We give the definition of higher-order collapsible stacks and their operations, before giving the definition of collapsible pushdown systems.

3.1.1. Higher-Order Collapsible Stacks

Higher-order collapsible stacks are a nested “stack-of-stacks” structure over a stack alphabet $\Sigma$. Each stack character contains a pointer — called a “link” — to a position lower down in the stack. The stack operations, defined below, create copies of sub-stacks. The link is intuitively a pointer to the context in which the stack character was first created. These links will be defined as tuples, the meaning of which is expanded upon after the following definition. Let the natural numbers $\mathbb{N}$ be $\left\{{0,1,2,\ldots}\right\}$. We will write stacks with the top of the stack appearing on the left.

{defi}

[Order-$n$ Collapsible Stacks] An order-$k$ link is a tuple $\left({k,i}\right)$ where $k\geq 1$ and $i$ are natural numbers. If $k\in\left\{{1,\ldots,n}\right\}$ we say the link is up-to order-$n$. Given a finite set of stack characters $\Sigma$, an order-[math] stack with an up-to order-$n$ link is ${a}^{\left({k,i}\right)}$ where $a\in\Sigma$ and $\left({k,i}\right)$ is an up-to order-$n$ link. An order-$k$ stack with up-to order-$n$ links is a sequence $w=[{w_{1}\ldots w_{\ell}}]_{k}$ such that each $w_{j}$ is an order-$(k-1)$ stack with up-to order-$n$ links. Moreover, for each $w_{j}$ and each order-$k$ link $\left({k,i}\right)$ appearing on a character in $w_{j}$, we have $0\leq i\leq\ell-j$. Let ${Stacks_{n}}\mathord{\left({\Sigma}\right)}$ denote the set of order-$n$ stacks over $\Sigma$ with up-to order-$n$ links.

In the sequel we will refer to order-$n$ stacks with up-to order-$n$ links simply as order-$n$ stacks. We will use order-$k$ stack to mean an order-$k$ stack with up-to order-$n$ links, where $n$ is clear from the context. We define the interpretation of the collapse links formally below. Intuitively, the collapse links point to a position lower down in the stack. In a link $\left({k,i}\right)$ the first component $k$ indicates that the link points to a location inside the order-$k$ stack where the link is contained. The second component $i$ gives the distance from the bottom of the stack of the targeted position. For example, a link $\left({2,0}\right)$ in an order-$2$ stack $[{w_{1}\ldots w_{\ell}}]_{2}$ would point to the bottom of the order-$2$ stack. That is, after $w_{\ell}$. Hence, we can represent collapse links informally with arrows as shown below.

Example 3.1**.**

An example order-$3$ stack is $[{[{[{a^{\left({3,1}\right)}b^{\left({1,0}\right)}}]_{1}}]_{2}[{[{c^{\left({2,1}\right)}}]_{1}[{d^{\left({1,1}\right)}e^{\left({1,0}\right)}}]_{1}}]_{2}}]_{3}$ where the topmost character is $a$. This could be written

[TABLE]

The collapse operation, defined below, will remove all parts of the stack above the destination of the topmost collapse link. Collapse on the stack in the example above gives $[{[{[{c^{\left({2,1}\right)}}]_{1}[{d^{\left({1,1}\right)}e^{\left({1,0}\right)}}]_{1}}]_{2}}]_{3}$. Note, we will often omit the collapse link annotations for readability. In particular, we will often write ${top_{1}}\mathord{\left({w}\right)}=a$ instead of ${top_{1}}\mathord{\left({w}\right)}={a}^{\left({k,i}\right)}$ when we are not interested in the link.

Given an order-$n$ stack $[{w_{1}\ldots w_{\ell}}]_{n}$, we define

[TABLE]

noting that ${top_{k}}\mathord{\left({w}\right)}$ is undefined if ${top_{k^{\prime}}}\mathord{\left({w}\right)}$ is empty for any $k^{\prime}>k$. For technical reasons, we also define ${top_{n+1}}\mathord{\left({w}\right)}=[{w}]_{n+1}$ when $w$ is an order-$n$ stack. We remove the top portion of a $top_{k}$ stack using, where $i>0$,

[TABLE]

For ${top_{1}}\mathord{\left({w}\right)}={a}^{\left({k,i}\right)}$, the destination of the link is ${bot^{i}_{k}}\mathord{\left({w}\right)}$.

When $u$ is an order-$(k-1)$ stack and $v=[{v_{1}\ldots v_{\ell}}]_{n}$ is an $n$-stack with $k\leq n$, we define ${u}:_{k}{v}$ as the stack obtained by adding $u$ on top of the topmost $k$-stack of $v$. Formally, we let

[TABLE]

3.1.2. Operations on Order-$n$ Collapsible Stacks

The following operations may be performed on an order-$n$ collapsible stack.

[TABLE]

We say $o\in\mathcal{O}_{n}$ is of order-$k$ when $k$ is minimal such that $o\in\mathcal{O}_{k}$. E.g., $push_{k}$ is of order $k$.

The $collapse_{k}$ operation is non-standard in the sense of Hagueet al. [HMOS08, HMOS17] and has the semantics of a normal collapse, with the additional constraint that the top character has an order-$k$ link. The standard version of collapse can be simulated with a non-deterministic choice on the order of the stack link. In the other direction, we can store in the stack alphabet the order of the collapse link attached to each character on the stack. Note, we do not allow order-$1$ links to be created or used. In effect, these links are “null”.

We define each stack operation in turn for an order-$n$ stack $w$. Collapse links are created by the $push^{k}_{a}$ operations, which add a character to the top of a given stack $w$ with a link pointing to ${pop_{k}}\mathord{\left({w}\right)}$.

1. (1)

We set ${pop_{k}}\mathord{\left({w}\right)}=v$ when $w$ decomposes into ${u}:_{k}{v}$. 2. (2)

We set ${push_{k}}\mathord{\left({w}\right)}={u}:_{k}{{u}:_{k}{v}}$ when $w={u}:_{k}{v}$. 3. (3)

We set ${collapse_{k}}\mathord{\left({w}\right)}={bot^{i}_{k}}\mathord{\left({w}\right)}$ when ${top_{1}}\mathord{\left({w}\right)}=a^{\left({k,i}\right)}$ for some $i$. 4. (4)

We set ${push^{k}_{b}}\mathord{\left({w}\right)}={b^{\left({k,\ell-1}\right)}}:_{1}{w}$ where ${top_{k+1}}\mathord{\left({w}\right)}=[{w_{1}\ldots w_{\ell}}]_{k+1}$. 5. (5)

We set ${rew_{b}}\mathord{\left({w}\right)}={b^{\left({k,i}\right)}}:_{1}{v}$ where $w={a^{\left({k,i}\right)}}:_{1}{v}$.

Note that, for a $push_{k}$ operation, links outside of $u={top_{k}}\mathord{\left({w}\right)}$ point to the same destination in both copies of $u$, while links pointing within $u$ point within the respective copies of $u$. For full introduction, we refer the reader to Hagueet al. [HMOS08, HMOS17]. In Section 4.3 we give several example stacks and show how the stack operations affect them.

3.1.3. Collapsible Pushdown Systems

We define alternating collapsible pushdown systems.

{defi}

[Collapsible Pushdown Systems] An alternating order-$n$ collapsible pushdown system (collapsible PDS) is a tuple $\mathcal{C}=\left({\mathcal{P},\Sigma,\mathcal{R}}\right)$ where $\mathcal{P}$ is a finite set of control states, $\Sigma$ is a finite stack alphabet, and $\mathcal{R}\subseteq\left({\mathcal{P}\times\Sigma\times\mathcal{O}_{n}\times\mathcal{P}}\right)\cup\left({\mathcal{P}\times 2^{\mathcal{P}}}\right)$ is a set of rules.

We write configurations of a collapsible PDS as a pair $\langle{p},{w}\rangle$ where $p\in\mathcal{P}$ and $w\in{Stacks_{n}}\mathord{\left({\Sigma}\right)}$. We write $\langle{p},{w}\rangle\longrightarrow\langle{p^{\prime}},{w^{\prime}}\rangle$ to denote a transition from a rule $\left({{p},{a},{o},{p^{\prime}}}\right)$ with ${top_{1}}\mathord{\left({w}\right)}=a$ and $w^{\prime}={o}\mathord{\left({w}\right)}$. Furthermore, we have a transition $\langle{p},{w}\rangle\longrightarrow\left\{{\langle{p^{\prime}},{w}\rangle}\ \left|\ {p^{\prime}\in P}\right.\right\}$ whenever we have a rule ${p}\rightarrow{P}$. A non-alternating collapsible PDS has no rules of this second form. We write $C$ to denote a set of configurations.

We will be interested in the configurations that may reach a particular target set. That is, given a set $C_{f}$ of target configurations, we define the set ${Pre^{*}_{\mathcal{C}}}\mathord{\left({C_{f}}\right)}$ of configurations which can eventually reach $C_{f}$. A configuration can reach $C_{f}$ if it is contained in $C_{f}$ or there is a transition to a configuration that can reach $C_{f}$. In the case of alternating transitions to a set of configurations $C$, we require all configurations in $C$ to be able to reach $C_{f}$. This is formally defined as ${Pre^{*}_{\mathcal{C}}}\mathord{\left({C_{f}}\right)}=\bigcup\limits_{\alpha<\omega}{\rm Phys.~{}Rev.~{}E}{\alpha}{\mathcal{C}}{A_{0}}$ where

[TABLE]

3.2. Regularity of Collapsible Stacks

We will present an algorithm that operates on sets of configurations.

For this we use order-$n$ stack automata, thus defining a notion of regular sets of stacks. These have a nested structure based on a similar automata model by Bouajjani and Meyer [BM04]. The handling of collapse links is similar to automata introduced by Broadbentet al. [BCOS10], except we read stacks top-down rather than bottom-up. Note, the second condition in the definition below is a uniqueness condition that will be technically convenient throughout this article. It can be shown that it does not restrict the expressive power of the automata.

{defi}

[Order-$n$ Stack Automata] An order-$n$ stack automaton

[TABLE]

is a tuple where $\Sigma$ is a finite stack alphabet, $\mathbb{Q}_{n},\ldots,\mathbb{Q}_{1}$ are finite disjoint statesets, and

1. (1)

for all $k\in\left\{{2,\ldots,n}\right\}$, we have that $\Delta_{k}\subseteq\mathbb{Q}_{k}\times\mathbb{Q}_{k-1}\times 2^{\mathbb{Q}_{k}}$ is a transition relation, and $\mathcal{F}_{k}\subseteq\mathbb{Q}_{k}$ is a set of accepting states, 2. (2)

for all $k\in\left\{{2,\ldots,n}\right\}$ and $q_{k-1}\in\mathbb{Q}_{k-1}$, if $\left({q_{k},q_{k-1},Q_{k}}\right)\in\Delta_{k}$ and $\left({q^{\prime}_{k},q_{k-1},Q^{\prime}_{k}}\right)\in\Delta_{k}$ then $q_{k}=q^{\prime}_{k}$ and $Q_{k}=Q^{\prime}_{k}$, and 3. (3)

$\Delta_{1}\subseteq\bigcup\limits_{2\leq k\leq n}\left({\mathbb{Q}_{1}\times\Sigma\times 2^{\mathbb{Q}_{k}}\times 2^{\mathbb{Q}_{1}}}\right)$ is a transition relation, and $\mathcal{F}_{1}\subseteq\mathbb{Q}_{1}$ a set of accepting states.

Stack automata are alternating automata that read the stack in a nested fashion. Order-$k$ stacks are recognised from states in $\mathbb{Q}_{k}$. A transition $\left({q,q^{\prime},Q}\right)\in\Delta_{k}$ from $q$ to $Q$ for some $k>1$ can be fired when the topmost order-$(k-1)$ stack is accepted from $q^{\prime}\in\mathbb{Q}_{(k-1)}$. The remainder of the stack must be accepted from all states in $Q$. At order-$1$, a transition $\left({q,a,Q_{col},Q}\right)$ is a standard alternating $a$-transition with the additional requirement that the stack pointed to by the collapse link of $a$ is accepted from all states in $Q_{col}$. A stack is accepted if a subset of $\mathcal{F}_{k}$ is reached at the end of each order-$k$ stack. In Section 3.2.1, we formally define the runs of a stack automaton. We write $w\in{\mathcal{L}_{q}}\mathord{\left({A}\right)}$ whenever $w$ is accepted from a state $q$. For ease of presentation, we write $q\xrightarrow{q^{\prime}}Q\in\Delta_{k}$ instead of $\left({q,q^{\prime},Q}\right)\in\Delta_{k}$ and $q\xrightarrow[Q_{col}]{a}Q\in\Delta_{1}$ instead of $\left({q,a,Q_{col},Q}\right)\in\Delta_{1}$. Note that a transition to the empty set is distinct from having no transition.

We give two informal examples of runs below. The first is more schematic, while the second is concrete. Further examples can be found in Section 4.3.

Example 3.2**.**

A (partial) run is informally pictured in Figure LABEL:fig:schematic-run, reading an order-$3$ stack using $q_{3}\xrightarrow{q_{2}}Q_{3}\in\Delta_{3},q_{2}\xrightarrow{q_{1}}Q_{2}\in\Delta_{2}$ and $q_{1}\xrightarrow[Q_{col}]{a}Q_{1}\in\Delta_{1}$. Note, the transition $q_{3}\xrightarrow{q_{2}}Q_{3}$ reads the topmost order-$2$ stack, with the remainder of the stack being read from $Q_{3}$. The node labelled $Q_{col}$ begins a run on the stack pointed to by the collapse link of $a$. Note that the label of this node may contain other elements apart from $Q_{col}$. These additional elements come from the part of the run coming from the previous node (and other collapse links).