2026-08-17T08:55:53Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5628 2024-03-06T10:36:42Z ddc:004 open_access

Fragments of Fixpoint Logic on Data Words Colcombet, Thomas Manuel, Amaldev Data words Data automata Fixpoint logic 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thomas Colcombet and Amaldev Manuel 2015 Is Part Of LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2015.98 urn:nbn:de:0030-drops-56289 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.98 eng https://creativecommons.org/licenses/by/3.0/legalcode