1Graph Query Verification
using
ndMonadic 2 -Order Logic
Graph

Kazuhiro Inaba (稲葉 一浩)
kinaba@NII.ac.jp
Oct 10, 2010
1st PKU-NII International Joint Workshop
on Advanced Software Engineering

Goal of This Research(Automated) Reasoning
on Graph Transformations
Is this update on the output
reflectable to the input?

Does the output of thistransformation always
have a desired structure?

2

Today’s Talk
• 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.”

3

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・・・

4

Example
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
Lazy programmer may write …
SNS

membernamefriend

・・・

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

Mary・・・friend

name・・・

JohnJohn・・・

6

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

friend
name

name

name
“Fan Clubof XXX”

“JavaProgrammer”

・・・

Mary

・・・

friendname

JohnJohn・・・

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

membernamefriendfriendBUGGY!
name
name“Fan Clubof XXX”

name
“JavaProgrammer”

・・・

John・・・
Mary

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

8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; }910What 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.

11

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

12How?
By encoding transformations into a logic formula.
class INPUT {reference SNS: SNSDB; }select {result: $x}
where{ _*: $x},
{name: John} in $xclass OUTPUT {reference result*: MEM; }formulaCheck VALIDNESS
using
an existing verifier“YES”/ “NO”+CE
Decode CE toa graph

13

The Challenge“How should we represent
schemas and transformations
by logic formulas?”– The logic must not be too strong(otherwise its validness becomes undecidable)– The logic must not be too weak(otherwise it cannot talk about our schemas and transformations)– What is the “just-fit” logic?

14Rest of the Talk
• Our Choice– Monadic 2nd-Order Logic (MSO)• Schema Language– How it can be represented in MSO• UnCAL Transformation Language– How, in MSO• Decide MSO: from Graph-MSO to Tree-MSO• Discussion : Why This Approach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

Graph Schema Language• Programmers can specify
any MSO-expressible property(as long as it is bisimulation-generic & compact)• For example,(count-free subset of) KM3 MetaModeling Language:class OUTPUT { reference result*: MEM; }class MEM { reference friend*: MEM;
reference name+: STRING; }17

Schema to MSO• We do need MSO’s expressivenessclass 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)∧…

18

Transformation Language• UnCAL [Buneman et al, 2000]– Internal Representation of “UnQL” 

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

E ::= {L:E, L:E, …, L:E}
| if L=L then E else E| $G| &| rec(λ($L,$G). E)(E)
L ::= (label constant)
| $L

19

“Bulk” Semantics of UnCAL
rec(λ($L,$G).
if $L = a then {b: {c: &}}else {d: $G})($input_db)

1acbd1z

1

1

1

2

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

Decompose toa set of edges!

cb
2

2z

Glue them!

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

a1

1

Copy as needed!

2

2

Glue them!

bTransform towhat we want!
1cb

2

20

1c

2

edgeb(v,e,u) ⇔∃v’ e’ u’. edgea(v’,e’,u’) & v=v’1 & e=e’1 & u=e’2
edgec(v,e,u) ⇔∃v’ e’ u’. edgea(v’,e’,u’) & v=e’2 & e=e’3 & e=u’1

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

d2edged(v,e,u) ⇔∃v’ e’ u’. ￢edgea(v’,e’,u’) & v=v’1 & e=e’1 & u=u’

22Transformation to MSO
Theorem:
Nest-free UnCAL is representable byfinite-copying MSO transduction.

rec(λ($L,$G).
if $L = athen {b: {c: &}} edgeb(v,e,u) ⇔ edgea(v’,e’,u’) & v=v’1 & e=e’1 & u=e’2
edgec(v,e,u) ⇔ edgea(v’,e’,u’) & v=e’2 & e=e’3 & e=u’1
else {d: $G})($input_db)
edged(v,e,u) ⇔ ￢edgea(v’,e’,u’) & v=v’1 & e=e’1 & u=u’((Transformation = Definition ofthe output-graph in terms of the input graph))23“Backward” Inference [Courcelle 1994]
OUTPUT GRAPH description
by the INPUT GRAPHMSO Formula stating“output conforms to the schema”
in terminology of OUTPUT GRAPHS

rec(λ($L,$G).
if $L = a then {b: {c: &}} else {d: $G})($input_db)

class OUTPUT { reference result*: MEM; }class MEM { reference friend*: MEM;
edge
reference name: STRING;} b(v,e,u) ⇔ edgea(v’,e’,u’) & v=v’1 & e=e’1 & u=e’2∃setOUTPUT.

∃setMEM.

edgec(v,e,u) ⇔ edgea(v’,e’,u’) & v=e’2 & e=e’3 & e=u’1
edged(v,e,u) ⇔ ￢edgea(v’,e’,u’) & v=v’1 & e=e’1 & u=u’(∀x. start(x)  x∈OUTPUT)∧ (∀x∈OUTPUT. ∀e. ∀u.
edge(x,e,u)  edgeresult(x,e,u) & u∈MEM) ∧ …

Verify this isvalid for anyINPUT GRAPHS!!

MSO Formula stating“output conforms to the schema”
in terminology of INPUT GRAPHS: edge(v’,e’,u’)24Note: Harder Case• Nested Recursion (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(why we need the power of MSO?)• E.g., for “regular path pattern”
select {result: $x}
where{ _*: $x},
{name: John} in $x

select {result: $x}
where{ (a|b).(c|d)*: $x},
{name: John} in $x• MSO can encode finite automata∃set Q1. ∃set Q2. … ∃set Qn. “there is a runof the automaton that reaches states
Q’s on each node”

26

MSO Validation
Now we have a MSO Formula on Graphs.

?

MSO (even 1st-Order Logic) on Graphs
is undecidable [Trakhtenbrot 1950].

MONA [Henriksen et al., 1995]
can decide validness of MSO on Finite Trees.

27

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

Bisimulation-generic Unfolding
aab・・・ ∞Cutac

UnCAL Transformation

Unfoldingabc・・・ ∞CutCompacta・・・bbbccbc・・・

28

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 [Henriksen et al., 1995]
can decide validness of MSO on Finite Trees.

29Discussion: Choice of Logic• MSO– Powerful, yet decidable (if we fully utilize bisimulation)• FO+TC (1st-Order Logic + Transitive Closure)– Very powerful; express all UnCAL without annotation– Undecidable, even on finite trees• FO (1st-Order), SMT (Satisfiability Modulo Theory)– Very good solvers– Too weak for schemas or UnCAL; cannot use repetition• mu-Calculus (Modal Logic with Fixpoint)– Theoretically, equal to MSO under bisimulation– Not clear how to represent transformations

30Discussion: Approach• Our Approach– “Backward” (define the output by the input, with logic)• Other Possible Approaches– “Forward” (e.g., abstract interpretation)• [Buneman et al., 1997] [Nakano, Today!]• Better in range analysis. Worse in counterexample generation.

– “Type System”• Hard, because we need context-dependent types, etc.
• Two $G may differ in types: if $L=a then …$G… else …$G…

31

SummaryVerify “type-correctness” of graph transformationsvia Monadic 2nd-Order Logic
class INPUT {{result:}$x}
reference selectSNS: SNSDB;
where { _*: $x},
{name: John} in $xclass OUTPUT {reference result*: MEM; }MSO“YES”/ “NO”+• MSO and bisimulation are good tools for graphs!
• Future work : checking other properties