Paper Info
Title
CTL Model Checking for Processing Simple XPath Queries
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.
Year
Venue
Keywords
2004
Studia Logica
model checker nusmv,alternative academic xpath processor,xml path language,xpath processing,computation tree logic,model checking,query processing problem,model checking-based approach,ctl model checking,model checking problem,simple xpath queries,xml document,xml documents,query languages,logic,informatics,extensible markup language,data models,temporal logic,databases,tree graphs,xml
Field
DocType
ISBN
Computation tree logic,Model checking,Programming language,XML Schema (W3C),Computer science,Path expression,XML Path Language,Theoretical computer science,Schematron,XPath,XPath 2.0
Conference
0-7695-2155-X
Citations 
PageRank 
References 
20
0.82
20
Authors
4
Name
Order
Citations
PageRank
Loredana Afanasiev11297.94
Massimo Franceschet265839.91
Maarten Marx3137297.86
Maarten de Rijke46516509.76