=Paper=
{{Paper
|id=None
|storemode=property
|title=On a Dynamic Logic for Graph Rewriting
|pdfUrl=https://ceur-ws.org/Vol-1000/ICTERI-2013-p-506-520-SMSV.pdf
|volume=Vol-1000
|dblpUrl=https://dblp.org/rec/conf/icteri/WinckelM13
}}
==On a Dynamic Logic for Graph Rewriting==
https://ceur-ws.org/Vol-1000/ICTERI-2013-p-506-520-SMSV.pdf
On a Dynamic Logic for Graph Rewriting ?
Mathias Winckel and Ralph Matthes
Institut de Recherche en Informatique de Toulouse (IRIT)
{winckel, matthes}@irit.fr
Abstract. Initially introduced by P. Balbiani, R. Echahed and A.
Herzig, this dynamic logic is useful to talk about properties on ter-
mgraphs and to characterize transformations on these graphs. Also are
presented the deterministic labelled graphs for which the logical frame-
work is designed.
This logic has been the starting point of a formal development, using the
Coq proof assistant, to design a logical and algorithmic framework useful
for verifyin and proving graph rewriting. The formalization allowed us to
figure out some ambiguities in the involved concepts. This formalization
is not the topic here but the clear view brought to us by the formal work,
so the results will be expressed using the original mathematical objects
of this logic.
Some problems of this logic are demonstrated, relatively to the repre-
sentation of graph rewriting. Some are minor issues but some are far
more important for the adequation between the formulas about graph
rewriting and the actual rewriting systems. Invalidating some resulting
propositions, solutions are given to reestablish the logical characteriza-
tion of graph rewriting, which was the initial purpose.
Keywords. Dynamic Logic, Graph Rewriting, Adequation Issues
Key terms. Formal Method, Model
1 Introduction
Nearly every field of computer science uses graphs to represent data or the
behavior of systems. Then, to get a higher level of dynamics, it uses rewriting
in a more or less formal way to handle manipulation of such objects. In some
fields, as in Formal Methods and Model-Driven Engineering, graphs are one of
the main tools, having advanced methods to express and reason on these graphs
is of great pertinance.
Modal logic allows to express relational properties naturally and, with Kripke
semantics, is closely linked to graphs which are its models. Yet, instead of dis-
cussing graphs and rewriting using hyper-graphs as models, the transformed
?
This work has been funded by the CLIMT project (ANR-11-BS02-016 of the French
Agence Nationale de la Recherche)
On a Dynamic Logic for Graph Rewriting 507
graphs could be directly these models. Dynamic logic as defined by D. Harel
offers by its modalities the possibility to express relations on models when they
have some desired properties. In this spirit, introduced during ICGT 2010, “A
Dynamic Logic for Termgraph Rewriting” [1] was proposed by P. Balbiani, R.
Echahed and A. Herzig as a suitable dynamic logic to describe graphs and
transformations on these graphs.
The termgraph lifts the concept of term to the more general one of graph. It
was initially introduced to represent terms while having a simpler way to talk
about recursion or sharing of sub-terms, what a tree-like structure doesn’t allow
to do easily.
Computer science involves data structures that are usually syntactically rep-
resented as simple terms. It is interesting to develop such a tool for more than
just a graphic representation: using graph rewriting, research could be done on
term rewriting with this rich and powerful layer of language of graph structure.
In the following, in Section 2 we will present the type of graphs we use, then
in Section 3 the dynamic logic for graph rewriting, its syntax and its semantics.
In Section 4 the rewriting system is presented, and propositions to logically talk
about it, but with issues to express these concepts with the logic as originally
introduced. Graph homomorphisms, rewriting steps and application to a graph,
with the definition of rewriting rules, matching of rules and normal forms, actu-
ally leads to some divergences between actual rewriting and its translation using
the logic. Section 4 also discuss and proposes some solutions for these original
issues, for such an utilisation.
2 Termgraph And Rooted Termgraph
To illustrate terms representation as graphs from some typical λ-calculus, as
shown in Figure 1, a classical tree-like term in (a), an example of argument
sharing in (b), and eventually a representation for a fixpoint operator in (c),
usually denoted Y for a function f [2]. One can easily unfold the recursion in
the latter graph and get Y f = f (Y f ), which is what is expected from a
fixpoint operator.
The graphs are deterministic and has labelled nodes and edges [3], but for
convenience edge labels will be named features. A linear graph grammar is de-
fined over a set of nodes N , a set of labels Ω and a set of features F [1], by the
following rules:
N ode ::= n : ω (f1 ⇒ N ode, ... , fk ⇒ N ode) | n : • | n
avec n ∈ N , ω ∈ Ω et f1 , ... , fk ∈ F
T ermGraph ::= N ode | N ode + T ermGraph
Allowing one to define a node, with its label and its direct sons, a node
without label or just a reference to an actual node with the first rules, and to
define multiparts termgraphs with the others.
508 M. Winckel and R. Matthes
app app
app
λx y app
f
x F x
(a) term: (λx.x) y (b) sharing: F x x (c) recursor: Y f
Fig. 1. Examples of term representation
In a less syntactic and maybe more semantic manner, a termgraph is defined
as well by a structure.
(N , E, LN , LE , S, T ) with
– N a finite set of nodes
– E a finite set of edges
– LN a partial function from N to Ω, associating a node to its label
– LE a total function from E to F, associating a edge to its feature
– S a source function from E to N
– T a target function from E to N
It’s assumed that the previous definitions respect a determinism condition de-
fined as
∀ e1 , e2 ∈ E, S(e1 ) = S(e2 ) ∧ LE (e1 ) = LE (e2 ) → e1 = e2
Rooted TermGraphs. In the following, for the need of the logic, the graphs
will be an extension of the termgrah with a specific node pointed as its root.
(N , E, LN , LE , S, T , r) with the root r ∈ N
3 Dynamic Logic for Graph Rewriting
A modal logic is a propositional logic, extended with one or several modality op-
erators. Dynamic logic [4] is a multi-modal logic, its modalities being actions and
the possibility to express a choice, an iteration or the sequence of actions. Actions
can be defined to express graph transformations by miscellaneous modalities.
3.1 Syntax of the Dynamic Logic
For given countable sets F and Ω, of features and labels (their respective ele-
ments being usually denoted a, b, ... and ω, π, ...), the rules defining the formulas
and the actions of the syntax are the following. [1]
For an action α:
On a Dynamic Logic for Graph Rewriting 509
α ::= a for the navigation by a ∈ F from the root
|U for changing the root to any node in the graph
|n|n for the creation of a node n, eventually setting it as the root
| φ? for the verification of the validity of a formula φ for the root
| (ω :=l φ) | (ω :=g φ) for labeling a node with a label ω ∈ Ω if a
formula φ is valid, locally for the root or globally for any node.
| (a + (φ, ψ)) | (a − (φ, ψ)) for adding or removing edges with the
feature a, between nodes verifying a formula φ and those verifying a formula
ψ.
| (α1 ; α2 ) | (α1 ∪ α2 ) | α1∗ for the definition of a sequence, a choice
or an iteration over actions α1 and α2 .
For a formula φ:
φ ::= ω | ⊥ | ¬ φ | φ ∨ ψ | [ α ]φ
ω as a formula means that node labels can be atomic formulas. And intuitively,
[ α ]φ means that after any execution of an action α, the formula φ holds. The
propositional logic of such dynamic logic being a classical one, some more sym-
bols can be defined as usual conjunction, implication and equivalency being re-
spectively φ∧ψ ≡ ¬(¬φ∨¬ψ), φ → ψ ≡ ¬φ∨ψ and φ ↔ ψ ≡ (φ → ψ)∧(ψ → φ),
for given formulas φ and ψ. One more modality can be defined, for a given action
α and formula φ, as < α > φ ≡ ¬[α]¬φ. Intuitively, it holds when an execution
of the action α makes φ hold.
3.2 Semantics of the Dynamic Logic
A semantic can be defined for this dynamic logic using rooted termgraphs as
models and verifying the properties expressed by the formulas on them, using
the sets of labels and features of the logic to define them. [1]
Models. The rooted termgraphs used here are different from the previous ones.
The labeling function for nodes is now defined over the power set of Ω, so typed
LN : N → P(Ω), of what the former definition is said to be a particular case.
Interpretation of Actions and Formulas. Before the definition of a satisfi-
ability relation, it needs interpretation functions over the models.
IG is defined as
– IG (a) = {e | e ∈ E and LE (e) = a} the set of a edges.
– IG (ω) = {n | n ∈ N and ω ∈ LN (n)} the set of nodes having the ω label.
And, for any a ∈ F, RG is a family of binary relations defined such as
– RG (a) = {(n1 , n2 ) | ∃e ∈ IG (a), S(e) = n1 and T (e) = n2 }
510 M. Winckel and R. Matthes
Because of dependency between formulas and actions, the satisfiability rela-
tion |= for a formula F and a rooted termgraph G requires an inductive definition
on F , dependent of a relation G −→α G0 for every action α.
– G ω iff n0 ∈ IG (ω), interpreting ω in G.
– G 2⊥
– G ¬φ iff G 2 φ
– G φ ∨ ψ iff G φ or G ψ
– G [α]φ iff for any rooted termgraph G0 , if G −→α G0 then G0 φ
with G −→α G0 the binary relation between two termgraphs G and G0 consid-
ering the action α. It is defined inductively on α, with G = (N , E, LN , LE , S, T , r)
0 0
and G0 = (N 0 , E 0 , LN , LE , S 0 , T 0 , r0 ), but only definitions for the useful cases
will be introduced. The definitions are declarative, so it should be read as condi-
tions for a correct relation between G and G0 and not as the way to get a model
G0 from a model G.
A notation JeKG is introduced for a graph G and an edge e of G, to express
(S(e), LE (e), T (e)). Ambiguity decreases, in the following definitions, the set E
being only identifiers of edges for the functions LE , S and T and not tuples of
these informations. We can justify this by looking at the other way, with E as a
set of tuples, and seeing that it does not make much sense: for example, when
redirecting edges, the set E was staying the same, and so were the tuples in this
set, but the target of an edge was changed and thus a tuple was associated by
functions to information which is no longer the content of the tuples.
For convenience, another notation G[n0 ] is introduced for a node n0 of a graph
G = (N , E, LN , LE , S, T , r), to express the graph (N , E, LN , LE , S, T , n0 ), or in
more simple terms, to express changing the root of G with n0 .
G −→a G0 iff
0 0
– N 0 = N , E 0 = E, LN = LN , LE = LE , S 0 = S and T 0 = T , to express
almost all parts of G0 being the same.
– (n0 , n00 ) ∈ RG (a), to express the possibility to navigate from the root of G
to the root of G0 .
G −→U G0 iff
0 0
– N 0 = N , E 0 = E, LN = LN , LE = LE , S 0 = S and T 0 = T , to express no
characterization for the root of G0 but other parts being the same.
G −→(ω:=g φ) G0 iff
0
– N 0 = N , E 0 = E, LE = LE , S 0 = S, T 0 = T and r0 = r
0 0
– for any m ∈ N , if G[m] φ then LN (m) = LN (m) ∪ {ω} else LN (m) =
N
L (m)\{ω}, expressing the addition or deletion of the label ω of any node
m of the graph satisfying the formula φ.
G −→φ? G0 iff
On a Dynamic Logic for Graph Rewriting 511
0 0
– N 0 = N , E 0 = E, LN = LN , LE = LE , S 0 = S, T 0 = T and r0 = r
– G φ, to express the formula φ being valid for G.
G −→(ω:=l φ) G0 iff
E0
– N 0 = N , E 0 = E, L
0
= LE , S 0 = S, T 0 = T and r0 = r
N0
– if G φ then L (r) = L (r) ∪ {ω} else L (r) = LN (r)\{ω}, to express
N N
the addition or deletion of the label ω from the root.
G −→(a+(φ,ψ)) G0 iff
0
– N 0 = N and LN = LN
Considering the set of candidate edges C = {(ns , a, nt ) | with ns ∈ N and nt ∈
N such as G[ns ] φ and G[nt ] ψ}, to be added only between nodes vali-
dating the formulas φ and ψ.
– E 0 ⊃ E, and for all e ∈ E, JeKG0 = JeKG , characterizing an addition without
any loss.
– for all p ∈ C, ∃e ∈ E 0 , JeKG0 = p and for all e ∈ E 0 \ E, JeKG0 ∈ C, expressing
candidate edges being added in E 0 but nothing else.
G −→(a−(φ,ψ)) G0 iff
0
– N 0 = N and LN = LN
Considering the set of deleted edges E = {e | e ∈ E such as JeKG0 = (ns , a, nt )
with ns and nt such as G[ns ] φ and G[nt ] ψ}.
– E 0 = E \ E characterizing deletion of edges only between nodes validating
formulas φ and ψ.0
– for all e ∈ E, LE (e) = LE (e), S 0 (e) = S(e), T 0 (e) = T (e) and r = r0 .
G −→α;β G0 iff
– there exists a rooted termgraph G00 such G −→α G00 and G00 −→β G0 .
G −→α∗ G0 iff
– there is a rooted termgraph sequence (G(0) ,. . . ,G(k) ) with G(0) = G, G(k) =
G0 and for all i ∈ {0, ... , k − 1}, G(i) −→α G(i+1) .
Semantics of left over actions n, n and α1 ∪ α2 are in the original paper.
At this point, the logic allows to characterize classes of graphs using the satisfi-
ability of formulas by these graphs as models. Everything goes pretty well, but
issues come when dealing with rewriting and propositions made to talk about
graph rewriting.
4 Actual Rewriting, and its Issues
The approach here is an algorithmic one: transformation actions are defined
within a rewriting system and can be applied to a graph, alone or sequentially.
It forms rules of rewriting that could be applied if an instantiation of the rule
is found in a given graph. Such instance can be defined with a graph morphism
which embeds the graph domain of the rule into the graph in which the rule
could be applied.
512 M. Winckel and R. Matthes
4.1 Homomorphism of Graphs
A homomorphism of labelled graphs h : G → G0 can be defined, given two rooted
0 0
termgraphs G = (N , E, LN , LE , S, T , r) and G0 = (N 0 , E 0 , LN , LE , S 0 , T 0 , r0 ).
n 0
Somewhat, only with a function h : N → N preserving the labeling of nodes
but equally preserving the source and target function for the edges, and thus the
labelization of edges.
0
So ∀m ∈ N , LN (hn (m)) = LN (m) is mandatory and then because of the deter-
minism condition satisfied by the graphs, there is no ambiguity on the conditions
for the edges of the codomain graph G0 . For any e of E, it only requires one exist-
0
ing e0 of E 0 verifying S 0 (e0 ) = hn (S(e)), LE (e0 ) = LE (e) and T 0 (e0 ) = hn (T (e)),
and so with corresponding source and target while preserving the edge labeliza-
tion, mandatory too for such homomorphism. There is no specific condition for
correspondence of roots of the two termgraphs.
Examples of the original paper can be presented here, in Figure 2, to display
some homomorphisms: morphisms h2 and h3 , between three graphs B1, B2 and
B3 displaying the association of their nodes.
n0 : f n0 : f n0 : f
h2 : B1 −→ B3 h3 : B2 −→ B3
1 1 1 n0 7→ n0 n0 7→ n0
n1 : g n1 : g n1 : g n1 7→ n1 n1 7→ n1
a b a b a b n2 7→ n2 n2 7→ n2
n2 : • n3 : • n2 : 0 n3 : • n2 : 0 n3 7→ n2 n3 7→ n2
B1 B2 B3
(a) termgraphs (b) homomorphisms
Fig. 2. Examples of termgraph homomorphisms
Existence of Graph Homomorphisms and Particularity of such
Homomorphisms
In the original paper, a way to talk about homomorphisms on graphs using
the logic is proposed, a formula express this concept and is defined for a graph
G = (N , E, LN , LE , S, T , r). Thus an action αG and a formula φG can relate that
there is a homomorphism from G to a graph G0 if and only if G0 < αG > φG .[1]
For this, considering N = {n0 , . . . , nN −1 }, with N being the number of nodes
of G and n0 being its root, and considering a sequence P = {π0 , . . . , πN −1 } of
distinct elements of Ω, each πi is going identify the node ni .
The action αG is defined
– with βG = (π0 :=g ⊥) ; . . . ; (πi :=g ⊥) ; . . . ; , (πN −1 :=g ⊥), characterizing
the elimination of any label πi .
On a Dynamic Logic for Graph Rewriting 513
i
– with, for 0 ≤ i ≤ N − 1, γG = (¬π0 ∧ . . . ∧ ¬πi )? ; (πi :=l >) ; U , charac-
terizing the labelization with πi of a node not already labelled with πk for
k ≤ i.
0 N −1
– and finally αG = βG ; γG ; . . . ; γG , sequencing these actions.
Then, the formula φG is defined
– with 0 ≤ i ≤ N − 1, if LN (ni ) 6= ∅ then ψG i
=< U > (πi ∧ LN (ni ))
i
else ψG = >, characterizing the conservation of the labelization of a node
identified as the image of ni , by the label πi , but nothing if this node wasn’t
labelled.
– with for 0 ≤ i, j ≤ N − 1, if ∃e ∈ E such S(e) = ni and T (e) = nj then
ζ i,j E i,j
G =< U > (πi ∧ < L (e) > πj ) else ζG = >, characterizing the existence
of edges corresponding to the ones of G.
0 N −1 0,0 N −1,N −1
– and finally φG = ψG ∧ . . . ∧ ψG ∧ ζG ∧ . . . ∧ ζG , verifying all these
formulas.
In the latter definition, it is assumed to have a subset P of Ω of fresh labels not
already used in G, and so that do not have to be preserved by the homomorphism
in G0 , and do not erase information when used in βG . Such dedicated labels for
identification of the elements of N could be assumed as a part of the set Ω, by
definition. This definition of P , identifying differently each node of G and the
way it is used in the formula, requires more for a homomorphism than what
implies the homomorphism definition. Acutally, the examples of the Figure 2,
which do not stand against the definition, are not injective morphisms. In the
formula < αG > φG , matched nodes are labelled to be identified to only one
node of G, as the test (¬π0 ∧ . . . ∧ ¬πi )? express it. Therefore, it is mandatory
for a homomorphism h : G −→ G0 to be injective to satisfy the formula and
this necessary condition on the models. Although, such injectivity is a common
feature of graph morphism in many graph rewriting frameworks, so it is not
mandatory to define formally such a system using injective matching only and the
initial definition of graph homomorphism should specify wether this particularity
is actually required.
4.2 Rewriting Step and Translation in Logic
The rewriting is defined to be applied to a graph G = (N , E, LN , LE , S, T , r)
0 0
to obtain a graph G0 = (N 0 , E 0 , LN , LE , S 0 , T 0 , r0 ), the result of the application
of an action α to a graph G is denoted α[G]. It is possible to make sequences
of actions, as empty or the concatenation of an action α and another sequence,
and the application of a sequence ∆ to a graph G is denoted ∆[G].[1]
– if ∆ is the empty sequence then ∆[G] = G
– if ∆ = α; ∆0 is a concatenation, with a sequential operator “;”, then ∆[G] =
∆0 [ α[G] ]
For a morphism h and a sequence ∆, h(∆) denotes the sequence one obtains by
substitution in ∆ of any node n by h(n).
514 M. Winckel and R. Matthes
The original paper proposes a way to talk about sequences of actions, by de-
scribing the sequence of rewriting actions as a sequence of logical actions. Thus,
after the translation of an action α of the rewriting system, the relation −→tr(α)
introduced with the semantic of the logic allows to relate models, the second
potentially being the result of the application of the action to the first one.
The translation of a sequence of a given action a and another sequence ∆ will
be the sequence of translations αa;∆ = αa ; α∆ . Assuming that any action has
a translation entirely independent of the rest of the sequence, the translation
order actually does not matter, but a sequential translation seizes a correct idea.
For the rewriting actions:
n a m is a local redirection.
An outgoing edge from a node n with the feature a is modified to point to
a node m.
0 0
– N 0 = N , E 0 = E, LN = LN , LE = LE , S 0 = S and r = r0 , the nodes, edges,
their labelization, the source of the edges and the root are the same.
0
– for e ∈ E such S 0 (e) = n and LE (e) = a then T 0 (e) = m, the target of the
only wanted edge is changed for m. ∀e0 ∈ E 0 , if e0 6= e then T 0 (e0 ) = T (e0 ),
the target function doesn’t change for the other edges.
To begin with, here is the given formula for the local redirection.
– αn a m = (a − (πn , >)) ; (a + (πn , πm ))
One can notice that this formula depicts a transformation by deleting an
edge, labelled a, between a node n and any other node, though the determinism
dictates the existence of at most only one such edge. But above all thus an a
edge between this node n and a node m is added at the end. Looking at the
definition of the local redirection, one can see that E 0 = E specify that no edge
is actually added and the other item clearly specify that only an existing e of E
with source as n and feature as a has its target changed to m.
A difference happens between the rewriting of a graph and the models linked
by the actions of the translation of the rewriting action, as shown in Figure 3
which is a counter example for adequation between this translation and rewriting.
n : πn n : πn n : [πn ] n : [πn ]
=⇒ −→ a
m : πm m : πm m : [πm ] m : [πm ]
(a) rewrite rule (b) models
Fig. 3. Local Redirection Difference
On a Dynamic Logic for Graph Rewriting 515
The problem being that the logical actions don’t require the existence of the
redirected edge, what is obviously mandatory to rewrite it. We proposed, as a
correction for this problem, the formula:
– αn a m = (λn :=g ⊥) ; (λn :=g πn ∧ < a > >) ; (a−(πn , >)) ; (a+(λn , πm ))
The added actions require the marking of a node n with a λn , assumed fresh
for the graph, validating the possibility to navigate along a a edge to any node,
then it proceeds to delete and add the edge only with this sole mark. If no edge
was removed, no mark will be found on the node n, correcting this problem of
adequation between rewriting and logical translation.
n m is a global redirection.
The target of every edge pointing to the node n is modified to make the
edges point to the node m.
0 00 0
– N 0 = N , LE = E, LN = LN , LE = LE and S 0 = S, the nodes, edges, their
labelizations and the source of the edges.
– for all e ∈ E such as T (e) = n then T 0 (e) = m else T 0 (e) = T (e), the targets
of the only wanted edges are changed for m, otherwise it does not change.
– if n = r then r0 = m else r0 = r, the root changes if it’s the former target of
the changed edges.
If one looks at the translation of the global redirection, with first a formula
to globally redirect to a node m every a edges initially pointing to a node n:
– αn ga m = (λa :=g ⊥) ; (λa :=g < a > πn ) ; (a − (>, πn )) ; (a + (λa , πm ))
This formula does not suffer of this problem, the second action marking with a
λa any reachable node by an edge with the feature a. Then, the action adding
the edges does not add wrongly an inexistant previously removed edge, since the
label λa ensures these nodes are subjects to redirection. However, it is implicitly
required that this λa is a dedicated label for this action, to not interfere with
any other formula using this label for another purpose. The full translation of
the rewriting step is finally a sequence of the previously defined formulas, for
every feature of the graph:
– αn m = ;a∈F αn ga m
Comes finally the last rewriting action, the node labelization.
n : ω (f1 ⇒ n1 , ... , fk ⇒ nk ) is a node definition or labelization.
It adds a node n, if it does not already belongs to the graph, or modifies
an already existing one. It assigns the label ω and defines the edges e1 to ek
outing of this node n, respectively pointing to the nodes n1 to nk with the
labels f1 to fk , according to the following definition:
– N 0 = N ∪ {n, n1 , ..., nk }, nodes of the rules which are not already included
in G are added.
516 M. Winckel and R. Matthes
00 0
– LN (n) = ω and ∀m ∈ N \ {n}, LN (m) = LN (m), n is labelled with ω and
the other nodes keep the same labeling.
0
Considering the newly defined edges E = {ei |S 0 (ei ) = n, LE (ei ) = fi and
T 0 (ei ) = ni } with 1 ≤ i ≤ k.
– E 0 = E ∪ E, new edges are added to the already existing ones.
0
– ∀ei ∈ E, LE (ei ) = fi , the features of the new edges are defined, and ∀e ∈ /
E0
E, L (e) = LE (e), the features of the other edges don’t change.
– ∀ei ∈ E, S 0 (ei ) = n and ∀e ∈/ E, S 0 (e) = S(e), the same thing is done for the
source function.
– ∀ei ∈ E, T 0 (ei ) = ni and ∀e ∈ / E, T 0 (e) = T (e), the same thing is done for
the target function.
– r0 = r, the root remains the same.
And the formula, initially given as its translation:
– αn : ω (f1 ⇒n1 , ... , fk ⇒nk ) =
U ; πn ? ; (ω :=l >) ; (f1 + (πn, , πn1 )) ; ... ; (fk + (πn, , πnk ))
One could there raise a first issue, regarding the end of the formula: it adds
without much care outgoing edges of the node n, thereby not ensuring the deter-
minism. The result is that no model can be related as resulting of the application
of this action, when what was intended was a relation on models displaying a
redirection of these edges. We proposed this correction, using as previously the
idea of edge redirection by deletion of the former edge and addition of the redi-
rected one.
– αn : ω (f1 ⇒n1 , ... , fk ⇒nk ) =
U ; πn ? ; (ω :=l >) ;
(f1 − (πn , >)) ; . . . ; (fk − (πn , >)) ; (f1 + (πn , πn1 )) ; . . . ; (fk + (πn , πnk ))
Now, a model related by the relation of the corresponding formula for this
action can exist, and it will be a deterministic graph with redirected edges. How-
ever, there still remains a problem. If one looks at the transformation expressed
by the formula, it translates the labelization of a node positionning the root
on a node n, identified by πn , thus it labelizes it with ω and finally changes the
edges outgoing of this node n. As displayed in Figure 4, this raises again a major
difference between the graph one obtains by rewriting and the models related by
the relation for the modality of the logical action. The behavior is not the same
because the formula requires only the addition of a label to the multiple already
existing labels of a node while the rewriting action requires the replacement as
an unique label.
For a better understanding of the extent of this problem, one should look at
the following, which demonstrates how much of an issue that becomes in regard
of characterization of rewriting system.
On a Dynamic Logic for Graph Rewriting 517
n:l =⇒ n:ω n : [l] −→ n : [ω, l]
(a) rewrite rule (b) models
Fig. 4. Node Labeling Difference
4.3 Rewriting Rules and Rewriting System Characterization
Rewriting rules
A rewriting rule is expressed as a graph L and a sequence of actions ∆ to apply,
and will be noted (L, ∆). It is said that a graph G is rewritten as a graph G0
if there exists a homomorphism h : L → G such as h(∆)[G] = G0 , denoted
G →L,∆ G0 .
A simple yet useful example may be defined, representing an action on a simple
on-off switch of an electrical network:
L= off : SwitchOff
e
on off
pos : • e e neg : •
int : Off on : SwitchOn
Fig. 5. Left-hand side L of a rule
Displayed in Figure 5, on the left of L there is a positive terminal of the
circuit, on the right side there is a negative one. The edges labelled edges as e are
for the electrical circuit and the switch is currently set to Off . The two positions
SwitchOn and SwitchOff are linked to each other to avoid any mismatch if
another switch is part of the network, even though a one-way link alone could
be enough.
∆switchOn = (int : On ( ) ; int >>e on)
Fig. 6. Sequence ∆ of a rule
The sequence for this rule, as displayed in Figure 6, is made of an action to
mark the switch node with On without adding any extra edge, and an action to
redirect the edge e, outgoing from this node to the Off position of the switch, to
get a graph representing a closed electrical circuit, displayed now in Figure 7 as
the result on the graph L.
518 M. Winckel and R. Matthes
off : SwitchOff
on off
pos : • e e e neg : •
=⇒ int : On on : SwitchOn
Fig. 7. result of applying ∆ to L
Rewriting System Characterization and The Labelization Problem
Using the previous example of a switch activation, a graph G is displayed in
the Figure 8, being a simple electrical network having only a generator and a
switch, and being really similar to the left-hand side of the rule (L, ∆switchOn )
previously defined.
off : SwitchOff
e
on off
e e
G = pos : DC+ int : Off on : SwitchOn neg : DC−
Fig. 8. graph G
The normal form of the graph G, with respect to the rule (L, ∆switchOn ),
satisfies the formula ψ := [U ]¬Off , because of its switch being activated and
thus being labelled with On, so no node is labelled with Off anymore.
In the end of the original paper, the proposition 4 [1] which defines a way to
talk about a normal formal of a graph G satisfying ψ says that this should be
equivalent to the following satisfaction
G [(αL ; φL ?; α∆switchOn )∗ ]([αL ; φL ?] ⊥ → ψ)
To explain this proposition, one can think about a normal form with respect
of a rule as resulting of successive matchings and applications of this rule. When
the rule cannot be matched anymore this implies that the formula ψ holds, which
characterizes the normal forms. In the example with the rule (L, ∆switchOn ),
every switch must be activated and the rule shouldn’t be matchable then, because
there is no label Off or any e edge pointing to the right position. But because of
the difference between rewriting and translation in the logic, when every e edge
of the switch is redirected in the models, no more matching is available but there
is still the label Off , along with the label On labeling the node int. The formula
ψ is thus unsatisfied, the graph G and the formula ψ are a counter example for
this proposition.
On a Dynamic Logic for Graph Rewriting 519
First, one can notice that relying on the definition of the models, the logic
makes use of the labels to mark and reason, but without any difference between
the ones being actual parts of the graph and the ones serving the logic. Even if
the problem appears with the semantics, the solution is not there, because any
change of the model definition, allowing to make a difference between graph and
logic for example by simply splitting in two layer these informations, doesn’t
mean that the same syntax of the logic allows to express this difference.
The problem comes with the translation of the label definition of a node, it
seems sounding to complete this translation to get the correspondence between
rewriting and relation on models. But the rules and the matching use the labels
to logically identify the node, so one should be careful with erasing, thus to erase
everything is not an option here. Actually, the syntax of the logic needs explicitly
the label to delete, with a global or local labeling action. And the syntax of the
action currently does not allow to say which label will be erased. This is where
the problem lies in: there is only the identifier of a node and the new label.
To actually translate the action, it is possible if it is given more information, so
a new label definition action is a possibility or the syntax of the logic should be
changed to express actions on a new model type.
But before any syntactic change, of rewriting actions or logic, it is interesting
to consider the action in the context of a graph. Because of the LN : N −→ Ω
of the graph, and having already the node n of the action, the labeling function
can give the label to remove. Regarding of the action to translate, there is not
this information, but more generally rewriting actions are defined for a specific
graph. Thus, lifting the translation in formula to the level of the rule, this gives
the required information. From this rule, a graph is given as left-hand side and
thus a LN : N −→ Ω function can be used, and it allows an explicit erasing of
a label as it was implicitly expected by the rewriting action.
For a graph G = (N , E, LN , LE , S, T , r) and a node labeling action n :
ω (f1 ⇒ n1 , ... , fk ⇒ nk ), we give as a correct translation the formula
– αG, n : ω (f1 ⇒n1 , ... , fk ⇒nk ) =
U ; πn ? ; (LN (n) :=l ⊥) ; (ω :=l >) ;
(f1 − (πn , >)) ; ... ; (fk − (πn , >)) ; (f1 + (πn , πn1 )) ; ... ; (fk + (πn , πnk ))
However, the application of the rule to the left-hand side results in another
graph with another labeling function and the translation of a sequence cannot
remain as previously proposed. Every node labeling action should be translated
depending on the result of previously applied actions. The translation of a se-
quence of an action a and another sequence ∆ is a sequence of sequential trans-
lations:
αG, (a;∆) = αG, a ; αa[G], ∆
One could notice that this translation is still done in a linear way through the
sequence, but this definition could actually be slightly changed because every
action but node labelization can be translated independently. Only the node
labelization is dependent of a context and more precisely there are conflicts only
520 M. Winckel and R. Matthes
when editing the same node, having to erase a label which was just defined
previously in the sequence.
5 Conclusion
This paper provided an introduction to a dynamic logic, defined by P. Balbiani,
R. Echahed and A. Herzig. Originally, a formalization was done using the
Coq proof assistant and so was done a study of this logic. During this work
some mistakes were spotted. While sometimes these were just minor-looking
imprecisions, when working with formal logic, it may be relevant to point out
such ambiguities if the logic can become incoherent with a wrong interpretation.
Other mistakes are not only due to interpretation, and as it was demon-
strated, they allow to find counter-examples for propositions and thus to estab-
lish incoherence with the main goal of this logic, to talk about rewriting systems.
Solutions to these issues are proposed, they resolve the issues by getting back to
an adequation between actual rewriting and relations on models of the logic.
A first idea to find another technical problem is the conservation of deter-
minism of graphs, which only seems currently assumed and can be broken by
the action of the logic, heading to the impossibility to relate a model to another
because of the determinism, assumed by definition. It could be more explicit in
the semantics of rewriting, and currently the definition of one of the rewriting
actions allows to add edges breaking this condition. This is something the logic
can express and handle during the translation of these rewriting actions, this
looks like an interesting improvement of the logical framework.
The models are defined with a multi-labeling function of nodes and already
demonstrate some differences during translation of rewriting into the logic, be-
cause the models are graphs with a unique-labeling function into the initial
rewriting system. It is not totally clear whether the difference stops there, and
it is required to study more uses of the logic in regards of rewriting to be sure
of the correct use. It seems interesting to study the reverse translation as well,
from logic to rewriting, to get an useful and complete logical framework, in the
idea of Curry − Howard correspondence with terms as proofs.
References
1. Balbiani, P., Echahed, R., Herzig, A.: A dynamic logic for termgraph rewriting. In
Ehrig, H., Rensink, A., Rozenberg, G., Schürr, A. (eds.) ICGT. LNCS, vol. 6372,
pp.59–74. Springer, Heidelberg (2010)
2. Ariola, Z.M., Klop, J.W.: Lambda calculus with explicit recursion. Inf. Comput.
147(2), 154–233 (1997)
3. Barendregt, H., van Eekelen, M., Glauert, J., Kennaway, J., Plasmeijer, M., Sleep,
M.: Term graph rewriting. In de Bakker, J., Nijman, A., Treleaven, P. (eds.)
PARLE Parallel Architectures and Languages Europe. LNCS, vol. 259, pp. 141–
158. Springer, Heidelberg (1987)
4. Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. Handbook of Philosophical Logic,
MIT Press. 497–604 (1984)