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.
A recent result of Haase et al. has shown that reachability in two-clock timed automata is log-space equivalent to reachability in bounded one-counter automata. We show that reachability in bounded one-counter automata is PSPACE-complete.
We study the qualitative and quantitative zero-reachability problem in probabilistic multi-counter systems. We identify the undecidable variants of the problems, and then we concentrate on the remaining two cases. In the first case, when we are interested in the probability of all runs that visit zero in some counter, we show that the qualitative zero-reachability is decidable in time which is polynomial in the size of a given pMC and doubly exponential in the number of counters. Further, we show that the probability of all zero-reaching runs can be effectively approximated up to an arbitraril…
We study the computational complexity of reachability, coverability and inclusion for extensions of context-free commutative grammars with integer counters and reset operations on them. Those grammars can alternatively be viewed as an extension of communication-free Petri nets. Our main results are that reachability and coverability are inter-reducible and both NP-complete. In particular, this class of commutative grammars enjoys semi-linear reachability sets. We also show that the inclusion problem is, in general, coNEXP-complete and already $Π_2^\text{P}$-complete for grammars with only one …
This article focuses on subset reachability in synchronizing automata. First, we provide families of synchronizing automata with subsets which cannot be reached with short words. These families do not fulfil Don's Conjecture about subset reachability. Moreover, they show that some subsets need exponentially long words to be reached, and that the restriction of the conjecture to included subsets also does not hold. Second, we analyze completely reachable automata and provide a counterexample to the conjecture of Bondar and Volkov about the so-called $Γ_1$-graph. We finally prove an alternative …
A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown store. A PVASS is said to be \emph{bidirected} if every transition (pushing/popping a symbol or modifying a counter) has an accompanying opposite transition that reverses the effect. Bidirectedness arises naturally in many models; it can also be seen as a overapproximation of reachability. We show that the reachability problem for \emph{bidirected} PVASS is decidable in Ackermann time and primitive recursive for any fixed dimension. For the special case of one-dimensional bidirect…
Vector addition system with states is an ubiquitous model of computation with extensive applications in computer science. The reachability problem for vector addition systems is central since many other problems reduce to that question. The problem is decidable and it was recently proved that the dimension of the vector addition system is an important parameter of the complexity. In fixed dimensions larger than two, the complexity is not known (with huge complexity gaps). In dimension two, the reachability problem was shown to be PSPACE-complete by Blondin et al. in 2015. We consider an extens…
We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper and lower bound tests against the counter value. Additionally, the counter updates associated with taking transitions can be (non-deterministically) scaled down by a nonzero factor between zero and one. Our three main results are as follows: (1) We prove that the reachability problem for COCA with global upper and lower bound tests is in NC2; (2) that, in general, the problem is decidable in polynomial time; and (3) that it is decidable in the polynomial hie…
We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the reachability problem for such systems to the reachability problem for register machines enriched with the given abstract data type. We use the translation to obtain tight complexity bounds for TSO-based parameterized verification over several abstract data types, such as push-down automata, ordered multi push-down automata, one-counter nets, one-counter automa…
Multi-stack pushdown systems are a well-studied model of concurrent computation using threads with first-order procedure calls. While, in general, reachability is undecidable, there are numerous restrictions on stack behaviour that lead to decidability. To model higher-order procedures calls, a generalisation of pushdown stacks called collapsible pushdown stacks are required. Reachability problems for multi-stack collapsible pushdown systems have been little studied. Here, we study ordered, phase-bounded and scope-bounded multi-stack collapsible pushdown systems using saturation techniques, sh…
Extensions to finite-state automata on strings, such as multi-head automata or multi-counter automata, have been successfully used to encode many infinite-state non-regular verification problems. In this paper, we consider a generalization of automata-theoretic infinite-state verification from strings to labeled series-parallel graphs. We define a model of non-deterministic, 2-way, concurrent automata working on series-parallel graphs and communicating through shared registers on the nodes of the graph. We consider the following verification problem: given a family of series-parallel graphs de…
We study pushdown vector addition systems, which are synchronized products of pushdown automata with vector addition systems. The question of the boundedness of the reachability set for this model can be refined into two decision problems that ask if infinitely many counter values or stack configurations are reachable, respectively. Counter boundedness seems to be the more intricate problem. We show decidability in exponential time for one-dimensional systems. The proof is via a small witness property derived from an analysis of derivation trees of grammar-controlled vector addition systems.
Parametric timed automata (PTA) are an extension of timed automata in which clocks can be compared against parameters. The reachability problem asks for the existence of an assignment of the parameters to the non-negative integers such that reachability holds in the underlying timed automaton. The reachability problem for PTA is long known to be undecidable, already over three parametric clocks. A few years ago, Bundala and Ouaknine proved that for PTA over two parametric clocks and one parameter the reachability problem is decidable and also showed a lower bound for the complexity class PSPAC…
Higher-order pushdown systems and ground tree rewriting systems can be seen as extensions of suffix word rewriting systems. Both classes generate infinite graphs with interesting logical properties. Indeed, the model-checking problem for monadic second order logic (respectively first order logic with a reachability predicate) is decidable on such graphs. We unify both models by introducing the notion of stack trees, trees whose nodes are labelled by higher-order stacks, and define the corresponding class of higher-order ground tree rewriting systems. We show that these graphs retain the decida…
We define a new class of pushdown systems where the pushdown is a tree instead of a word. We allow a limited form of lookahead on the pushdown conforming to a certain ordering restriction, and we show that the resulting class enjoys a decidable reachability problem. This follows from a preservation of recognizability result for the backward reachability relation of such systems. As an application, we show that our simple model can encode several formalisms generalizing pushdown systems, such as ordered multi-pushdown systems, annotated higher-order pushdown systems, the Krivine machine, and or…
A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show decidability of the diagonal problem for schemes. This result has several interesting consequences. In particular, it gives an algorithm that computes the downward closure of languages of words recognized by schemes. In turn, this has immediate application to separability problems and reachability analysis of concurrent systems.
We study the first-order model checking problem on two generalisations of pushdown graphs. The first class is the class of nested pushdown trees. The other is the class of collapsible pushdown graphs. Our main results are the following. First-order logic with reachability is uniformly decidable on nested pushdown trees. Considering first-order logic without reachability, we prove decidability in doubly exponential alternating time with linearly many alternations. First-order logic with regular reachability predicates is uniformly decidable on level 2 collapsible pushdown graphs. Moreover, nest…
We study the reachability problem for networks of timed communicating processes. Each process is a timed automaton communicating with other processes by exchanging messages over unbounded FIFO channels. Messages carry clocks which are checked at the time of transmission and reception with suitable timing constraints. Each automaton can only access its set of local clocks and message clocks of sent/received messages. Time is dense and all clocks evolve at the same rate. Our main contribution is a complete characterisation of decidable and undecidable communication topologies generalising and un…
