Sound & Complete Validation of Graph

Sound & Complete Validation of
Graph Transformations
稲葉一浩、日高宗一郎、胡振江、加藤弘之（NII）、中野圭介（電通大）
a
b b
d
a
a
スキーマ SI
c
目的：
グラフ変換が意図した構造変換を行う
d
こと ∀g∈S I .
f(g)∈S O
の静的保証
スキーマ SO 対象言語：
type T {a:{} b:S}
type S {a: T∨{} }
type R {c:{}
d:R∨{} }
変換> UnCAL [Bunemanら 00] のSubset
スキーマ>
KM3 [ATLAS group 04] like
UnCAL Subset e ::= {l:e, …, l:e} | $g | if l = l then e else e | &i | rec( λ($l,$v). e, …, e )(e)
l ::= $l | L
L ∈ ラベル名
Schema s ::= type T {L : t …} …
t ::= {} | T | t∨t
T ∈ 型名
手法：保証したい性質を、恒真性が決定可能なLogicの論理式で表現
UnCALの持つさまざまな良い性質の、検証への応用
a
b
d
b
a a
b b
a
a
d
c
c
d
d
a
a
b
b
✂
✂
✂
a
b
b
a
a
†
✂
✂
Compact 無限木Tから有限木tへ
†
t∈cut(T) ⇒ f (t)∈cut(f(T))
†
∀t
∈
cut(f(T)).
∃t
∈cut(T).
t
≺
f
(t
)
O
I
O
I
c
c
✂
d
✂
d
✂
t ⊧ “t satisfies SI
†
†
⇒ “f (t) satisfies SO ”
†”
Bisimulation-Generic グラフgから無限木Tへ
g～T ⇒ f(g) ～ f(T)
g～T ⇒ (g∈S ⇔ T∈S)
∴ ∀g∈SI. f(g)∈SO ⇔∀T∈SI. f(T)∈SO
…
†
†
†
∴ ∀T∈SI. f(T)∈SO ⇔∀t∈SI . f (t)∈SO
MSO-Definable 有限木変換からLogicへ
関数内関数のないUnCALは MSO (単項
二階論理)変換 [Courcelle94]で記述可能
(有限)木上 MSO の恒真性は決定可能
今後の課題： (1) 実装効率向上
(2) 対象言語拡大（関数内関数、“isEmpty”、個数制約 e.g., type T{a[1..3]:T} ）

Download Report