Reachability Problems in Multi-Queue Automata

In this talk, we will focus on automata having multiple reliable queues which are partially synchronized. This means, whenever we write or read some letter we do this operation on a specified subset of these queues at the same time. For example, with the help of these machines we can easily simulate networks of finite automata which communicate through some reliable channels, so-called communicating automata. However, these partially synchronized multi-queue automata are more general since we are able to synchronize the contents of two specified channels while other channels can be handled asynchronously. Note that this model also covers automata having one or more queues without any synchronization. Obviously, the reachability problem of these machines is undecidable. Hence, we need some approximation of this problem. This can be done step by step by computation of all configurations after application of n atomic queue operations for some increasing natural number n. Using this approach we obtain an algorithm which semi-decides the reachability problem. However, this approximation is very inefficient since we always explore only a finite space of reachable configurations. Boigelot et al. improved this approximation by introduction of so-called meta-transformations. These are special sets of transformation sequences such that we can easily compute the set of reachable configurations. Boigelot et al. focused on single- and (asynchronous) multi-queue automata looping through a single sequence of transformations t. In other words, given a recognizable set C of configurations and some special transformation sequence t, the authors have proven that the set configurations reachable from C via t^* is effectively recognizable. Here, we generalize this result to our partially synchronized multi-queue automata. We also consider some special recognizable sets T of transformation sequences such that we can compute a recognizable set of configurations which are reachable via the transformation sequences in T^*. Concretely, we consider such recognizable sets of transformation sequences which are alternating between two sets of write actions and read actions. For these sets we prove that, starting from a given recognizable set of configurations we will end up in an effectively recognizable set of configurations after application of these transformation sequences.

Authors

• Chris Köcher

Keywords

No keywords are indexed for this paper.