Graph-transformation verification using monadic second-order logic

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

研究成果: Conference contribution

15 被引用数 (Scopus)

抄録

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.

本文言語English
ホスト出版物のタイトルPPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming
ページ17-28
ページ数12
DOI
出版ステータスPublished - 2011
外部発表はい
イベント13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011 - Odense, Denmark
継続期間: 2011 7 202011 7 22

出版物シリーズ

名前PPDP'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
国/地域Denmark
CityOdense
Period11/7/2011/7/22

ASJC Scopus subject areas

  • 計算理論と計算数学
  • 応用数学

フィンガープリント

「Graph-transformation verification using monadic second-order logic」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル