Graph-transformation verification using monadic second-order logic

Kazuhiro Inaba, Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 Citations (Scopus)

Abstract

This paper presents a new approach to solving the problem of verification of graph transformation, by proposing a new static verification algorithm for the Core UnCAL, the query algebra for graph-structured databases proposed by Bunemann et al. Given a graph transformation annotated with schema information, our algorithm statically verifies that any graph satisfying the input schema is converted by the transformation to a graph satisfying the output schema. We tackle the problem by first reformulating the semantics of UnCAL into monadic second-order logic (MSO). The logic- based foundation allows to express the schema satisfaction of transformations as the validity of MSO formulas over graph structures. Then by exploiting the two established properties of UnCAL called bisimulation-genericity and compactness, we reduce the problem to the validity of MSO over trees, which has a sound and complete decision procedure. The algorithm has been efficiently implemented; all the graph transformations in this paper and the system web page can be verified within several seconds.

Original languageEnglish
Title of host publicationPPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming
Pages17-28
Number of pages12
DOIs
Publication statusPublished - 2011
Externally publishedYes
Event13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011 - Odense, Denmark
Duration: 2011 Jul 202011 Jul 22

Publication series

NamePPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming

Other

Other13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011
CountryDenmark
CityOdense
Period11/7/2011/7/22

Keywords

  • Graph transformation
  • Monadic second-order logic
  • UnCAL

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Applied Mathematics

Fingerprint Dive into the research topics of 'Graph-transformation verification using monadic second-order logic'. Together they form a unique fingerprint.

Cite this