|
Published Articles >> Table of Contents >> Abstract
11th International Symposium on Temporal Representation and Reasoning (TIME'04)
pp. 117-124
CTL Model Checking for Processing Simple XPath Queries
Loredana Afanasiev, University of Amsterdam
Massimo Franceschet, University of Amsterdam and University "G. d’Annunzio" of Chieti-Pescara
Maarten Marx, University of Amsterdam
Maarten de Rijke, University of Amsterdam
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2004.1314428
Send link to a friend
| Abstract |
|
The Extensible Markup Language (XML) was
designed to describe the content of a document
and its hierarchical structure, and the XML Path
language (XPath) is a language for selecting elements
from XML documents. There is a close connection
between the query processing problem for
XPath and the model checking problem for temporal
logics. Both boil down to checking which
nodes of a graph satisfy a property. We investigate
the potential of a technique based on Computation
Tree Logic (CTL) model checking for evaluating
queries expressed in (a subset of) XPath. To this
aim, we isolate a simple fragment of XPath that
is naturally embeddable into CTL. We report on
experiments based on the model checker NuSMV,
and compare our results with alternative academic
XPath processors. We comment on the advantages
and drawbacks of the application of our model
checking-based approach to XPath processing.
|
 Additional Information
|
Citation:
Loredana Afanasiev, Massimo Franceschet, Maarten Marx, Maarten de Rijke,
"CTL Model Checking for Processing Simple XPath Queries,"
time,
pp. 117-124,
11th International Symposium on Temporal Representation and Reasoning (TIME'04),
2004
|
|
