Reachability Problem for Weak Multi-Pushdown Automata

TL;DR

This paper investigates the reachability problem in a restricted class of multi-pushdown automata with a partial order on control states, proving decidability and identifying NP-complete subclasses, linking to communication-free vector addition systems.

Contribution

It introduces a new decidability result for a subclass of multi-pushdown automata and characterizes the complexity of reachability in relevant subclasses.

Findings

Decidability of reachability in the restricted subclass.

NP-completeness of reachability in certain subclasses.

Equivalence in complexity with communication-free vector addition systems.

Abstract

This paper is about reachability analysis in a restricted subclass of multi-pushdown automata. We assume that the control states of an automaton are partially ordered, and all transitions of an automaton go downwards with respect to the order. We prove decidability of the reachability problem, and computability of the backward reachability set. As the main contribution, we identify relevant subclasses where the reachability problem becomes NP-complete. This matches the complexity of the same problem for communication-free vector addition systems, a special case of stateless multi-pushdown automata.