Adding Nesting Structure to Words
Adding Nesting Structure to Words
复制标题
DOI：
10.1145/1516512.1516518
复制
发表时间：
2009-05-01
影响因子：
2.5
通讯作者：
Madhusudan, P.
中科院分区：
文献类型：
--
作者：
Alur, Rajeev;Madhusudan, P.
我们提出了嵌套词模型，用于表示项的线性排序和分层嵌套匹配的数据。具有这种双线性-分层结构的数据的例子包括结构化程序、带注释的语言数据和HTML/XML文档的执行。嵌套字词泛化了字词和有序树，并允许字和树操作。我们定义了嵌套词的嵌套词自动机--有限态嵌套词的接受者，并证明了由此得到的嵌套词正则语言类具有经典正则词语言所具有的所有吸引人的理论性质：确定性嵌套词自动机的表达能力与它们的非确定对应的嵌套词自动机相同；类在并、交、补、级联、Kleene-*、前缀和语言同态下是封闭的；从属关系、空性、语言包含和语言等价都是可判定的；一元二阶逻辑中的可定义性恰好对应于有限状态可识别性。我们还考虑了无限嵌套词的正则语言，证明了决策问题的闭包性质、MSO刻画和可判定性，嵌套词的线性编码给出了一类明显的下推语言，这类语言介于平衡语言和确定性上下文无关语言之间。我们认为，对于结构化程序的算法验证，不应将程序视为一种基于词的上下文无关语言，而应将其视为一种嵌套词的规则语言(或等价地，明显的下推语言)，这将允许对现有规范逻辑中无法表达的许多性质(如堆栈检查、前置条件)进行模型检查。我们还研究了有序树和嵌套词以及相应自动机之间的关系：尽管嵌套词自动机的分析复杂性与经典树自动机相同，但它们结合了自下而上和自上而下的遍历，并享受了树自动机的表现性和简洁性优势。
We propose the model of nested words for representation of data with both a linear ordering and a hierarchically nested matching of items. Examples of data with such dual linear-hierarchical structure include executions of structured programs, annotated linguistic data, and HTML/XML documents. Nested words generalize both words and ordered trees, and allow both word and tree operations. We define nested word automata-finite-state acceptors for nested words, and show that the resulting class of regular languages of nested words has all the appealing theoretical properties that the classical regular word languages enjoys: deterministic nested word automata are as expressive as their nondeterministic counterparts; the class is closed under union, intersection, complementation, concatenation, Kleene-*, prefixes, and language homomorphisms; membership, emptiness, language inclusion, and language equivalence are all decidable; and definability in monadic second order logic corresponds exactly to finite-state recognizability. We also consider regular languages of infinite nested words and show that the closure properties, MSO-characterization, and decidability of decision problems carry over.The linear encodings of nested words give the class of visibly pushdown languages of words, and this class lies between balanced languages and deterministic context-free languages. We argue that for algorithmic verification of structured programs, instead of viewing the program as a context-free language over words, one should view it as a regular language of nested words ( or equivalently, a visibly pushdown language), and this would allow model checking of many properties (such as stack inspection, pre-post conditions) that are not expressible in existing specification logics.We also study the relationship between ordered trees and nested words, and the corresponding automata: while the analysis complexity of nested word automata is the same as that of classical tree automata, they combine both bottom-up and top-down traversals, and enjoy expressiveness and succinctness benefits over tree automata.