XML query evaluation via CTL symbolic model checking
Loredana Afanasiev · 2004
Abstract. The Extensible Markup Language (XML) was designed to describe the content of a document and its hierarchical structure. The XML Path language (XPath) is a language for selecting elements from XML documents. We propose and implement a linear embedding of the query evaluation problem for Core XPath, the navigational fragment of XPath, into the model checking problem for Computation Tree Logic (CTL). This allows us to evaluate Core XPath queries by exploiting a model checker for CTL. We report on experiments with the state-of-the-art model checker NuSMV, and compare our results with alternative academic XPath processors. 1