Mapping SPARQL Query to temporal logic query based on NμSMV Model Checker to Query Semantic Graphs

International audienceThe RDF (W3C standard for metamodeling) 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