Document

Fragments of Fixpoint Logic on Data Words

File

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

Cite As

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

References

1. Henrik Björklund and Thomas Schwentick. On notions of regularity for data languages. Theor. Comput. Sci., 411(4-5):702-715, 2010.
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.
3. Mikołaj Bojańczyk. Data monoids. In STACS, pages 105-116, 2011.
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.
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.
6. Thomas Colcombet and Amaldev Manuel. Generalized data automata and fixpoint logic. In FSTTCS 2014, volume 29 of LIPIcs, pages 267-278, 2014.
7. Thomas Colcombet and Amaldev Manuel. Combinatorial expressions and lower bounds. In STACS 2015, volume 30 of LIPIcs, pages 249-261, 2015.
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.
9. Stéphane Demri and Ranko Lazić. LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic, 10(3), April 2009.
10. D. Figueira. Alternating register automata on finite data words and trees. Logical Methods in Computer Science, 8(1), 2012.
11. D. Figueira. Decidability of downward XPath. ACM Transactions on Computational Logic, 13(4), 2012.
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.
13. M. Jurdziński and R. Lazic. Alternating automata on data trees and xpath satisfiability. ACM Trans. Comput. Log., 12(3):19, 2011.
14. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994.
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.
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.
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.
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.