eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2014-12-12
267
278
10.4230/LIPIcs.FSTTCS.2014.267
article
Generalized Data Automata and Fixpoint Logic
Colcombet, Thomas
Manuel, Amaldev
Data omega-words are omega-words where each position is additionally labelled by a data value from an infinite alphabet. They can be seen as graphs equipped with two sorts of edges: "next position" and "next position with the same data value". Based on this view, an extension of Data Automata called Generalized Data Automata (GDA) is introduced. While the decidability of emptiness of GDA is open, the decidability for a subclass class called Büchi GDA is shown using Multicounter Automata. Next a natural fixpoint logic is defined on the graphs of data omega-words and it is shown that the mu-fragment as well as the alternation-free fragment is undecidable. But the fragment which is defined by limiting the number of alternations between future and past formulas is shown to be decidable, by first converting the formulas to equivalent alternating Büchi automata and then to Büchi GDA.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol029-fsttcs2014/LIPIcs.FSTTCS.2014.267/LIPIcs.FSTTCS.2014.267.pdf
Data words
Data Automata
Decidability
Fixpoint Logic