加载中…
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.

生成讲解博客的中文版本

生成AI智能校验的中文版本