loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
11th International Symposium on Temporal Representation and Reasoning (TIME'04)
CTL Model Checking for Processing Simple XPath Queries
Tatihou, Normandie, France
July 01-July 03
ISBN: 0-7695-2155-X
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
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.
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
Usage of this product signifies your acceptance of the Terms of Use.