摘要：In this paper, we show the process inspired by model checking whichintegrate temporal logic to the application of semi-structured data query. Weinvestigate the potential of a technique based on CTL (Computation Tree Logic)model checking for evaluating queries expressed in (a subset of) XPath. Our researchconsists of query algebra, constraint understanding and expression mapping. Thecore of research is mapping the XML query algebra to an expression collection oftemporal logic. We try a new kind of query execution strategy to enhance the accuracyof semantic description of the XML query. For the purpose of supporting thegeneration of the formal specifications and reducing the mapping processing, theXML query constraint can be converted to a specification of SPS (SpecificationPattern System) through which we get the formula set to evaluate path queriesdirectly on CTL formula.
关键词：XML; model checking; Xpath; temporal logic; SPS.
