Name
Abstract | ||
|---|---|---|
Close relationships between XML navigation and temporal logics have been discovered recently, in particular between logics LTL and CTL* and XPath navigation, and between the μ-calculus and navigation based on regular expressions. This opened up the possibility of bringing model-checking techniques into the field of XML, as documents are naturally represented as labeled transition systems. Most known results of this kind, however, are limited to Boolean or unary queries, which are not always sufficient for complex querying tasks. Here we present a technique for combining temporal logics to capture n-ary XML queries expressible in two yardstick languages: FO and MSO. We show that by adding simple terms to the language, and combining a temporal logic for words together with a temporal logic for unary tree queries, one obtains logics that select arbitrary tuples of elements, and can thus be used as building blocks in complex query languages. We present general results on the expressiveness of such temporal logics, study their model-checking properties, and relate them to some common XML querying tasks. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/11965893_25 | ICDT |
Keywords | Field | DocType |
temporal logic,model-checking technique,complex query language,complex querying task,common xml querying task,model-checking property,n-ary xml,querying xml document,logics ltl,xml navigation,xpath navigation,query language,regular expression,model checking,xml document | Computation tree logic,T-norm fuzzy logics,Query language,Programming language,XML,XML validation,Tuple,Computer science,Theoretical computer science,XPath,Temporal logic | Conference |
Volume | ISSN | ISBN |
4353 | 0302-9743 | 3-540-69269-X |
Citations | PageRank | References |
7 | 0.44 | 34 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marcelo Arenas | 1 | 2618 | 193.91 |
| Pablo Barceló | 2 | 492 | 41.45 |
| Leonid Libkin | 3 | 3446 | 764.02 |