Reasoning about XML with temporal logics and automata
Reasoning about XML with temporal logics and automata
复制标题
使用时态逻辑和自动机推理 XML
DOI：
10.1016/j.jal.2009.09.005
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Cristina Sirangelo
中科院分区：
文献类型：
--
作者：
L. Libkin;Cristina Sirangelo
我们表明，在静态分析的XML规范和转换中出现的问题，可以处理使用类似的技术开发的静态分析程序。XML上下文中的许多感兴趣的属性都与导航有关，并且可以用树的时态逻辑来表示。我们选择了一种逻辑，该逻辑允许简单的单指数转换为无排名树自动机，遵循经典的LTL到Büchi自动机转换的精神。从这种翻译产生的自动机有一些额外的属性，特别是，它们便于推理一元节点选择查询，这在XML上下文中很重要。我们给出了这样的推理的两个应用程序：一个处理一个经典的XML问题的推理模式的存在下，导航，另一个涉及到验证安全属性的XML视图。
We show that problems arising in static analysis of XML specifications and transformations can be dealt with using techniques similar to those developed for static analysis of programs. Many properties of interest in the XML context are related to navigation, and can be formulated in temporal logics for trees. We choose a logic that admits a simple single-exponential translation into unranked tree automata, in the spirit of the classical LTL-to-Büchi automata translation. Automata arising from this translation have a number of additional properties; in particular, they are convenient for reasoning about unary node-selecting queries, which are important in the XML context. We give two applications of such reasoning: one deals with a classical XML problem of reasoning about navigation in the presence of schemas, and the other relates to verifying security properties of XML views.