Paper detail

$μ$-calculus on data words

We study the decidability and expressiveness issues of $μ$-calculus on data words and data $ω$-words. It is shown that the full logic as well as the fragment which uses only the least fixpoints are undecidable, while the fragment containing only greatest fixpoints is decidable. Two subclasses, namely BMA and BR, obtained by limiting the compositions of formulas and their automata characterizations are exhibited. Furthermore, Data-LTL and two-variable first-order logic are expressed as unary alternation-free fragment of BMA. Finally basic inclusions of the fragments are discussed.