Verifying Multi-Pushdown Automata

In this talk we will focus on automata having multiple stacks as their memory. Concretely, our automata consist of multiple local finite automata each having one stack. We additionally allow partial synchronizations between these stacks. This means, whenever we read or write a letter we do this operation on a specified subset of these stacks at the same time. Note that our model also covers automata having one or more stacks without synchronization. It is well-known that automata having at least two stacks are as powerful as Turing-machines implying the undecidability of all non-trivial verification problems of such systems. To circumvent these undecidabilities we consider a special restriction to these automata. So, when applying a transition of our special automata, we read a letter a, execute local transitions simultaneously on each local automaton able to handle the letter a, and we write other letters at most into the stacks associated to the letter a. We can show then that the set of backwards reachable configurations of a recognizable set of configurations of such special multi-pushdown automaton is effectively recognizable again. In contrast we can find a recognizable set of configurations such that the forwards reachable configurations are not recognizable anymore. Anyways, we learn that the reachability problem and even recurrent reachability problem are decidable in polynomial time. We also obtain that the model checking problem of Thiagarajan's LTL for traces is decidable in our multi-pushdown automata. Note that this talk is based on a joint work with Dietrich Kuske.

Authors

• Chris Köcher

Keywords

No keywords are indexed for this paper.