Regular Languages of Nested Words: Fixed Points, Automata, and Synchronization
Regular Languages of Nested Words: Fixed Points, Automata, and Synchronization
复制标题
嵌套词的正则语言：不动点、自动机和同步
DOI：
10.1007/s00224-010-9292-5
复制
发表时间：
2010
影响因子：
0.5
通讯作者：
Arenas M
中科院分区：
文献类型：
--
作者：
Arenas M
嵌套词提供了具有递归过程调用的程序运行的自然模型。一元二阶逻辑（MSO）和自动机之间的通常联系从单词扩展到嵌套单词，并给我们一个嵌套单词的规则语言的自然概念。在本文中，我们研究了正则语言的一些众所周知的方面——它们通过不动点的表征，它们的确定性和交替自动机，以及定义正则关系的同步——并将它们扩展到嵌套词。我们证明了mu-calculus在有限和无限嵌套词上与MSO一样具有表达性，并且更一般地说，对于具有过去模态的mu-calculus，在单词的任意位置评估，而不仅仅是在第一个位置。我们为嵌套词引入交替自动机的概念，表明它们与通常的自动机一样具有表达能力，并且还证明穆勒自动机是可以确定的（不像在可见的下推语言的情况下）。最后，我们看一下嵌套词的同步。我们证明了通常的字母到字母的同步与嵌套词是完全不相容的（在这个意义上，即使是最弱的同步形式也会导致一种不可确定的形式主义），并提出了另一种同步形式，它给我们提供了规则关系的可确定概念。
Nested words provide a natural model of runs of programs with recursive procedure calls. The usual connection between monadic second-order logic (MSO) and automata extends from words to nested words and gives us a natural notion of regular languages of nested words.In this paper we look at some well-known aspects of regular languages—their characterization via fixed points, deterministic and alternating automata for them, and synchronization for defining regular relations—and extend them to nested words. We show that mu-calculus is as expressive as MSO over finite and infinite nested words, and the equivalence holds, more generally, for mu-calculus with past modalities evaluated in arbitrary positions in a word, not only in the first position. We introduce the notion of alternating automata for nested words, show that they are as expressive as the usual automata, and also prove that Muller automata can be determinized (unlike in the case of visibly pushdown languages). Finally we look at synchronization over nested words. We show that the usual letter-to-letter synchronization is completely incompatible with nested words (in the sense that even the weakest form of it leads to an undecidable formalism) and present an alternative form of synchronization that gives us decidable notions of regular relations.
登录
查看更多内容
DOI：
10.1007/3-540-61604-7_60
发表时间：
1996-08
期刊：
--
影响因子：
--
作者：
David Janin;I. Walukiewicz
通讯作者：
David Janin;I. Walukiewicz
固定点与无限生成
DOI：
--
发表时间：
1988
期刊：
[1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science
影响因子：
--
作者：
D. Niwinski
通讯作者：
D. Niwinski
嵌套树的语言
DOI：
--
发表时间：
2006
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
R. Alur;Swarat Chaudhuri;P. Madhusudan
通讯作者：
P. Madhusudan
明显下推语言的正则性问题
DOI：
--
发表时间：
2006
期刊：
Symposium on Theoretical Aspects of Computer Science
影响因子：
--
作者：
V. Bárány;Christof Löding;O. Serre
通讯作者：
O. Serre
验证流式 XML 文档
DOI：
--
发表时间：
2002
期刊：
ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems
影响因子：
--
作者：
L. Segoufin;V. Vianu
通讯作者：
V. Vianu