TY - GEN

T1 - Graph-transformation verification using monadic second-order logic

AU - Inaba, Kazuhiro

AU - Hidaka, Soichiro

AU - Hu, Zhenjiang

AU - Kato, Hiroyuki

AU - Nakano, Keisuke

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

KW - Graph transformation

KW - Monadic second-order logic

KW - UnCAL

UR - http://www.scopus.com/inward/record.url?scp=80052173451&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=80052173451&partnerID=8YFLogxK

U2 - 10.1145/2003476.2003482

DO - 10.1145/2003476.2003482

M3 - Conference contribution

AN - SCOPUS:80052173451

SN - 9781450307765

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

SP - 17

EP - 28

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

T2 - 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011

Y2 - 20 July 2011 through 22 July 2011

ER -