Title: MAPPING SPARQL QUERY TO TEMPORAL LOGIC QUERY BASED ON NµSMV MODEL CHECKER TO QUERY SEMANTIC GRAPHS

Issue Number: Vol. 1, No. 2
Year of Publication: 2011
Page Numbers: 332-345
Authors: Mahdi Gueffaz, Sylvain Rampacek, Christophe Nicolle
Journal Name: International Journal of Digital Information and Wireless Communications (IJDIWC)
- Hong Kong

Abstract:


The RDF (W3C standard for meta-modeling) language is the most frequently used to represent the semantic graphs. This paper presents a new research combining different fields that are: the semantic web and the model checking. We developed a tool, RDF2NµSMV, which converts RDF graphs into NµSMV language. This conversion aims checking the semantic graphs that have numerous errors of interpretation with the model checker NµSMV in order to verify the consistency of the data. The SPARQL query language is the standard for querying the semantic graph but have a lot of limitations. To this purpose, we define a translation from the SPARQL query language into the temporal logic query language. This language is a graph manipulation language implemented in our toolbox. This translation makes it possible to extend the expressive power of SPARQL naturally by adding temporal logic formulas characterizing sequences, trees, or general sub-graphs of the RDF graph. Our approach exhibits a performance comparable to dedicated SPARQL query evaluation engines, as illustrated by experiments on large RDF graphs. We developed the STL Resolver tool to resolve the temporal logic query. This tool is based on the model checker NµSMV algorithms.