We investigate the decidability of logical aspects of graphs that arise as Cayley-graphs of the so-called 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.
@InProceedings{abuzaid_et_al:LIPIcs.FSTTCS.2018.9, author = {Abu Zaid, Faried and K\"{o}cher, Chris}, title = {{The Cayley-Graph of the Queue Monoid: Logic and Decidability}}, booktitle = {38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)}, pages = {9:1--9:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-093-4}, ISSN = {1868-8969}, year = {2018}, volume = {122}, editor = {Ganguly, Sumit and Pandya, Paritosh}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.9}, URN = {urn:nbn:de:0030-drops-99088}, doi = {10.4230/LIPIcs.FSTTCS.2018.9}, annote = {Keywords: Queues, Transformation Monoid, Cayley-Graph, Logic, First-Order Theory, MSO Theory, Model Checking} }
Feedback for Dagstuhl Publishing