XML schema, tree logic and sheaves automata
XML schema, tree logic and sheaves automata
复制标题
XML 模式、树逻辑和滑轮自动机
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
D. Lugiez
中科院分区：
文献类型：
--
作者：
Silvano Dal;D. Lugiez
XML文档可以粗略地描述为未排序的有序树，因此使用树自动机来处理或验证它们是很自然的。这个思想已经成功地应用于文档类型定义（Document Type Definition， DTD）的上下文中，DTD是定义文档有效性的最简单标准，但是还需要做额外的工作来考虑XML Schema，这是一种更高级的标准，常规树自动机不能满足这种标准。在本文中，我们介绍了一种新的树形逻辑，它扩展了W3C XML模式定义语言（WXS）的无递归片段的语法。然后，我们为未排序树定义了一类新的自动机，为SL的基本问题提供了决策过程：模型检查；可满足性;蕴涵。同一类自动机也用于回答有关WXS的基本问题，包括递归模式：类型检查文档的可判定性；测试模式的空性；测试一个模式是否包含另一个模式。
XML documents may be roughly described as unranked, ordered trees and it is therefore natural to use tree automata to process or validate them. This idea has already been successfully applied in the context of Document Type Definition (DTD), the simplest standard for defining document validity, but additional work is needed to take into account XML Schema, a more advanced standard, for which regular tree automata are not satisfactory. In this paper, we introduce Sheaves Logic (SL), a new tree logic that extends the syntax of the – recursion-free fragment of – W3C XML Schema Definition Language (WXS). Then, we define a new class of automata for unranked trees that provides decision procedures for the basic questions about SL: model-checking; satisfiability; entailment. The same class of automata is also used to answer basic questions about WXS, including recursive schemas: decidability of type-checking documents; testing the emptiness of schemas; testing that a schema subsumes another one.