License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2015.98
URN: urn:nbn:de:0030-drops-56289
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5628/
Colcombet, Thomas ;
Manuel, Amaldev
Fragments of Fixpoint Logic on Data Words
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.
BibTeX - Entry
@InProceedings{colcombet_et_al:LIPIcs:2015:5628,
author = {Thomas Colcombet and Amaldev Manuel},
title = {{Fragments of Fixpoint Logic on Data Words}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {98--111},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Prahladh Harsha and G. Ramalingam},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5628},
URN = {urn:nbn:de:0030-drops-56289},
doi = {10.4230/LIPIcs.FSTTCS.2015.98},
annote = {Keywords: Data words, Data automata, Fixpoint logic}
}
|
Keywords: |
|
Data words, Data automata, Fixpoint logic |
|
Collection: |
|
35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015) |
|
Issue Date: |
|
2015 |
|
Date of publication: |
|
14.12.2015 |
