CTL model checking for processing simple XPath queries

The Extensible Markup Language (XML) wasdesigned to describe the content of a documentand its hierarchical structure, and the XML Pathlanguage (XPath) is a language for selecting elementsfrom XML documents. There is a close connectionbetween the query processing problem forXPath and the model checking problem for temporallogics. Both boil down to checking whichnodes of a graph satisfy a property. We investigatethe potential of a technique based on ComputationTree Logic (CTL) model checking for evaluatingqueries expressed in (a subset of) XPath. To thisaim, we isolate a simple fragment of XPath thatis naturally embeddable into CTL. We report onexperiments based on the model checker NuSMV,and compare our results with alternative academicXPath processors. We comment on the advantagesand drawbacks of the application of our modelchecking-based approach to XPath processing.