Fragments of Fixpoint Logic on Data Words

Authors Thomas Colcombet, Amaldev Manuel



PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2015.98.pdf
  • Filesize: 0.54 MB
  • 14 pages

Document Identifiers

Author Details

Thomas Colcombet
Amaldev Manuel

Cite AsGet BibTex

Thomas Colcombet and Amaldev Manuel. Fragments of Fixpoint Logic on Data Words. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 98-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.FSTTCS.2015.98

Abstract

We study fragments of a mu-calculus over data words whose primary modalities are 'go to next position' (X^g), 'go to previous position}' (Y^g), 'go to next position with the same data value' (X^c), 'go to previous position with the same data value (Y^c)'. Our focus is on two fragments that are called the bounded mode alternation fragment (BMA) and the bounded reversal fragment (BR). BMA is the fragment of those formulas that whose unfoldings contain only a bounded number of alternations between global modalities (X^g, Y^g) and class modalities (X^c, Y^c). Similarly BR is the fragment of formulas whose unfoldings contain only a bounded number of alternations between left modalities (Y^g, Y^c) and right modalities (X^g, X^c). We show that these fragments are decidable (by inclusion in Data Automata), enjoy effective Boolean closure, and contain previously defined logics such as the two variable fragment of first-order logic and DataLTL. More precisely the definable language in each formalism obey the following inclusions that are effective. FO^2 subsetneq DataLTL subsetneq BMA BR subsetneq nu subseteq Data Automata. Our main contribution is a method to prove inexpressibility results on the fragment BMA by reducing them to inexpressibility results for combinatorial expressions. More precisely we prove the following hierarchy of definable languages, emptyset=BMA^0 subsetneq BMA^1 subsetneq ... subsetneq BMA subsetneq BR , where BMA^k is the set of all formulas whose unfoldings contain at most k-1 alternations between global modalities (X^g, Y^g) and class modalities (X^c, Y^c). Since the class BMA is a generalization of FO^2 and DataLTL the inexpressibility results carry over to them as well.
Keywords
  • Data words
  • Data automata
  • Fixpoint logic

Metrics

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

References

  1. Henrik Björklund and Thomas Schwentick. On notions of regularity for data languages. Theor. Comput. Sci., 411(4-5):702-715, 2010. Google Scholar
  2. 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
  3. Mikołaj Bojańczyk. Data monoids. In STACS, pages 105-116, 2011. Google Scholar
  4. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27, 2011. Google Scholar
  5. Thomas Colcombet, Clemens Ley, and Gabriele Puppis. On the use of guards for logics with data. In MFCS, volume 6907 of LNCS, pages 243-255. Springer, 2011. Google Scholar
  6. Thomas Colcombet and Amaldev Manuel. Generalized data automata and fixpoint logic. In FSTTCS 2014, volume 29 of LIPIcs, pages 267-278, 2014. Google Scholar
  7. Thomas Colcombet and Amaldev Manuel. Combinatorial expressions and lower bounds. In STACS 2015, volume 30 of LIPIcs, pages 249-261, 2015. Google Scholar
  8. 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
  9. Stéphane Demri and Ranko Lazić. LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic, 10(3), April 2009. Google Scholar
  10. D. Figueira. Alternating register automata on finite data words and trees. Logical Methods in Computer Science, 8(1), 2012. Google Scholar
  11. D. Figueira. Decidability of downward XPath. ACM Transactions on Computational Logic, 13(4), 2012. Google Scholar
  12. 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
  13. M. Jurdziński and R. Lazic. Alternating automata on data trees and xpath satisfiability. ACM Trans. Comput. Log., 12(3):19, 2011. Google Scholar
  14. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. Google Scholar
  15. Ahmet Kara, Thomas Schwentick, and Thomas Zeume. Temporal logics on words with multiple data values. In FSTTCS, volume 8 of LIPIcs, pages 481-492, 2010. Google Scholar
  16. L. Libkin and D. Vrgoc. Regular expressions for data words. In LPAR, volume 7180 of Lecture Notes in Computer Science, pages 274-288. SPRINGER, 2012. Google Scholar
  17. A. Manuel, A. Muscholl, and G. Puppis. Walking on data words. In Computer Science Theory and Applications, volume 7913 of LNCS, pages 64-75. Springer, 2013. Google Scholar
  18. F. Neven, T. Schwentick, and V. Vianu. Finite state machines for strings over infinite alphabets. ACM Transactions on Computational Logic, 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