Graph-transformation verification using monadic second-order logic
-
- Kazuhiro Inaba
- National Institute of Informatics, Tokyo, Japan
-
- Soichiro Hidaka
- National Institute of Informatics, Tokyo, Japan
-
- Zhenjiang Hu
- National Institute of Informatics, Tokyo, Japan
-
- Hiroyuki Kato
- National Institute of Informatics, Tokyo, Japan
-
- Keisuke Nakano
- The University of Electro-Communications, Tokyo, Japan
説明
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.
収録刊行物
-
- Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming
-
Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming 17-28, 2011-07-20
ACM