Document Open Access Logo

Generalized Data Automata and Fixpoint Logic

Authors Thomas Colcombet, Amaldev Manuel

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2014.267.pdf
  • Filesize: 477 kB
  • 12 pages

Document Identifiers

Author Details

Thomas Colcombet
Amaldev Manuel

Cite As Get BibTex

Thomas Colcombet and Amaldev Manuel. Generalized Data Automata and Fixpoint Logic. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 267-278, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/LIPIcs.FSTTCS.2014.267

Abstract

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.

Subject Classification

Keywords
  • Data words
  • Data Automata
  • Decidability
  • Fixpoint Logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. H. Björklund and T. Schwentick. On notions of regularity for data languages. Theor. Comput. Sci., 411(4-5):702-715, 2010. Google Scholar
  2. M. Bojańczyk. Data monoids. In STACS, pages 105-116, 2011. Google Scholar
  3. M. Bojańczyk, C. David, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27, 2011. Google Scholar
  4. M. Bojańczyk and S. Lasota. An extension of data automata that captures xpath. In Logic in Computer Science (LICS), 2010, pages 243-252, July 2010. Google Scholar
  5. T. Colcombet, C. Ley, and G. Puppis. On the use of guards for logics with data. In MFCS, volume 6907 of LNCS, pages 243-255. Springer, 2011. Google Scholar
  6. S. Demri, D. Figueira, and M. Praveen. Reasoning about data repetitions with counter systems. In Logic in Computer Science (LICS), 2013, pages 33-42, June 2013. Google Scholar
  7. S. Demri and R. Lazić. LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic, 10(3), April 2009. Google Scholar
  8. D. Figueira. Alternating register automata on finite data words and trees. Logical Methods in Computer Science, 8(1), 2012. Google Scholar
  9. D. Figueira. Decidability of downward XPath. ACM Transactions on Computational Logic, 13(4), 2012. Google Scholar
  10. E. Grädel, W. Thomas, and T. Wilke, editors. Automata Logics, and Infinite Games: A Guide to Current Research. Springer-Verlag New York, Inc., New York, NY, USA, 2002. Google Scholar
  11. O. Grumberg, O. Kupferman, and S. Sheinvald. Variable automata over infinite alphabets. In Language and Automata Theory and Applications, pages 561-572. Springer, 2010. Google Scholar
  12. M. Jurdziński and R. Lazic. Alternating automata on data trees and xpath satisfiability. ACM Trans. Comput. Log., 12(3):19, 2011. Google Scholar
  13. M. Kaminski and N. Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. Google Scholar
  14. A. Kara, T. Schwentick, and T. Zeume. Temporal logics on words with multiple data values. In FSTTCS, volume 8 of LIPIcs, pages 481-492, 2010. Google Scholar
  15. L. Libkin and D. Vrgoc. Regular expressions for data words. In LPAR, volume 7180, pages 274-288, 2012. Google Scholar
  16. A. Manuel, A. Muscholl, and G. Puppis. Walking on data words. In Computer Science Theory and Applications, volume 7913 of LNCS, pages 64-75. 2013. Google Scholar
  17. F. Neven, T. Schwentick, and V. Vianu. Finite state machines for strings over infinite alphabets. 5(3):403-435, 2004. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact