<abstract xmlns="http://www.w3.org/1999/xhtml"><p> In this paper, we show the process inspired by model checking which integrate temporal logic to the application of semi-structured data query. We investigate the potential ofatechnique based on CTL (Computation Tree Logic) model checking for evaluating queries expressed in (a subset of) XPath. Our research consists of query algebra, constraint understanding and expression mapping. The core of research is mapping the XMLquery algebra to an expression collection of temporal logic. We tryanew kind of query execution strategy to enhance the accuracy of semantic description of the XMLquery. For the purpose of supporting the generation of the formal specifications and reducing the mapping processing, the XMLquery constraint can be converted toaspecification of SPS (Specification Pattern System) through which we get the formula set to evaluate path queries directly on CTLformula.</p></abstract>

In this paper, we show the process inspired by model checking which integrate temporal logic to the application of semi-structured data query. We investigate the potential ofatechnique based on CTL (Computation Tree Logic) model checking for evaluating queries expressed in (a subset of) XPath. Our research consists of query algebra, constraint understanding and expression mapping. The core of research is mapping the XMLquery algebra to an expression collection of temporal logic. We tryanew kind of query execution strategy to enhance the accuracy of semantic description of the XMLquery. For the purpose of supporting the generation of the formal specifications and reducing the mapping processing, the XMLquery constraint can be converted toaspecification of SPS (Specification Pattern System) through which we get the formula set to evaluate path queries directly on CTLformula.

An Approach of XML Query Evaluation Based Model Checking

College of Computer Science and Technology, Harbin Engineering University, Harbin 150001,

Cybernetics and Information Technologies

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.

{"article-title":"An Approach of XML Query Evaluation Based Model Checking"}

In this paper, we show the process inspired by model checking which integrate temporal logic to the application of semi-structured data query. We investigate...

An Approach of XML Query Evaluation Based Model Checking

Published Online: Dec 22, 2016

Page range: 45 - 54

DOI: https://doi.org/10.1515/cait-2016-0066

Keywords
XML, model checking, Xpath, temporal logic, SPS

© by Li Yan-Mei

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.

An Approach of XML Query Evaluation Based Model Checking

Published Online: Dec 22, 2016

Page range: 45 - 54

DOI: https://doi.org/10.1515/cait-2016-0066

KeywordsXML, model checking, Xpath, temporal logic, SPS

© by Li Yan-Mei

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.

Keywords
XML, model checking, Xpath, temporal logic, SPS