Abstract
Abstract: We study fragments of a $\mu$-calculus over data words whose primary modalities are ‘go to next position’ ($\mathtt{X}^g$), ‘go to previous position’ ($\mathtt{Y}^g$), ‘go to next position with the same data value’ ($\mathtt{X}^c$), ‘go to previous position with the same data value ($\mathtt{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 ($\mathtt{X}^g, \mathtt{Y}^g$) and class modalities ($\mathtt{X}^c, \mathtt{Y}^c$). Similarly BR is the fragment of formulas whose unfoldings contain only a bounded number of alternations between left modalities ($\mathtt{Y}^g, \mathtt{Y}^c$) and right modalities ($\mathtt{X}^g, \mathtt{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.
$$\mathrm{FO}^2 \subsetneq \mathrm{DataLTL} \subsetneq \mathrm{BMA} \subsetneq \mathrm{BR} \subsetneq \nu \subseteq \mathrm{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 = \mathrm{BMA}^0 \subsetneq \mathrm{BMA}^1 \subsetneq \cdots \subsetneq \mathrm{BMA} \subsetneq \mathrm{BR},$$
where $\mathrm{BMA}^k$ is the set of all formulas whose unfoldings contain at most $k−1$ alternations between global modalities ($\mathtt{X}^g, \mathtt{Y}^g$) and class modalities ($\mathtt{X}^c, \mathtt{Y}^c$). Since the class BMA is a generalization of $\mathrm{FO}^2$ and DataLTL, the inexpressibility results carry over to them as well.
