Paper Info
Title
Graph-transformation verification using monadic second-order logic
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.
Year
DOI
Venue
2011
10.1145/2003476.2003482
PPDP
Keywords
Field
DocType
schema information,graph structure,monadic second-order logic,algorithm statically verifies,mso formula,output schema,core uncal,schema satisfaction,input schema,new static verification algorithm,graph transformation,graph-transformation verification,web pages,satisfiability
Programming language,Web page,Computer science,Compact space,Theoretical computer science,Null graph,Graph rewriting,Clique-width,Schema (psychology),Semantics,Monad (functional programming)
Conference
Citations 
PageRank 
References 
10
0.58
20
Authors
5
Name
Order
Citations
PageRank
Kazuhiro Inaba11028.07
Soichiro Hidaka218514.89
Zhenjiang Hu3134199.25
Hiroyuki Kato41288.75
Keisuke Nakano521224.62