Reachability Problems on Partially Lossy Queue Automata

We study the reachability problem for queue automata and lossy queue automata. Queue automata are known to be Turing-complete implying the undecidability of the reachability problem. In contrast to this result, reachability is decidable (but not primitive recursive) if the queue automata are allowed to forget any parts of their contents. A trivial approach to approximate the reachability problem is the step-by-step simulation of the queue automata’s computations. Boigelot et al. and Abdulla et al. improved this approximation by considering so-called “meta-transitions” which are special sequences of transformations. In particular, the iteration of some sequence of transformations is such a meta-transition. It was proven that, starting from a regular language of queue contents, the set of reachable queue contents after application of any meta-transition is effectively regular, again. Here, we want to improve these results by considering two further meta-transformations: on the one hand, we consider the iteration of certain languages of transformations. Especially, this is a generalization of the results from Boigelot et al. and Abdulla et al. On the other hand, we consider languages of transformations which are closed under certain context-sensitive commutations. We will see that the application of both meta-transformations preserves regularity. Both constructions are possible in polynomial time. Hence, this is a huge benefit for verification in contrast to the undecidability resp. inefficiency of the original reachability problem of reliable and lossy queue automata.

Authors

• Chris Köcher.

Keywords

No keywords are indexed for this paper.