1Graph-Transformation
Verificationndusing Monadic 2 -Order Logic
Kazuhiro Inaba
with S. Hidaka, Z. Hu, H. Kato
(National Institute of Informatics, Japan)
Graphand K. Nakano(University of Electro-Communications)

PPDP 2011, OdenseGraph Transformation
GRoundTram ( www.biglab.org )2

Two Languages Involved
Transformation:
UnQL / UnCAL [Buneman&Fernandez&Suciu, 2000]
select {result: $x} where { _*: $x}, {name: John} in $x

Schema: KM3 [ATLAS Group]class INPUT{ reference SNS: SNSDB; … }class OUTPUT{ reference result*: MEM; }3

4

Today’s Topic: Static Check• Given– A graph transformation f– Input schema SI– Output schema So• Statically verify that “there’s no type error”,
i.e., “for any graph g conforming to SI ,f(g) always conforms to So.”

Example : SNS-Members
Extract all members using the screen-name “John”.
SNSmembernamefriend

・・・

friendnameselect {result: $x}
where{SNS: {member: $x}},{name: John} in $x

Mary・・・

friendname・・・

JohnJohn・・・

5

Example
Extract all members using the screen-name “John”.
SNSmembernamefriend・・・

friendnameselect {result: $x}
where{SNS: {member: $x}},{name: John} in $x

Mary・・・friend

name・・・

JohnJohn・・・

6

Example
Lazy programmer may write …
SNSmember

namefriend

・・・

friendnameselect {result: $x}
where{ _*: $x},
{name: John} in $x

Mary・・・

friendname・・・

JohnJohn・・・

7

Example
In fact, the graph contained “group” data, too!
SNSmember

namefriend

・・・

friend
name

name

name
“Fan Clubof XXX”

“JavaProgrammer”

・・・

Mary・・・

friendnameJohnJohn・・・

8

Example
What happens if there’s {group: {name: John, …}}SNS

membernamefriend
friendBUGGY!
name
name“Fan Clubof XXX”

name
“JavaProgrammer”

・・・

John

・・・
Mary

select {result: $x}
・・・
wherefriend{ _*:$x},name
John{name: John} in $x

・・・

910

What We Provide
Programmers specify their intention
about the structure of input/output.
class OUTPUT { reference result*: MEM; }// Input Schema supplied by the SNS provider

class INPUT { reference SNS: SNSDB; }class SNSDB
class MEM
class GRP

{ reference member*: MEM;
reference group*: GRP; }{ reference friend*: MEM;
reference name: STRING; }{ reference name: STRING;
reference member*: MEM; }11What We Provide
Then, our system automatically verify it!
class INPUT {reference SNS: SNSDB; }select {result: $x}
where{SNS: {member: $x}},{name: John} in $xclass OUTPUT {reference result*: MEM; }“OK!”※ Our checker is SOUND.
If it says OK, then theprogram never goes wrong.

12What We Provide
Then, our system automatically verify it!
class INPUT {reference SNS: SNSDB; }select {result: $x}
where{ _*: $x},
{name: John} in $x“BUG!”
SNSnameJohn

class OUTPUT {reference result*: MEM; }※ Our checker provides
a COUNTER-EXAMPLE.

13

Outline of the Rest of the Talk
How We Implemented This Verification–Monadic 2nd-Order Logic (MSO)–Schema to MSO–Transformations to MSO–Decide MSO: from Graphs to Trees

14

Overall Picture
KM3 Schema

MSO Logic[ATLAS Group]

UnQL / UnCALThisWork

MSO Definable
Transduction[Courcelle 94][Buneman, et.al. 00]

Bwd Inference

Nice Properties

MONA : MSO Solver[Møller, et.al. 95-]

15ndMonadic 2 -Order Logic
MSO is a usual 1st order logic on graphs …

edgefoo(x, e, y) start(x)(connectives) ￢P P&Q P∨Q ∀x.P(x) ∃x.P(x)(primitives)… extended with(set-quantifiers) ∀setS. P(S) ∃setS.P(S)(set-primitives)x∈SS⊆T

16

Schema to MSO• Straightforward
class OUTPUT { reference result*: MEM; }class MEM { reference friend*: MEM;
reference name: STRING; }∃setOUTPUT. ∃setMEM.
(∀x. start(x)  x∈OUTPUT)∧ (∀x∈OUTPUT. ∀e. ∀u.
edge(x,e,u)  edgeresult(x,e,u) & u∈MEM)∧…

17

Transformation to MSO
Q: What do we mean by“representing transformations in MSO”?
select {result: $x}
where{ _*: $x},
{name: John} in $x

edge[OUT]b (v, e, u) ⇔∃v’ e’ u’. edgea(v’,e’,u’) & v=v’ & e=e’ & u=e’edge[OUT]d (v, e, u) ⇔∃v’ e’ u’. ￢edgea(v’,e’,u’) & v=v’ & e=e’ & u=u’…

A: We convert UnQL’s functional core language
into a (kind of) logic program in MSO.

18

Transformation Language• “Core UnCAL”– Internal Representation of “UnQL” 

select {result: $x}
where{ _*: $x},
{name: John} in $x

E ::= {L1:E1, L2:E2, …, Ln:En}| if L=L then E else E| $G| &| rec(λ($L,$G). E)(E) | …
L ::= (label constant)
| $L

19

Semantics of rec in UnCAL
rec(λ($L,$G).
if $L = a then {b: {c: &}}else {d: $G})($input_graph)1

acbd1z1

1

1

2

if $L = a then {b: {c: &}}else {d: $G}
1

Decompose toa set of edges!

cb22z

Glue them!

2aa22z12dMore Precise, MSO-Representable“Finite-Copy” Semantics
if $L = a then {b: {c: &}}else {d: $G}

a1

2

1

Copy as needed!

22

Glue them!

bTransform towhat we want!
1cb

1c

2

edge[112]b (v, e, u) ⇔∃v’ e’ u’. edgea(v’,e’,u’) & v=v’ & e=e’ & u=e’edge[231]c(v, e, u) ⇔∃v’ e’ u’. edgea(v’,e’,u’) & v=e’ & e=e’ & u=u’

20

21

“Finite-Copy” Semantics
if $L = a then {b: {c: &}}else {d: $G}
121z
Copy as needed!
Transform towhat we want!
22d
Glue them!

d2edge[110]d(v, e, u) ⇔∃v’ e’ u’. ￢edgea(v’,e’,u’) & v=v’ & e=e’ & u=u’

22Transformation to MSO
Theorem:
Nest-free UnCAL is representable byfinite-copying MSO transduction.
rec(λ($L,$G).
if $L = athen {b: {c: &}}else {d: $G})($input_db)

edge[112]b (v, e, u) ⇔∃v’ e’ u’. edgea(v’,e’,u’) & v=v’ & e=e’ & u=e’edge[231]c (v, e, u) ⇔∃v’ e’ u’. edgea(v’,e’,u’) & v=e’ & e=e’ & u=u’edge[110]d (v, e, u) ⇔∃v’ e’ u’. ￢edgea(v’,e’,u’) & v=v’ & e=e’ & u=u’((Transformation = Definition ofthe output-graph in terms of the input graph))23“Backward” Inference [Courcelle 1994]
Output SchemaTransformation
rec(λ($L,$G).
if $L = a then {b: {c: &}} else {d: $G})($input_db)∃e. edgec(_, e, _)edge[112]b (v, e, u) ⇔ ∃v’ e’ u’. …
edge[231]c (v, e, u) ⇔∃e. edge[_0_]c (_, e, _)∨ edge[_1_]c (_, e, _)∨ edge[_2_]c (_, e, _)∨ edge[_3_]c (_, e, _)∃v’ e’ u’. edgea(v’,e’,u’) & … & e=e’edge[110]d (v, e, u) ⇔ ∃v’ e’ u’. …
InputSchema∃e. false∨ false∨ false∨ ∃v’ e’ u’. edgea(v’,e’,u’) & … & e=e’⇒∃e. edgea(_, e, _)24

Nested rec• Nested rec (arising from “cross product”)
cannot be encoded into finite-copy semantics
select {p: {f: $G1, s:$G2}}
where {_: $G1} in $db,{_ : $G2} in $db

Currently we ask
programmer toadd annotation rec(λ($L1,$G1).
rec(λ($L2,$G2).
{pair: {first: $G1, second: $G2}})($db))($db)rec(λ($L1,$G1). rec(λ($L2,$G2).
{pair: {first: ($G1 :: MEM),second: $G2}} …

25

Remark: Why MSO• It is expressive power is needed.
– Schemas can encode runs of automata, which isbasically equivalent to MSO.
– Transformation also requires MSO power, fortracking edge-erasing.

• It can be made decidable!
– In contrast to, e.g., FO+TCk that can capture
nested recs without annotation.

26

Two Nice Props of UnCAL[Buneman et al. 2000] UnCAL is …
aa

Bisimulation-generic Unfolding
aab・・・ ∞Cutac

UnCAL TransformationUnfolding

abc・・・ ∞CutCompacta・・・bbbccbc・・・

27

MSO Validation
Now we have a MSO Formula on Graphs.

!

MSO (even 1st-Order Logic) on Graphs
is undecidable [Trakhtenbrot 1950].
Theorem: If MSO formula is
Bisimulation-Generic and Compact, itis valid on graphs iff on finite trees.

MONA MSO Solver [Møller, et.al. 95-]
can decide validness of MSO on Finite Trees.

28Conclusion
Static verification of graph transformations via MSO
class INPUT {select {result: $x}reference SNS: SNSDB; }where { _*: $x},
{name: John} in $xclass OUTPUT {reference result*: MEM; }• Future work :MSO

“YES”/ “NO”+– Complete checking w/o annotations.
– Support for full UnCAL (with data value comparison).
– Use MSO-Transduction semantics for checking otherproperties.
– Comprehensive experiments on performance.