Reasoning about XML with temporal logics and automata

13 years 5 months ago
Reasoning about XML with temporal logics and automata
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¨uchi 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. Keywords Query automata, static analysis, temporal logics, XML
Leonid Libkin, Cristina Sirangelo
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2010
Authors Leonid Libkin, Cristina Sirangelo
Comments (0)