Multi-stack automata reachability: A New Tractable Subclass

Abstracted concurrent programs with recursion are best viewed as multi-stack automata. Reachability of multi-stack automata is undecidable, and several approaches to handle restricted reachability have been developed (e.g. bounded context-switching reachability is decidable).

Building on work on visibly pushdown automata, we define a new powerful class of multi-stack automata that have a decidable reachability problem. We show that if automata are restricted so that they work in at most k phases, where in each phase only one stack can be popped (push transitions on all stacks are always permitted), then the reachability problem is decidable. In fact, we obtain a robust tractable subclass of context-sensitive languages, closed under all boolean operations and with decidable emptiness and inclusion.

Finally, we consider infinite automata (not to be confused with automata on infinite words), which are automata with an infinite number of states and transitions defined using stack automata as above. We show a surprising result that these automata precisely capture the complexity class 2ETIME.