Modal-μ Definable
Graph Transduction
Kazuhiro Inaba
National Institute of Informatics, Japan

4th DIKU-IST Workshop, 2011

2/35

What We Want to Do
 Verification of Graph-to-Graph Transformations

ababf

A

BAB

 e.g., Queries on Graph-Structured Databaseor Transformations of XML with “id” links

3/35

What We Want to Do
 Verification of Graph-to-Graph Transformations

with respect to input/output specifications

φIN“From (a) we canreach (a) again.”
abafb

φOUT

“From (A) we canreach (A) again.”AA

verify whether or not:for any graph G, G ⊧ φIN ⇒ f(G) ⊧ φOUTBB

Verification by Pre-Image

4/35(a.k.a. “weakest precondition” or “inverse type inference”)

Given f and φOUT , compute invf(φOUT) such that:for any graph G, f(G) ⊧ φOUT iff G ⊧ invf(φOUT)
invf(φOUT)

φINf

φOUT

Then “for any graph G, G ⊧ φIN ⇒ f(G) ⊧ φOUT”
iff “for any graph G, G ⊧ (φIN → invf(φOUT ))”i.e., φIN → invf(φOUT ) is valid

5/35

To Be More Concrete…
 Which logic can we use for specifying φIN/OUT ?
 Must be strong enough to express useful conditions.
 Must be weak enough to have decidable validity.

 What kind of transformation f can be verified ?
 We must be able to compute the pre-image.

6/35

Our Approach Take Modal-μ Calculus as the specification logic
 (At least for trees) capture all existing XML-Schemas

 Define a new model of graph transformation

called Modal-μ Definable Transduction
 Pre-image of modal-μ sentence can be

fully automatically computed
 Expressive enough to capture(unnested) structural recursion on graphs

7/35

Related Work MSO (Monadic 2nd-Order Logic) Definable Transduction
 Overall structure is more or less the same.

 Ours is a proposal to use Modal-μ instead of MSO

 Hoare-Style Verification of Imperative Programs Ours don’t deal with pointers or destructive updates.
 Rather, it is more suitable forfunctional programs Structural recursion is handled
without any annotations
fun f( {$l: $x} ) = {cap($l) : g($x)}
fun g( {_: $x} ) = f($x){ φIN } f { φOUT }{ φIN }
p := root
while p != null doq := p.next
p.next := p.next.next
p := qend{ φOUT }8/35

Outline Two Kinds of Logics on Graphs
 Predicate Logics
 Modal Logics
 Why Modal-μ ?

 Review: Predicate-Logic Based Approach MSO-Definable Graph Transduction [Courcelle 94]

 Our Work: Modal-μ Definable Graph Transduction
 Computation of Pre-Image9/35

Graphs (in Today’s Talk) Σ : Finite Nonempty Alphabet
 G = (V, E, π)V

Set of Nodes
Set of Directed Edges
Labels on Nodes

E⊆V×V π : V → 2Σ

Σ = {a, b} π =V = { ab→ {a,b}ababab}→ {a}
→ {b}
→ {}

10/35Predicate Logics on Graphs
φ ::=FO| False | ￢ φ | φ ∨ φ| σ(x) (for σ∈Σ)“node x is labeled σ”| edge(x, y) “an edge connects x to y”| ∃x. φ“there’s x that makes ψ hold”| ∃S. φ “there’s a set S that makes ψ hold”| x ∈ S “x is in S”
MSO
We can define True, φ∧φ , φ→φ, ∀x.φ, and ∀S.φ.

11/35

Semantics
 For a graph G=(V,E,π) and an environment

Γ : Var→V G, Γ ⊧ σ(x)iff σ ∈ π(Γ(x))“node x is labeled σ”

 G, Γ ⊧ edge(x, y) iff (Γ(x), Γ(y)) ∈ E“an edge connects x to y”

 G, Γ ⊧ ∃x.φ iff there’s v∈V s.t. G,Γ[x:v] ⊧ φ…

12/35Modal Logics on Graphs
ψ ::=M| False | ￢ φ | φ ∨ φ| σ (for σ∈Σ) “current node is labeled σ”| ◇φ “current node has an outgoing edge
whose destination satisfies φ”|X| μX.φ “least fixpoint” (X must be in even # of ￢) MμWe Can Define: □φ (dual of ◇) and νX.φ (GreatestFixPt)

13/35Semantics
 For a graph G=(V,E,π), an environment

Γ : Var→2V, and the current node v ∈ V
 G, v, Γ ⊧ σiff σ ∈ π(v)“current node is labeled σ”

 G, v, Γ ⊧ ◇φ iff there’s w (v,w)∈E & G,w,Γ ⊧ φ“current node has an outgoing edge
whose destination satisfies φ”

 G, v, Γ ⊧ μY. φ

iff v ∈ LFP(F)where F(A) = {w∈V | G, w, Γ[Y:A] ⊧ φ}…

14/35

Examples “From the node x, we can reach a σ-node”∀S. ( (x∈S ∧ ∀y.∀z.(y∈S ∧(edge(y,z)→z∈S)))→ ∃y. (y ∈ S ∧ σ(y)))
 “Confluence”∀y. ∀z. ( edge(x,y) ∧ edge(x,z)→ ∃w. (edge(y,w) ∧ edge(z,w)) ) “From the current node, we can reach a σ-node”

μY. (σ ∨ ◇Y)
 “Confluence”(No way to express it in Modal-μ)MSO Definable (1-copying) Transduction[Courcelle 94]

15/35

A set of MSO formulas T =・ σOUT(x)for each σ∈Σ・ edgeOUT(x,y)
defines a transformation fT convertingG = (V, E, π) into G’ = (V, E’, π’) where π’( v ) = { σ | G, x:v ⊧ σOUT(x) } E’ = { (v, w) | G, x:v, y:w ⊧ edgeOUT (x,y) }16/35

Example (Σ = {a, b, A, B})
ababedgeOUT(x, y) ≡∃z.(edge(x,z)∧ edge(z,y))aOUT(x) ≡ bOUT(x) ≡ False
AOUT(x) ≡ a(x)BOUT(x) ≡ b(x)ABAB

17/35Pre-Image is Easily Obtainedabab

edgeOUT(x, y) ≡∃z.(edge(x,z)∧ edge(z,y))aOUT(x) ≡ bOUT(x) ≡ False
AOUT(x) ≡ a(x)BOUT(x) ≡ b(x)∀x. a(x) → ∃y.
∃z.(edge(x,z) ∧ edge(z,y))∧ a(y)

InlineExpansion

ABAB∀x. A(x) → ∃y.
edge(x,y)∧ A(y)

18/35

Expressiveness & Complexity
Modal◇φPSPACEFO∃x.φ
Undecidable

EXPTIMEμX.φ

Modal-μ∃S.φ

MSO

19/35

Expressiveness & Complexity(on “tree-like” graphs)
Modal
◇φ

PSPACEFO∃x.φ
NonElementary

EXPTIMEμX.φ

Modal-μ∃S.φ

MSO

20/35Modal-μ and MSO
 Complexity of Validity Checking
 Modal-μ : EXPTIME-complete MSO : Undecidable (Even in Trees, HyperEXP) Expressive Power Modal-μ = Bisimulation-Invariant Subset of MSO[Janin & Walukiewicz 96]
 “Bisimulation-Invariant” ≃“Physical equality of pointers cannot be checked”
 Not a severe restriction for purely functional
programs!

21/35Modal-μ Definable (1-copying) Transduction
A set of Modal-μ formulas T =・ σOUTfor each σ∈Σ・ edgeOUT an existential formula Fv={X}defines a transformation fT convertingG = (V, E, π) into G’ = (V, E’, π’) where π’( v ) = { σ | G, v ⊧ σOUT } E’ = { (v, w) | G, v, X:{w} ⊧ edgeOUT }22/35

Example (Σ = {a, b, A, B})aedgeOUT ≡ ◇◇Xbab

AaOUT ≡ bOUT ≡ False
AOUT ≡ a
BOUT ≡ ba → ◇◇a

BAA → ◇AB

23/35

Existential Formula A formula e with one free variable X isexistential, if
for all G=(V,E,π), v∈V, P⊆V
G, v, X:P ⊧ e iff ∃w∈P. G, v, X:{w} ⊧ e Examples: “X ∨ True”
 “◇X”

 “□X”
 “σ”

is not existential (Consider P={}).
is existential.
is not (when v is a leaf node …).
is not, but “X ∧ σ” is.24/35

Syntactic Condition
for all G=(V,E,π), v∈V, P⊆VG, v, X:P ⊧ e iff ∃w∈P. G, v, X:{w} ⊧ e Theorem:e is existential if it is in the following syntax
e ::= False | X | Y | e ∨ e | ◇e | μY. e| e ∧ φ where φ is any formula without free variables(True, ￢, σ, □, and GFP must be “guarded” by _ ∧ _)OPEN QUESTION: is this a necessary condition ?
(i.e., do all existential formulas have logically-equivalent forms in this syntax?)

25/35More Examples(Non-Examples) edgeOUT ≡ X

edgeOUT ≡ a

 edgeOUT ≡ μY. ((X ∧ a) ∨ ◇Y)

aaaedgeOUT ≡ X∧◇X edgeOUT ≡ μY. ((X ∧ a ∧ □b) ∨ (￢a ∧ ◇Y)bbaaba26/35Pre-Image Computation
For T = (σOUT, eOUT), define inv( False )= False inv( ￢ φ )= ￢ inv( φ ) inv( φ1 ∨ φ2 )= inv( φ1 ) ∨ inv( φ2 ) inv( σ )= σOUT inv( ◇ φ )= edgeOUT [X / inv(φ)]
 inv( Y )=Y inv( μY. φ )= μY. inv(φ)

Theorem: fT(G), v ⊧ φiff

G, v ⊧ inv(φ)

27/35

Proof of the Theorem
Theorem: fT(G), v ⊧ φiff

G, v ⊧ inv(φ)

 By Induction on φ. The essential case is:G, v ⊧ inv(◇φ)

iff G,v ⊧ edgeOUT [X / inv(φ)]
iff
iff
iff
iff

(definition of inv)

∃w (G,v,X:{w} ⊧ edgeOUT and G,w ⊧inv(φ)) (ext)∃w ((v,w) in E’ and G,w ⊧inv(φ))(def of E’)∃w ((v,w) in E’ and fT(G),w ⊧φ)(IH)
fT(G), v ⊧ ◇φ(definition of ◇)n-copying
Modal-μ Definable Transduction

28/35

A set of Modal-μ formulas T =・ σkOUTfor each σ∈Σ, k∈{1 .. n}・ edgeikOUT for each i, k∈{1 .. n} : existential
defines a transformation fT convertingG = (V, E, π) into G’ = (V*{1..n}, E’, π’) where π’( <v,k> ) = { σ | G, v ⊧ σkOUT } E’ = { (<v,i>, <w,k>)| G, v, X:{w} ⊧ edgeikOUT }29/35

Example (Σ = {a, b, A, B})
edge12OUT ≡ X
edge21OUT ≡ ◇Xabu ⊧ a → ◇bba1OUT ≡ A2OUT ≡ ab1OUT ≡ B2OUT ≡ botherwise ≡ Falseu ⊧ A2OUT →( edge21OUT [b1OUT]∨ edge22OUT [b2OUT] )AaBbBb<u,2> ⊧ A→◇b

30/35

Example Mutual structural recursion (withoutaccumulating parameters) can be dealt with.
 For the detail of structural recursion over graphs,see [Buneman, Fernandez & Suciu 00]
 fun ev( a fun ev( b fun od( a fun od( b1x)= A1x)= Bx ) =3 Ax ) =3 B

2Aod(x)

od(x)
ev(x)
4Bev(x)edge12OUT ≡ a ∧ X edge23OUT ≡ a ∧ ◇X
edge13OUT ≡ a ∧ ◇X
edge31OUT ≡ b ∧ ◇X
edge34OUT ≡ b ∧ X edge41OUT ≡ b ∧ ◇X

31/35Pre-Image Computation
 invk ( False, Δ ) = False
 invk ( ￢φ , Δ )= ￢ invk ( φ, Δ ) invk ( φ1∨φ2, Δ ) = invk ( φ1, Δ ) ∨ invk ( φ2, Δ ) invk ( σ, Δ )= σkOUT invk ( ◇φ, Δ )= ∨j∈{1..n} edgekjOUT [X / invj(φ, Δ)] invk ( Y, Δ )= Yk if k∈S invk ( Y, Δ )= μYk. invk( φ, Δ[Y→<S∪{k},φ>] )where (S,φ) = Δ(Y)
 invk ( μY.φ , Δ ) = μYk. invk( φ, Δ[Y→<{k},φ>] )Thm: fT(G), <v,k> ⊧ φiff

G,v ⊧ invk(φ, {})32/35

Exampleedge11OUT ≡ edge12OUT ≡ edge21OUT ≡ edge22OUT ≡ ◇X
a1OUT ≡ a2OUT ≡ a
OPEN QUESTION: caninv(μ) be shorter
than (n-1)!+1 ?

⊧ μY. (a ∧ ◇Y)
 G, v ⊧ μY1. inv1( a ∧ ◇Y )
 G, v ⊧ μY1.
a ∧ (◇inv1(Y) ∨ ◇inv2(Y))
 G, v ⊧ μY1. a ∧ (◇Y1 ∨ ◇μY2.inv2(a∧◇Y)) G, v ⊧ μY1. a ∧ (◇Y1 ∨ ◇μY2. a∧(◇inv1(Y)∨◇inv2(Y))
 G, v ⊧ μY1. a ∧ (◇Y1 ∨ ◇μY2. a∧(◇Y1∨◇Y2))
 f(G), <v,1>

33/35

Some Useful Results
Theorem:
Modal-μ Definable Transduction isclosed under composition.
Construction is analogous to inv(φ).

Theorem:
Modal-μ Definable Transduction⇔ MSO Definable & Bisimulation-Invariant.
It is known that Bisimulation-Invariant MSO transduction isequal to structural recursion [Colcombet & Löding 04].

34/35Conclusion
 Modal-μ Definable Transduction Pre-Image of a modal-μ sentence is computable
 Structural recursion is expressible
 (Not in the talk) Node-erasing transformations
 Edge-labeled graphs
 Transformations with multiple inputs/outputs

 Future Work Implementation
 Addition of Backward Modality ( G,v ⊧ ◆φiff
there’s (w,v)∈E s.t. G,w ⊧ φ ) Syntactic necessary condition for edgeOUT
 More concise formula for inv(μY.φ)35/35

References[Trakhtenbrot 50] Impossibility of an Algorithm for the Decision Problem for Finite Classes
Satisfiability of FO on graphs is undecidable[Meyer 74] Weak monadic second order theory of successor is not elementary-recursiveSatisfiability of MSO on finite strings is Non-Elementary[Robertson 74] Structure of Complexity in the Weak Monadic Second-Order Theories of the NaturalNumbersSatisfiability of FO[<] on finite strings is Non-Elementary[Lander 77] The Computational Complexity of Provability in Systems of Propositional Modal Logic

Satisfiability of Modal Logic on graphs is PSPACE-complete[Emereson & Jutla 88] The Complexity of Tree Automata and Logics of ProgramsSatisiability of Modal-μ on graphs is EXPTIME-complete[van Benthem 86] Essays in Logical Semantics
FO ∩ Bisim = Modal[Janin & Walukiewicz 96] On the Expressive Completeness of the Propositional mu-Calculus withRespect to Monadic Second Order Logic

MSO ∩ Bisim = Modal-μ[Colcombet & Löding 04] On the Expressiveness of Deterministic Transducers over Infinite TreesMSO-Definable Graph Transduction ∩ Bisim = Structural Recursion[Courcelle 94] Monadic Second-Order Definable Graph Transductions: A Survey
On MSO-Definable Transduction