- CTL model checking for processing simple XPath queries
- Book title
- Proceedings Temporal Representation and Reasoning (TIME 2004)
- IEEE Computer Society Press
- Document type
- Faculty of Science (FNWI)
Faculty of Social and Behavioural Sciences (FMG)
- Informatics Institute (IVI)
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.
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.