Reasoning about XML with temporal logics and automata

Leonid Libkin, Cristina Sirangelo

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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-Buchi 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 (C) 2009 Elsevier B V. All rights reserved.

Original languageEnglish
Pages (from-to)210-232
Number of pages23
JournalJournal of applied logic
Issue number2
Publication statusPublished - Jun 2010


Dive into the research topics of 'Reasoning about XML with temporal logics and automata'. Together they form a unique fingerprint.

Cite this