The Cayley-Graph of the Queue Monoid: Logic and Decidability

We investigate the decidability of logical aspects of graphs that arise as Cayley-graphs of the socalled queue monoids. These monoids model the behavior of the classical (reliable) fifo-queues. We answer a question raised by Huschenbett, Kuske, and Zetzsche and prove the decidability of the first-order theory of these graphs with the help of an at least for the authors new combination of the well-known method from Ferrante and Rackoff and an automata-based approach. On the other hand, we prove that the monadic second-order of the queue monoid’s Cayley-graph is undecidable. 2012 ACM Subject Classification Theory of computation Ñ Logic, Theory of computation Ñ Models of computation, Information systems Ñ Data structures