Journal of Software, Vol 7, No 7 (2012), 1462-1472, Jul 2012
doi:10.4304/jsw.7.7.1462-1472

Temporal Logic To Query Semantic Graphs Using The Model Checking Method

Mahdi Gueffaz, Sylvain Rampacek, Christophe Nicolle

Abstract


Semantic interoperability problems have found their solutions due to the use of languages and techniques from the Semantic Web. The proliferations of ontologies and meta-information have improved the understanding of information and the relevance of search engine responses. However, the construction of semantic graphs is a source of numerous errors of interpretation or modeling, and scalability remains a major problem. The processing of large semantic graphs is a limit to the use of semantics in current information systems. The work presented in this paper is part of a new research at the border of two areas: the semantic web and the model checking. This line of research concerns the adaptation of model checking techniques to semantic graphs. We present a first method of converting RDF (Resource Description Framework) graphs into NμSMV and PROMELA (Process Meta Language) languages in order to be checked with the temporal logic property and queried by the temporal logic query.  SPARQL (Simple Protocol and RDF query Language) query language is the standard for querying the Semantic Web, but it has a lot of limitations. Our primary goal with the temporal logic query is to overcome this limitation of the SPARQL query language. To reach this goal, three tools have been developed. The first two tools “RDF2SPIN” and “RDF2NµSMV” are used to transform the Semantic graph into a model written in PROMELA and respectively in NµSMV languages – in order to be understood by the SPIN and respectively the NµSMV model checkers. The STL Resolver tool is used to find solutions to the temporal logic query. It is based on the model checking algorithms.   


Keywords


Semantic graph; model checking; temporal logic; temporal logic query; SPARQL

References


 

[1] T. Bray, J. Paoli, C. Sperberg-McQueen. M., Maler, E., Yergeau, F., Cowan, J.: Extensible Markup Language (XML) 1.1 (second edition) W3C recommendation. (2006)

[2] T. Berners-Lee, J. Hendler, and O. Lassila. The Semantic Web. Scientific American. pp. 34–43. (2001)
http://dx.doi.org/10.1038/scientificamerican0501-34

[3] J. Kahan, M. Koivunen, E. Prud'Hommeaux, R. R. Swick. Annotea: An Open RDF Infrastructure for Shared Web Annotations, in Proc. of the WWW 10th International Conference, Hong Kong. (2001)

[4] J. P. Katoen: The princiapl of Model Checking. University of Twente. (2002)

[5] K. Homma, K. Takahashi, A. Togashi. Modeling and Verification of Web Applications Using Formal Approach. IEICE Tech. Rep., vol. 109, no. 40, SS2009-8, pp. 43-48. (2009)

[6] A. Pnueli. The temporal logic of programs. In proc. 18th IEEE Symp. Foundations of Computer Science (FOCS’77), Providence, RI, USA. pages 46-57. (1977)

[7] W. Chan. “Temporal-Logic Queries,” Proc. 12th Conf. Computer Aided Verification (CAV ’00), pp. 450-463, July 2000.

[8] R. Angles and C. Gutierrez. Querying RDF Data from a Graph Database Perspective. 2nd. European Semantic Web Conference (ESWC2005), May 2005, Heraklion, Greece. Lecture Notes in Computer Science, Volume 3532, pp. 346-360. 2005

[9] G. Karvounarakis, S., Alexaki, V. Christophides, D. Plexousakis, M. Scholl. RQL: A Declarative Query Language for RDF. In: Proc. of the 11th WWW conference, ACM Press. Pages 592–603. 2002.

[10] A. Seaborne. RDQL - A Query Language for RDF, W3C Member Submission 9 January 2004. http://www.w3.org/Submission/2004/SUBM-RDQL-20040109/

[11] M. Sintek, S. Decker. TRIPLE - A Query, Inference, and Transformation Language for the Semantic Web. Proc. of the 1th ISWC (2002)

[12] T. Berners-Lee. Notation 3 - An RDF Language for the Semantic Web. http://www.w3.org/DesignIssues/Notation3 (2001)

[13] A. Magkanaraki, G. Karvounarakis, T.T. Anh, V. Christophides, D. Plexousakis. Ontology Storage and Querying. Tech. Report 308, ICS-FORTH - Hellas (2002)

[14] P. Haase, J. Broekstra, A. Eberhart, R. Volz. A Comparison of RDF Query Languages. In: Proc. of the 3th ISWC conference. Number 3298 in LNCS, Springer-Verlag 502 (2004)

[15] E. Prudhommeaux, A. Seaborne. SPARQL Query Language for RDF. http://www.w3.org/TR/rdf-sparql-query/ (2005)

[16] D. Becket, B. McBride: RDF/ XML Syntax Specification (Revised). W3C recommendation. (2004)

[17] T. Berners-Lee. W3C recommandation. (2007)

[18] V. Bönström, A. Hinze, H. Schweppe: Storing RDF as a graph. Latin American WWW conference, Santiago, Chile. (2003)

[19] A. Chebotko, S. Lu, H. M. Jamil, and F. Fotouhi. Semantics Preserving SPARQL-to-SQL Query Translation for Optional Graph Patterns. Technical report, Wayne State University, TR-DB-052006-CLJF, 2006.

[20] M. Mukund. Model Checking: Automated Verification of Computational Systems. Pages 667-681. (2009)

[21] S. Bardin. Introduction to the Model Checking. CEA,LIST, Safety Software laboratory. 2008

[22] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.

[23] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of the Workshop on Logics of Programs, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer-Verlag, 1981.
http://dx.doi.org/10.1007/BFb0025774

[24] JP. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th International Symposium on Programming, volume 137 of Lecture Notes in Computer Science, pages 337–350. Springer-Verlag, 1982.
http://dx.doi.org/10.1007/3-540-11494-7_22

[25] A. Gurfinkel, B. Devereux and M. Chechik. Model exploration with temporal logic query checking. SIGSOFT 2002/ FSE-10, 2002.

[26] A. Gurfinkel, M. Chechik and B. Devereux. Temporal logic query checking: a tool for model exploration. IEEE computer society. (2003)

[27] R. Mateescu, S. Meriot, S. Rampacek. Extending SPARQL with Temporal logic. Technical report. (2009)

[28] S. Hornus and Ph. Schnoebelen. On solving temporal logic queries. Algebraic Methodology and Software Technology. Lecture Notes in Computer Science, Volume 2422/2002, pages 73-89. 2002.

[29] M. Gheorghiu and A. Gurfinkel. TLQ: A query solver for states. 2006.

[30] S. Hornus and Ph. Schnoebelen. Queries in temporal logic. Technical report. 2009.

[31] A. Cimatti, E. Clarke, F. Giunchiglia, M. Roveri. NµSMV: a new symbolic model checker. (2000)

[32] M. Ben-Ari. Principles of the SPIN Model Checker. Springer. ISBN: 978-1-84628-769-5. (2008)

[33] R. E. Tarjan: Depth-First search and linear graph algorithm. SIAM Journal of Computing 1, 2, 146-160. (1972).
http://dx.doi.org/10.1137/0201010

[34] M. Schmidt. Fondations of SPARQL query optimization. PhD Thesis, Albert-Ludwigs-Universität Freiburg (Germany) 2009.

[35] J. Pérez, M. Arenas, and C. Gutierrez. Semantics and Complexity of SPARQL. Best Paper Award, 5th International Semantic Web Conference, ISWC 2006.

[36] T. Neumann and G. Weikum. Scalable Join Processing on very large RDF graphs. SIGMOD’09. (2009)

[37] G. Lausen, M. Meier and M. Schmidt. SPARQLing Constraints for RDF. In EDBT, pages 499–509, 2008.

[38] A. Polleres, F. Scharffe, and R. Schindlauer. SPARQL++ for Mapping Between RDF Vocabularies. On the Move to Meaningful Internet Systems 2007: CoopIS, DOA, ODBASE, GADA, and IS, pages 878–896, 2007.

[39] ARQ SPARQL Processor for Jena. http://jena.sourceforge.net/ARQ/.

[40] C. Blakeley. Mapping Relational Data to RDF with Virtuoso’s RDF Views, 2007. OpenLink Software. (2007)

[41] K. Kochut and M. Janik. SPARQLeR: Extended SPARQL for Semantic Association Discovery. In ESWC, pages 145–159, 2007.

[42] J. Pérez, M. Arenas, and C. Gutierrez. nSPARQL: A Navigational Language for RDF. In ISWC, pages 66–81, 2008.

[43] F. Alkhateeb, JF. Baget, and J. Euzenate. Extending SPARQL with regular expression patterns (for querying RDF). Web Semantics, 7(2):57–73, 2009.
http://dx.doi.org/10.1016/j.websem.2009.02.002

[44] B. Vatant. Metadata to describe resources (Semantic Web Languages). In Proceedings of the INRA Seminar : Metadata: changes and prospects. (2008)


Full Text: PDF


Journal of Software (JSW, ISSN 1796-217X)

Copyright @ 2006-2013 by ACADEMY PUBLISHER – All rights reserved.