A modal Logic for Termgraph Rewriting

⋆

Ph. Balbiani1 , R. Echahed2 , and A. Herzig1

arXiv:1003.4369v1 [cs.LO] 23 Mar 2010

1

Université de Toulouse, CNRS
Institut de Recherche en Informatique de Toulouse (IRIT)
118 route de Narbonne, 31062 Toulouse Cedex 9, France
{balbiani,herzig}@irit.fr
2
Laboratoire LIG
Bât IMAG C
BP 53
38041 Grenoble Cedex, France
Rachid.Echahed@imag.fr

Abstract. We propose a modal logic tailored to describe graph transformations and discuss some of its properties. We focus on a particular
class of graphs called termgraphs. They are first-order terms augmented
with sharing and cycles. Termgraphs allow one to describe classical datastructures (possibly with pointers) such as doubly-linked lists, circular
lists etc. We show how the proposed logic can faithfully describe (i) termgraphs as well as (ii) the application of a termgraph rewrite rule (i.e.
matching and replacement) and (iii) the computation of normal forms
with respect to a given rewrite system. We also show how the proposed
logic, which is more expressive than propositional dynamic logic, can
be used to specify shapes of classical data-structures (e.g. binary trees,
circular lists etc.).

1

Introduction

Graphs are common structures widely used in several areas in computer science
and discrete mathematics. Their transformation constitute a domain of research
per se with a large number of potential applications [11, 8, 9]. There are many
different ways to define graphs and graph transformation. We consider in this
paper structures known as termgraphs and their transformation via rewrite rules
[5, 10]. Roughly speaking, a termgraph is a first-order term with possible sharing
(of sub-terms) and cycles. Below we depict three examples of termgraphs : G0 is a
classical first-order term. G1 represents the same expression as G0 but argument
x is shared. G1 is often used to define the function double double(x) = G1 . The
second termgraph G2 represents a circular list of two “records” (represented here
by operator cons) sharing the same content G1 .
⋆

This work has been partly funded by the project ARROWS of the French Agence
Nationale de la Recherche.

x

{{
}{
{

+C
CC
C!

+
x

 
x

s
consI
II
II
$

+

/ cons
uu
u
uz u

 
x
G0

G1

G3

Termgraphs allow to represent real-world data structures (with pointers)
such as circular lists, doubly-linked lists etc [7], and rewriting allows to efficiently process such graphs. They are thus a suitable framework for declarative
languages dealing with such complex data structures. However, while there exist
rewriting-based proof methods for first-order terms, there is a lack of appropriate termgraph rewriting proof methods, diminishing thus their operational
benefits. Indeed, equational logic provides a logical setting for first-order term
rewriting [4], and many theorem provers use rewrite techniques in order to efficiently achieve equational reasoning. In [6] an extension of first-order (clausal)
logic dealing with termgraphs has been proposed to give a logic counterpart of
termgraph rewriting. In such a logic operations are interpreted as continuous
functions [12, 13] and bisimilar graphs cannot be distinguished (two termgraphs
are bisimilar if and only if they represent the same rational term). Due to that,
reasoning on termgraphs is unfortunately much trickier than in first-order classical logic. For example, equational theories on termgraphs are not recursively
enumerable whereas equational theories on terms are r.e.).
In this paper, we investigate a modal logic with possible worlds semantics
which better fits the operational features of termgraph rewriting systems. Termgraphs can easily be interpreted within the framework of possible worlds semantics, where nodes are considered as worlds and edges as modalities. Based
on this observation, we investigate a new modal logic which has been tailored to
fit termgraph rewriting. We show how termgraphs as well as rewrite rules can be
specified by means of modal formulae. In particular we show how a rewrite step
can be defined by means of a modal formula which encodes termgraph matching (graph homomorphism) and termgraph replacement (graph construction and
modification). We show also how to define properties on such structures, such as
being a list, a circular list, a tree, a binary tree. The computation of termgraph
normal form is formulated in this new logic. In addition, we formulate invariant preservation by rewriting rules and discuss subclasses for which validity is
decidable.
The next two sections introduce respectively the considered class of termgraph rewrite systems and the proposed modal logic. In section 4 we discuss
briefly the expressive power of the modal logic and show particularly how graph
homomorphisms can be encoded. In section 5 we show how elementary graph
transformations can be expressed as modal logic formulae whareas section 6
shows how termgraph rewriting can be specified as modal formulae. Section 7
gives some concluding remarks.

2

Termgraph Rewriting

This section defines the framework of graph rewrite systems that we consider
in the paper. There are different approaches in the literature to define graph
transformations. We follow here an algorithmic approach to termgraph rewriting
[5]. Our definitions are consistent with [7].
Definition 21 (Graph)
A termgraph, or simply a graph is a tuple G = (N , E, Ln , Le , S, T ) which consists
of a finite set of nodes N , a finite set of edges E, a (partial) node labelling function
Ln : N → Ω which associates labels in Ω to nodes in N , a (total) edge labelling
function Le : E → F which associates, to every edge in E, a label (or feature) in
F , a source function S : E → N and a target function T : E → N which specify
respectively, for every edge e, its source S(e) and its target T (e).
Note that G is a first-order term if and only if G is a tree.
We assume that the labelling of edges Le fulfills the following additional determinism condition: ∀e1 , e2 ∈ E, (S(e1 ) = S(e2 ) and Le (e1 ) = Le (e2 )) implies e1 =
e2 . This last condition expresses the fact that for every node n there exists at
most one edge e of label a such that the source of e is n. We denote such an
edge by the tuple (n, a, m) where m is the target of edge e.
Notation: For each labelled node n the fact that ω = Ln (n) is written n : ω,
and each unlabelled node n is written as n : •. This ‘unlabelled’ symbol • is used
in termgraphs to represent anonymous variables. n : ω(a1 ⇒ n1 , . . . , ak ⇒ nk )
describes a node n labelled by symbol ω with k outgoing edges, e1 , . . . , ek , such
that for every edge ei , Le (ei ) = ai , S(ei ) = n and T (ei ) = ni . In the sequel we
will use the linear notation of termgraphs [5] defined by the following grammar.
The variable A (resp. F and n) ranges over the set Ω (resp. F and N ) :
TermGraph ::= Node | Node + TermGraph
Node
::= n:A(F ⇒ Node,. . . ,F ⇒ Node) | n:• | n
the operator + stands for the disjoint union of termgraph definitions. We assume
that every node is labelled at most once. The expression n : ω(n1 , . . . , nk ) stands
for n : ω(1 ⇒ n1 , . . . , k ⇒ nk ).
A graph homomorphism, h : G → G1 , where G = (N , E, Ln , Le , S, T ) and
G1 = (N1 , E1 , Ln1 , Le1 , S1 , T1 ) is a pair of functions h = (hn , he ) with hn : N → N1
and he : E → E1 which preserves the labelling of nodes and edges as well
as the source and target functions. This means that for each labelled node
m in G, Ln1 (hn (m)) = Ln (m) and for each edge f in G, Le1 (he (f )) = Le (f ),
S1 (he (f )) = hn (S(f )) and T1 (he (f )) = hn (T (f )). Notice that the image by hn
of an unlabelled node may be any node.
Remark: Because of the determinism condition, a homomorphism h : G →
G1 is completely defined by the function hn : N → N1 which should satisfy the
following conditions : for each labelled node m in G, Ln1 (hn (m)) = Ln (m) and
for every outgoing edge from m, say (m, a, w), for some feature a and node w,
the edge (hn (m), a, hn (w)) belongs to E1 .

Example 22 Let B1 , B2 and B3 be the following termgraphs.
B1 : n 0 : h
1


n1 : gM
MMaM
M&
b
n2 : •
n3 : •

B2 : B n 0 : h

B3 : n 0 : h

1


n1 : gL
LLLa
LL%
b
n3 : •
n2 : 0

1
n1 : g
b  a
n2 : 0

and h and h′ be two functions on nodes defined as follows: h(ni ) = ni for
i in {0, 1, 2, 3} and h′ (ni ) = ni for i in {0, 1, 2} and h′ (n3 ) = n2 . h defines a
homomorphism from B1 to B2 . h′ defines a homomorphism from B1 to B3 and
from B2 to B3 . There is no homomorphism from B3 to B2 or to B1 , nor from
B2 to B1 .
The following definition introduces a notion of actions. Each action specifies
an elementary transformation of graphs. These elementary actions are used later
on to define graph transformations by means of rewrite rules.
Definition 23 (Actions) An action has one of the following forms.
– a node definition or node labelling n : f (a1 ⇒ n1 , . . . , ak ⇒ nk ) where
n, n1 , . . . , nk are nodes and f is a label of node n. For i ∈ {1, . . . , k}, ai
is the label of an edge, ei , such that (Le (ei ) = ai ) and whose source is n
(S(ei ) = n) and target is node ni (T (ei ) = ni ). This action, first creates a
new node n if n does not already exist in the context of application of the
action. Then node n is defined by its label and its outgoing edges.
– an edge redirection or local redirection n ≫a m
where n, m are nodes and a is the feature of an edge e outgoing node n
(S(e) = n and Le (e) = a). This action is an edge redirection and means that
the target of edge e is redirected to point to the node m (i.e., T (e) = m after
performing the action n ≫a m).
– a global redirection n ≫ m
where n and m are nodes. This means that all edges e pointing to n (T (e) =
n) are redirected to point to the node m (T (e) = m).
The result of applying an action α to a termgraph G = (N , E, Ln , Le , S, T ) is
denoted by α[G] and is defined as the following termgraph G1 = (N1 , E1 , Ln1 , Le1 , S1 , T1 )
such that :
– If α = n : f (a1 ⇒ n1 , . . . , ak ⇒ nk ) then
• N1 = N ∪ {n, n1 , . . . , nk },
• Ln1 (n) = f and Ln1 (m) = Ln (m) if m 6= n,
• Let E = {ei | 1 ≤ i ≤ k, ei is an edge such that S(ei ) = n, T (ei ) =
e
ni and L
(ei ) = ai }. E1 = E ∪ E,
ai
if e = ei ∈ E
e
• L1 (e) =
Le (e)
if e 6∈ E



n
if e = ei ∈ E
S(e)
if
e 6∈ E

ni
if e = ei ∈ E
• T1 (e) =
T (e)
if e 6∈ E
∪ denotes classical union. This means that the nodes in {n, n1 , . . . , nk } which
already belong to G are reused whereas the others are new.
– If α = n ≫a m then
• N1 = N , Ln1 = Ln , Le1 = Le , S1 = S and
• Let e be the edge of label a outgoing n.
T1 (e) = m and T1 (e′ ) = T (e′ ) if e′ 6= e.
– If α = n ≫ m then N1 = N , Ln1 = Ln , Le1 = Le , S1 = S and

m
if T (e) = n
T1 (e) =
T (e)
otherwise
• S1 (e) =

A rooted termgraph is a termgraph G with a distinguished node n called
its root. We write G = (N , E, Ln , Le , S, T , n). The application of an action α
to a rooted termgraph G = (N , E, Ln , Le , S, T , n) is a rooted termgraph G1 =
(N1 , E1 , Ln1 , Le1 , S1 , T1 , n1 ) such that G1 = α[G] and root n1 is defined as follows :
– n1 = n if α is not of the form n ≫ p.
– n1 = p if α is of the form n ≫ p.
The application of a sequence of actions ∆ to a (rooted) termgraph G is defined
inductively as follows : ∆[G] = G if ∆ is the empty sequence and ∆[G] = ∆′ [α[G]]
if ∆ = α; ∆′ where “;” is the concatenation (or sequential) operation. Let h be
a homomorphism. We denote by h(∆) the sequence of actions obtained from ∆
by substituting every node m occurring in ∆ by h(m).
Example 24 This example illustrates the application of actions. Let H1 , H2 ,
H3 , H4 and H5 be the following termgraphs.
H2 : n1 : gL
LLLa
LL%
b
n3 : •
n2 : 0

H1 : n 1 : f
a


n2 : 0

1
n1 : gL
LLLa
LL%
b
n3 : •
n2 : 0

H5 :

H4 : n 0 : h
1

b


n1 : g
b  a
n2 : 0

H3 : n 0 : h

n3 : •

nB 0 : h\
a
1
n1 : g
n2 : 0

n3 : •

H2 is obtained from H1 by applying the action n1 : g(b ⇒ n2 , a ⇒ n3 ). n1
is relabelled whereas n3 is a new unlabelled node. H3 is obtained from H2 by

applying the action α = n0 : h(n1 ). n0 is a new node labelled by h. h has one
argument n1 . H4 is obtained from H3 by applying the action n1 ≫a n2 . The
effect of this action is to change the target n3 of the edge (n1 , a, n3 ) by n2 . H5
is obtained from H4 by applying the action n2 ≫ n0 . This action redirects the
incoming edges of node n2 to target node n0 .
Definition 25 (Rule, system, rewrite step) A rewrite rule is an expression
of the form l → r where l is a termgraph and r is a sequence of actions. A rule is
written l → (a1 , . . . , an ) or l → a1 ; . . . ; an where the a′i s are elementary actions.
A termgraph rewrite system is a set of rewrite rules. We say that the term-graph
G rewrites to G1 using the rule l → r iff there exists a homomorphism h : l → G
and G1 = h(r)[G]. We write G →l→r G1 , or simply G → G1 .
Example 26 We give here an example of a rewrite step. Consider the following
rewrite rule:
n1 : g(a ⇒ n2 : •, b ⇒ n3 : •) → n0 : h(1 ⇒ n1 ); n1 ≫a n2 ; n2 ≫ n0
The reader may easily verify that the graph H2 of Example 24 can be rewritten by the considered rule into the graph H5 of Example 24.
Example 27 We give here somme illustrating examples of the considered class
of rewrite systems. We first define an operation, insert, which inserts an element
in a circular list.
r : insert(m : •, p1 : cons(m1 : •, p1 )) → p2 : cons(m, p1 ); p1 ≫2 p2 ; r ≫ p2
r : insert(m : •, p1 : cons(m1 : •, p2 ))+p3 : cons(m2 , p1 ) → p4 : cons(m, p1 );
p3 ≫2 p4 ; r ≫ p4
As a second example, we define below the operation length which computes the
number of elements of any, possibly circular, list.
r : length(p : •) → r′ : length′(p, p); r ≫ r′
r : length′ (p1 : nil, p2 : •) → r′ : 0; r ≫ r′
r : length′ (p1 : cons(n : •, p2 : •), p2 ) → r′ : succ(0); r ≫ r′
r : length′ (p1 : cons(n : •, p2 : •), p3 : •) → r′ : s(q : •); q : length′ (p2 , p3 ); r ≫ r′
Pointers help very often to enhance the efficiency of algorithms. In the following, we define the operation reverse which performs the so-called “in-situ
list reversal”.
o : reverse(p : •) → o′ : reverse′ (p, q : nil); o ≫ o′
o : reverse′ (p1 : cons(n : •, q : nil), p2 : •) → p1 ≫2 p2 ; o ≫ p1
o : reverse′ (p1 : cons(n : •, p2 : cons(m : •, p3 : •), p4 : •) → p1 ≫2 p4 ;
o ≫1 p2 ; o ≫2 p1

The last example illustrates the encoding of classical term rewrite systems.
We define the addition on naturals as well as the function double with their usual
meanings.
r : +(n : 0, m : •) → r ≫ m
r : +(n : succ(p : •), m : •) → q : succ(k : +(p, m)); r ≫ q
r : double(n : •) → q : +(n, n); r ≫ q

3

Modal logic

It is now time to define the syntax and the semantics of the logic of graph
modifiers that will be used as a tool to talk about rooted termgraphs.

3.1

Syntax

Like the language of propositional dynamic logic, the language of the logic of
graph modifiers is based on the idea of associating with each action α of an
action language a modal connective [α]. The formula [α]φ is read “after every
terminating execution of α, φ is true”. Consider, as in section 2, a countable
set F (with typical members denoted a, b, etc) of edge labels and a countable
set Ω (with typical members denoted ω, π, etc) of node labels. These labels are
formulas defined below. A node labeled by π is called a π node.
Formally we define the set of all actions (with typical members denoted α,
β, etc) and the set of all formulas (with typical members denoted φ, ψ, etc) as
follows:
– α ::= a | U | n | n | φ? | (ω :=g φ) | (ω :=l φ) | (a + (φ, ψ)) | (a − (φ, ψ)) |
(α; β) | (α ∪ β) | α⋆ ,
– φ :: ω | ⊥ | ¬φ | (φ ∨ ψ) | [α]φ.
We adopt the standard abbreviations for the other Boolean connectives. Moreover, for all actions α and for all formulas φ, let hαiφ be ¬[α]¬φ. As usual, we
follow the standard rules for omission of the parentheses. An atomic action is
either an edge label a in F , the universal action U , a test φ? or an update action
n, n, ω :=g φ, ω :=l φ, a + (φ, ψ) or a − (φ, ψ). U reads “go anywhere”, n reads
“add some new node”, n reads “add some new node and go there”, ω :=g φ
reads “assign to ω nodes the truth value of φ everywhere (globally)”, ω :=l φ
reads “assign to ω the truth value of φ here (locally)”, a + (φ, ψ) reads “add
a edges from all φ nodes to all ψ nodes”, and a − (φ, ψ) reads “deletea edges
from all φ nodes to all ψ nodes”. Complex actions are built by means of the
regular operators “;”, “∪” and “⋆ ”. An update action is an action without edge
labels and without U . An update action is :=l -free if no local assignment ω :=l φ
occurs in it.

3.2

Semantics

Like the truth-conditions of the formulas of ordinary modal logics, the truthconditions of the formulas of the logic of graph modifiers is based on the idea of
interpreting, within a rooted termgraph G = (N , E, Ln , Le , S, T , n0 ), edge labels
in F by sets of edges and node labels in Ω by sets of nodes. In this section, we
consider a more general notion of node labeling functions Ln of termgraphs
such that nodes can have several labels (propositions). In this case the labeling
function has the following profile Ln : N → P(Ω). Node labeling functions
considered in section 2 where a node can have at most one label is obviously a
particular case. Let IG be the interpretation function in G of labels defined as
follows:
– IG (a) = {e ∈ E: Le (e) = a},
– IG (ω) = {n ∈ N : ω ∈ Ln (n)}.
For all abstract actions a, let RG (a) = {(n1 , n2 ): there exists an edge e ∈ IG (a)
such that S(e) = n1 and T (e) = n2 } be the binary relation interpreting the
abstract action a in G. The truth-conditions of the formulas of the logic of
graph modifiers are defined by induction as follows:
–
–
–
–
–

G |= ω iff n0 ∈ IG (ω),
G 6|= ⊥,
G |= ¬φ iff G 6|= φ,
G |= φ ∨ ψ iff G |= φ or G |= ψ,
G |= [α]φ iff for all rooted termgraphs G′ = (N ′ , E ′ , Ln ′ , Le ′ , S ′ , T ′ , n′0 ), if G
−→α G′ then G′ |= φ

where the binary relations −→α are defined by induction as follows:
– G −→a G′ iff N ′ = N , E ′ = E, Ln ′ = Ln , Le ′ = Le , S ′ = S, T ′ = T and
(n0 , n′0 ) ∈ RG (a),
– G −→φ? G′ iff N ′ = N , E ′ = E, Ln ′ = Ln , Le ′ = Le , S ′ = S, T ′ = T , n′0
= n0 and G′ |= φ,
– G −→U G′ iff N ′ = N , E ′ = E, Ln ′ = Ln , Le ′ = Le , S ′ = S and T ′ = T ,
– G −→n G′ iff N ′ = N ∪ {n1 } where n1 is a new node, E ′ = E, Ln ′ (m) =
Ln (m) if m 6= n1 , Ln ′ (n1 ) = ∅, Le ′ = Le , S ′ = S, T ′ = T and n′0 = n0 ,
– G −→n G′ iff N ′ = N ∪ {n1 } where n1 is a new node, E ′ = E, Ln ′ (m) =
Ln (m) if m 6= n1 , Ln ′ (n1 ) = ∅, Le ′ = Le , S ′ = S, T ′ = T and n′0 = n1 ,
– G −→ω:=g φ G′ iff N ′ = N , E ′ = E, Ln ′ (m) = if (N , E, Ln , Le , S, T , m) |=
φ} then Ln (m) ∪ {ω} else Ln (m) \ {ω}, Le ′ = Le , S ′ = S, T ′ = T and n′0
= n0 ,
– G −→ω:=l φ G′ iff N ′ = N , E ′ = E, Ln ′ (n0 ) = if (N , E, Ln , Le , S, T , n0 ) |=
φ then Ln (n0 ) ∪ {ω} else Ln (n0 ) \ {ω}, Ln ′ (m) = Ln (m) if m 6= n0 , Le ′ =
Le , S ′ = S, T ′ = T and n′0 = n0 ,
– G −→a+(φ,ψ) G′ iff N ′ = N , E ′ = E ∪ {(n1 , a, n2 ) : (N , E, Ln , Le , S, T , n1 ) |=
φ and (N , E, Ln , Le , S, T , n2 ) |= ψ}, Ln ′ = Ln , Le ′ (e) = if e ∈ E then
Le (e) else a, S ′ (e) = if e ∈ E then S(e) else e is of the form (n1 , a, n2 ) and
S ′ (e) = n1 , T ′ = if e ∈ E then T (e) else e is of the form (n1 , a, n2 ) and
T ′ (e) = n2 and n′0 = n0 ,

– G −→a−(φ,ψ) G′ iff N ′ = N , E ′ = E\{(n1 , a, n2 ) : (N , E, Ln , Le , S, T , n1 ) |= φ
and (N , E, Ln , Le , S, T , n2 ) |= ψ}, Ln ′ = Ln , Le ′ (e) = Le (e), S ′ = S, T ′ =
T and n′0 = n0 ,
– G −→α;β G′ iff there exists a rooted termgraph G′′ = (N ′′ , E ′′ , Ln ′′ , Le ′′ , S ′′ , T ′′ , n′′0 )
such that G −→α G′′ and G′′ −→β G′ ,
– G −→α∪β G′ iff G −→α G′ or G −→β G′ ,
(0)
– G −→α⋆ G′ iff there exists a sequence G(0) = (N (0) , E (0) , Ln (0) , Le (0) , S (0) , T (0) , n0 ),
(k)
. . ., G(k) = (N (k) , E (k) , Ln (k) , Le (k) , S (k) , T (k) , n0 ) of rooted termgraphs
(0)
(k)
′
such that G
= G, G
= G and for all non-negative integers i, if i <
k then G(i) −→α G(i+1) .
The above definitions of formulas reflect our intuitive understanding of the actions of the language of the logic of graph modifiers. Obviously, G |= hαiφ iff there
exists a rooted termgraph G′ = (N ′ , E ′ , Ln ′ , Le ′ , S ′ , T ′ , n′0 ) such that G −→α G′
and G′ |= φ. The formula φ is said to be valid in class C of rooted termgraphs, in
symbols C |= φ, iff G |= φ for each rooted termgraph G = (N , E, Ln , Le , S, T , n0 )
in C. The class of all rooted termgraphs will be denoted more briefly as Call .
3.3

Validities

Obviously, as in propositional dynamic logic, we have
–
–
–
–

Call
Call
Call
Call

|=
|=
|=
|=

[φ?]ψ ↔ (φ → ψ),
[α; β]φ ↔ [α][β]φ,
[α ∪ β]φ ↔ [α]φ ∧ [β]φ,
[α⋆ ]φ ↔ φ ∧ [α][α⋆ ]φ.

If α is a :=l -free update action then
– Call |= [α]⊥ ↔ ⊥,
– Call |= [α]¬φ ↔ ¬[α]φ,
– Call |= [α](φ ∨ ψ) ↔ [α]φ ∨ [α]ψ.
The next series of equivalences guarantees that each of our :=l -free update actions can be moved across the abstract actions of the form a or U :
Call |= [n][a]φ ↔ [a][n]φ,
Call |= [n][U ]φ ↔ [n]φ ∧ [U ][n]φ,
Call |= [n][a]φ ↔ ⊤,
Call |= [n][U ]φ ↔ [n]φ ∧ [U ][n]φ,
Call |= [ω :=g φ][a]ψ ↔ [a][ω :=g φ]φ,
Call |= [ω :=g φ][U ]ψ ↔ [U ][ω :=g φ]ψ,
Call |= [a + (φ, ψ)][b]χ ↔ [b][a + (φ, ψ)]χ if a 6= b and Call |= [a + (φ, ψ)][b]χ ↔
[b][a + (φ, ψ)]χ ∧ (φ → [U ](ψ → [a + (φ, ψ)]χ)) if a = b,
– Call |= [a + (φ, ψ)][U ]χ ↔ [U ][a + (φ, ψ)]χ,
– Call |= [a − (φ, ψ)][b]χ ↔ [b][a − (φ, ψ)]χ if a 6= b and Call |= [a − (φ, ψ)][b]χ ↔
(¬φ ∧ [b][a − (φ, ψ)]χ) ∨ (φ ∧ [b](¬ψ → [a − (φ, ψ)]χ)) if a = b,
– Call |= [a − (φ, ψ)][U ]χ ↔ [U ][a − (φ, ψ)]χ.

–
–
–
–
–
–
–

Finally, once we have moved each of our :=l -free update actions across the abstract actions of the form a or U , these update actions can be eliminated by
means of the following equivalences:
–
–
–
–
–

Call
Call
Call
Call
Call

|=
|=
|=
|=
|=

[n]ω ↔ ω,
[n]ω ↔ ⊥,
[ω :=g φ]π ↔ π if ω 6= π and Call |= [ω :=g φ]π ↔ φ if ω = π,
[a + (φ, ψ)]ω ↔ ω,
[a − (φ, ψ)]ω ↔ ω.

Proposition 31 For all :=l -free ⋆ -free formulas φ, there exists a :=l -free ⋆ -free
formula ψ without update actions such that Call |= φ ↔ ψ.
Proof. See the above discussion.

Just as for :=l -free update actions, we have the following equivalences for the
update actions of the form ω :=l φ:
–
–
–
–

Call
Call
Call
Call

|=
|=
|=
|=

[ω
[ω
[ω
[ω

:=l
:=l
:=l
:=l

φ]⊥ ↔ ⊥,
φ]¬ψ ↔ ¬[ω :=l φ]ψ,
φ](ψ ∨ χ) ↔ [ω :=l φ]ψ ∨ [ω :=l φ]χ,
φ]π ↔ π if ω 6= π and Call |= [ω :=g φ]π ↔ φ if ω = π.

But it is not possible to formulate reduction axioms for the cases [ω :=l φ][a]ψ
and [ω :=l φ][U ]ψ. More precisely,
Proposition 32 There exists a ⋆ -free formula φ such that for all ⋆ -free formulas
ψ without update actions, Call 6|= φ ↔ ψ.
Proof. Take the ⋆ -free formula φ = [ω :=g ⊥][U ][ω :=l ⊤][a]¬ω. The reader may
easily verify that for all rooted termgraphs G = (N , E, Ln , Le , S, T , n0 ), G |= φ
iff RG (a) is irreflexive. Seeing that the fact that the binary relation interpreting
an abstract action of the form a is irreflexive cannot be modally defined in
propositional dynamic logic, then for all formulas ψ without update actions, Call
6|= φ ↔ ψ.
3.4

Decidability, axiomatization and a link with hybrid logics

Firstly, let us consider the set L of all :=l -free ⋆ -free formulas φ such that Call
|= φ. Together with a procedure for deciding membership in ⋆ -free propositional
dynamic logic, the equivalences preceding proposition 31 provide a procedure for
deciding membership in L. Hence, membership in L is decidable.
Secondly, let us consider the set L(:=l ) of all ⋆ -free formulas φ such that Call
|= φ. Aucher et al. [3] have defined a recursive translation from the language of
hybrid logic [2] into the set of all our ⋆ -free formulas that preserves satisfiability.
It is known that the problem of deciding satisfiability of hybrid logic formulas

is undecidable [1, Section 4.4]. The language of hybrid logic has formulas of the
form @i φ (“φ is true at i”), @x φ (“φ is true at x”) and ↓x.φ (“φ holds after x is
bound to the current state”), where NOM = {i1 , . . .} is a set of nominals, and
SVAR = {x1 , . . .} is a set of state variables. The (slightly adapted) translation
of a given hybrid formula φ0 is recursively defined as follows.
τ (ω)
=ω
τ (i)
= ωi where ωi does not occur in φ0
τ (x)
= ωx where ωx does not occur in φ0
τ (¬φ) = ¬τ (φ)
τ (φ ∨ ψ) = τ (φ) ∨ τ (ψ)
τ ([a]φ) = [a]τ (φ)
τ ([U ]φ) = [U ]τ (φ)
τ (@i φ) = hU i(ωi ∧ τ (φ))
τ (@x φ) = hU i(ωx ∧ τ (φ))
τ (↓x.φ) = [ωx :=g ⊥][ωx :=l ⊤]τ (φ)
As the satisfiability problem is undecidable in hybrid logic, membership in L(:=l )
is undecidable, too.
Thirdly, let us consider the set L(⋆ ) of all :=l -free formulas φ such that Call
|= φ. It is still an open problem whether membership in L(⋆ ) is decidable or not:
while the update actions can be eliminated from :=l -free formulas, it is not clear
whether this can be done for formulas in which e.g. iterations of assignments
occur.
As for the axiomatization issue, the equivalences preceding proposition 31
provide a sound and complete axiom system of L, whereas no axiom system of
L(:=l ) and L(⋆ ) is known to be sound and complete.

4

Definability of classes of termgraphs

For all abstract actions a, by means of the update actions of the form ω :=l φ,
we can express the fact that the binary relation interpreting an abstract action
of the form a is deterministic, irreflexive or locally reflexive. More precisely, for
all rooted termgraphs G = (N , E, Ln , Le , S, T , n0 ),
– G |= [ω :=g ⊥][π :=g ⊥][U ][ω :=l ⊤][a][π :=l ⊤][U ](ω → [a]π) iff RG (a) is
deterministic,
– G |= [ω :=g ⊥][U ][ω :=l ⊤][a]¬ω iff RG (a) is irreflexive,
– G |= [ω :=g ⊥][ω :=l ⊤]haiω iff RG (a) is locally reflexive in n0 .
Together with the update actions of the form ω :=l φ, the regular operation
“⋆ ” enables us to define non-elementary classes of rooted termgraphs. As a first
example, the class of all infinite rooted termgraphs cannot be modally defined
in propositional dynamic logic but the following formula pins it down:
– [ω :=g ⊤][(U ; ω?; ω :=l ⊥)⋆ ]hU iω.

As a second example, take the class of all a-cycle-free rooted termgraphs. It cannot be modally defined in propositional dynamic logic but the following formula
pins it down:
– [ω :=g ⊤][U ][ω :=l ⊥][a+ ]ω.
As a third example, within the class of all a-deterministic rooted termgraphs, the
class of all a-circular rooted termgraphs3 cannot be modally defined in propositional dynamic logic but the following formula pins it down:
– [ω :=g ⊥][U ][ω :=l ⊤]ha+ iω.
Now, within the class of all rooted termgraphs that are both a- and b-deterministic,
the class of all (a ≤ b) rooted termgraphs 4 cannot be modally defined in propositional dynamic logic but the following formula pins it down:
– [ω :=g ⊥][ω :=l ⊤][π :=g ⊥][π :=l ⊤][((U ; ω?; a; ¬ω?; ω :=l ⊤); (U ; π?; b; ¬π?; π :=l
⊤))⋆ ](hU i(π ∧ [b]⊥) → hU i(ω ∧ [a]⊥)).
Finally, within the class of all finite (a ∪ b)-cycle-free (a, b)-deterministic rooted
termgraphs, the class of all (a, b)-binary rooted termgraphs cannot be modally
defined in propositional dynamic logic but the following formula pins it down:
– [ω :=g ⊥][U ][ω :=l ⊤][a][π :=g ⊤][(a ∪ b)⋆ ][π :=l ⊥][U ](ω → [b][(a ∪ b)⋆ ]π).
Most important of all is the ability of the language of the logic of graph modifiers
to characterize finite graph homomorphisms.
Proposition 41 Let G = (N , E, Ln , Le , S, T , n0 ) be a finite rooted termgraph.
There exists a ⋆ -free action αG and a ⋆ -free formula φG such that for all finite
rooted termgraphs G′ = (N ′ , E ′ , Ln ′ , Le ′ , S ′ , T ′ , n′0 ), G′ |= hαG iφG iff there exists
a graph homomorphism from G into G′ .
Proof. Let G = (N , E, Ln , Le , S, T , n0 ) be a finite rooted termgraph. Suppose
that N = {0, . . . , N − 1} and consider a sequence (π0 , . . . , πN −1 ) of pairwise
distinct elements of Ω. Each πi will identify exactly one node of N , and π0 will
identify the root.
We define the action αG and the formula φG as follows:
– βG = (π0 :=g ⊥); . . . ; (πN −1 :=g ⊥),
i
– for all non-negative integers i, if i < N then γG
= (¬π0 ∧. . .∧¬πi−1 )?; (πi :=l
⊤); U ,
N −1
0
– αG = βG ; γG
; . . . ; γG
,
3

4

In an a-circular rooted termgraph for every node n there is an i and there are a1 ,
. . . an such that a = a1 = an and nk is related to nk+1 by an edge labelled a, for all
k ≤ i.
Rooted termgraphs are termgraphs where the path obtained by following feature b
is longer than or equal to the path obtained by following feature a.

i
– for all non-negative integers i, if i < N then ψG
= if Ln (i) is defined then
n
hU i(πi ∧ L (i)) else ⊤,
– for all non-negative integers i, j, if i, j < N then χi,j
G = if there exists an
edge e ∈ E such that S(e) = i and T (e) = j then hU i(πi ∧ hLe (e)iπj ) else ⊤,
N −1,N −1
N −1
0
– φG = ψG
∧ . . . ∧ ψG
∧ χ0,0
.
G ∧ . . . ∧ χG

The reader may easily verify that for all finite rooted termgraphs
G′ = (N ′ , E ′ , Ln ′ , Le ′ , S ′ , T ′ , n′0 ), G′ |= hαG iφG iff there exists a graph homomorphism from G to G′ .

5

Definability of transformations of termgraphs

In this section we show how elementary actions over termgraphs as defined in
Section 2 can be encoded by means of formulas of the proposed modal logic. Let
αa be the action defined as follows:
– αa = (ω :=g ⊥); (ω :=l ⊤); (π :=g ⊥); (π :=g haiω); (a − (⊤, ω)); n; (ω :=g
⊥); (ω :=l ⊤); (a + (π, ω)).
The reader may easily verify that for all rooted termgraphs
G = (N , E, Ln , Le , S, T , n0 ) and G′ = (N ′ , E ′ , Ln ′ , Le ′ , S ′ , T ′ , n′0 ), G −→αa G′
iff G′ is obtained from G by redirecting every a-edge pointing to the current root
towards a freshly created new root. Hence, together with the update actions n,
n, ω :=g φ, ω :=l φ, a+ (φ, ψ) and a− (φ, ψ), the regular operations “;”, “∪” and
“⋆ ” enable us to define the elementary actions of node labelling, local redirection
and global redirection of Section 2. Let us firstly consider the elementary action
of node labelling: n : f (a1 ⇒ n1 , . . . , ak ⇒ nk ). Applying this elementary action
consists in redirecting towards nodes n1 , . . ., nk the targets of a1 -, . . ., ak - edges
starting from node n. It corresponds to the action nl(n : f (a1 ⇒ n1 , . . . , ak ⇒
nk )) defined as follows:
– nl(n : f (a1 ⇒ n1 , . . . , ak ⇒ nk )) = U ; πn ?; (f :=l ⊤); (a1 +(πn , πn1 )); . . . ; (ak +
(πn , πnk )).
where the πi ’s are as in the proof of Proposition 41. The reader may easily verify that for all rooted termgraphs G = (N , E, Ln , Le , S, T , n0 ), G′ =
(N ′ , E ′ , Ln ′ , Le ′ , S ′ , T ′ , n′0 ), G −→nl(n:f (a1 ⇒n1 ,...,ak ⇒nk )) G′ iff G′ is obtained
from G by redirecting towards nodes n1 , . . ., nk the targets of a1 -, . . ., ak - edges
starting from node n. Let us secondly consider the elementary action of local
redirection: n ≫la m. Applying this elementary action consists in redirecting
towards node m the target of an a-edge starting from node n. It corresponds to
the action lr(n, a, m) defined as follows:
– lr(n, a, m) = (a − (πn , ⊤)); (a + (πn , πm )).
The reader may easily verify that for all rooted termgraphs G = (N , E, Ln , Le , S, T , n0 ),
G′ = (N ′ , E ′ , Ln ′ , Le ′ , S ′ , T ′ , n′0 ), G −→lr(n,a,m) G′ iff G′ is obtained from G by
redirecting towards node m the target of an a-edge starting from node n. Let us

thirdly consider the elementary action of global redirection: n ≫ga m. Applying
this elementary action consists in redirecting towards node n the target of every
a-edge pointing towards node m. It corresponds to the action gr(n, a, m) defined
as follows:
– gr(n, a, m) = (λa :=g ⊥); (λa :=g haiπn ); (a − (⊤, πn )); (a + (λa , πm )).
The reader may easily verify that for all rooted termgraphs G = (N , E, Ln , Le , S, T , n0 ),
G′ = (N ′ , E ′ , Ln ′ , Le ′ , S ′ , T ′ , n′0 ), G −→gr(n,a,m) G′ iff G′ is obtained from G by
redirecting towards node n the target of every a-edge pointing towards node m.
To redirect towards n the target of all edges pointing towards m, the action
V
gr(n, a, m).
gr(n, a, m) can be performed for all a ∈ F . We get gr(n, m) =
a∈F

6

Translating rewrite rules in modal logic

Now we are ready to show how termgraph rewriting can be specified by means
of formulas of the proposed modal logic.
Let G → (a1 , . . . , an ) be a rewrite rule as defined in Section 2, i.e., G =
(N , E, Ln , Le , S, T , n0 ) is a finite rooted termgraph and (a1 , . . . , an ) is a finite
sequence of elementary actions. We have seen how to associate to G a ⋆ -free
action αG and a ⋆ -free formula φG such that for all finite rooted termgraphs G′ =
(N ′ , E ′ , Ln ′ , Le ′ , S ′ , T ′ , n′0 ), G′ |= hαG iφG iff there exists a graph homomorphism
from G into G′ . We have also seen how to associate to the elementary actions a1 ,
. . ., an actions α1 , . . ., αn . In the following proposition we show how to formulate
the fact that a normal form with respect to a rewrite rule (generalization to a set
of rules is obvious) satisfies a given formula ϕ. A termgraph t is in normal form
with respect to a rule R iff t cannot be rewritten by means of R. Such formulation
may help to express proof obligations of programs specified as termgraph rewrite
rules. Let n1 , . . ., nk be the list of all nodes occurring in a1 , . . ., an but not
occurring in G. The truth of the matter is that
Proposition 61 Let ϕ be a modal formula. For all finite rooted termgraphs
G′ = (N ′ , E ′ , Ln ′ , Le ′ , S ′ , T ′ , n′0 ), every normal form of G′ with respect to G →
(a1 , . . . , an ) satisfies ϕ iff G′ |= [(αG ; φG ?; n; (πn1 :=g ⊥); (πn1 :=l ⊤); . . . ; n; (πnk :=g
⊥); (πnk :=l ⊤); α1 ; . . . ; αn )⋆ ]([αG ; φG ?]⊥ → ϕ).
Proof. ⇐: Suppose that G′ |= [(αG ; φG ?; n; (πn1 :=g ⊥); (πn1 :=l ⊤); . . . ; n; (πnk :=g
⊥); (πnk :=l ⊤); α1 ; . . . ; αn )⋆ ]([αG ; φG ?]⊥ → ϕ). Consider a normal form Gnf of
G′ with respect to G → (a1 , . . . , an ). Then there exists a non-negative integer k
and there exist finite rooted termgraphs G0 , . . ., Gk such that:
– G0 = G′ ,
– Gk = Gnf ,
– for all non-negative integers i, if i < k then Gi →G→(a1 ,...,an ) Gi+1 .

Hence, for all non-negative integers i, if i < k then
Gi −→αG ;φG ?;n;(πn1 :=g ⊥);(πn1 :=l ⊤);...;n;(πnk :=g ⊥);(πnk :=l ⊤);α1 ;...;αn Gi+1 . Moreover,
seeing that Gnf is a normal form with respect to G → (a1 , . . . , an ), Gnf |=
[αG ; φG ?]⊥. Since G′ |= [(αG ; φG ?; n; (πn1 :=g ⊥); (πn1 :=l ⊤); . . . ; n; (πnk :=g
⊥); (πnk :=l ⊤); α1 ; . . . ; αn )⋆ ]([αG ; φG ?]⊥ → ϕ), then Gnf |= ϕ. Thus, every
normal form of G′ with respect to G → (a1 , . . . , an ) satisfies ϕ.
⇒: Suppose that every normal form of G′ with respect to G → (a1 , . . . , an )
satisfies ϕ. Let Gnf be a finite rooted termgraph such that
G′ −→(αG ;φG ?;n;(πn1 :=g ⊥);(πn1 :=l ⊤);...;n;(πnk :=g ⊥);(πnk :=l ⊤);α1 ;...;αn )⋆ Gnf and Gnf
|= [αG ; φG ?]⊥. Then Gnf is a normal form of G′ with respect to G → (a1 , . . . , an ).
Hence, Gnf satisfies ϕ. Thus, G′ |= [(αG ; φG ?; n; (πn1 :=g ⊥); (πn1 :=l ⊤); . . . ; n; (πnk :=g
⊥); (πnk :=l ⊤); α1 ; . . . ; αn )⋆ ]([αG ; φG ?]⊥ → ϕ).
In other respects, the following proposition shows how an invariant ϕ of a rewrite
rule can be expressed in the proposed logic.
Proposition 62 Let ϕ be a modal formula. The rewrite rule G → (a1 , . . . , an )
strongly preserves ϕ iff |= ϕ → [αG ; φG ?; n; (πn1 :=g ⊥); (πn1 :=l ⊤); . . . ; n; (πnk :=g
⊥); (πnk :=l ⊤); α1 ; . . . ; αn ]ϕ.
Proof. ⇐: Suppose that |= ϕ → [αG ; φG ?; n; (πn1 :=g ⊥); (πn1 :=l ⊤); . . . ; n; (πnk :=g
⊥); (πnk :=l ⊤); α1 ; . . . ; αn ]ϕ. Let G′ , G′′ be finite rooted termgraphs such that
G′ |= ϕ and G′ →G→(a1 ,...,an ) G′′ . Then G′ |= [αG ; φG ?; n; (πn1 :=g ⊥); (πn1 :=l
⊤); . . . ; n; (πnk :=g ⊥); (πnk :=l ⊤); α1 ; . . . ; αn ]ϕ and
G′ −→αG ;φG ?;n;(πn1 :=g ⊥);(πn1 :=l ⊤);...;n;(πnk :=g ⊥);(πnk :=l ⊤);α1 ;...;αn G′′ . Hence, G′′
|= ϕ. Thus, the rewrite rule G → (a1 , . . . , an ) strongly preserves ϕ.
⇒: Suppose that the rewrite rule G → (a1 , . . . , an ) strongly preserves ϕ. Let G′ ,
G′′ be finite rooted termgraphs such that G′ |= ϕ and
G′ −→αG ;φG ?;n;(πn1 :=g ⊥);(πn1 :=l ⊤);...;n;(πnk :=g ⊥);(πnk :=l ⊤);α1 ;...;αn G′′ . Then G′ →G→(a1 ,...,an )
G′′ and G′′ |= ϕ. Thus, |= ϕ → [αG ; φG ?; n; (πn1 :=g ⊥); (πn1 :=l ⊤); . . . ; n; (πnk :=g
⊥); (πnk :=l ⊤); α1 ; . . . ; αn ]ϕ.

7

Conclusion

We have defined a modal logic which can be used either (i) to describe datastructures which are possibly defined by means of pointers and considered as
termgraphs in this paper, (ii) to specify programs defined as rewrite rules which
process these data-structures or (iii) to reason about data-structures themselves
and about the behavior of the considered programs. The features of the proposed logic are very appealing. They contribute to define a logic which captures
faithfully the behavior of termgraph rewrite systems. They also open new perspectives for the verification of programs manipulating pointers.
Our logic is undecidable in general. This is not surprising at all with respect
to its expressive power. However, this logic is very promising in developing new

proof procedure regarding properties of termgraph rewrite systems. For instance,
we have discussed a first fragment of the logic, consisting of formulas without
relabelling actions, where validity is decidable. Future work include mainly the
investigation of new decidable fragments of our logic and their application to
program verification.

References
1. C. Areces, P. Blackburn, and M. Marx. A road-map on complexity for hybrid
logics. In J. Flum and M. Rodrı́guez-Artalejo, editors, Computer Science Logic,
number 1683 in LNCS, pages 307–321, Madrid, Spain, 1999. Springer. Proceedings
of the 8th Annual Conference of the EACSL, Madrid, September 1999.
2. C. Areces and B. ten Cate. Hybrid logics. In P. Blackburn, J. van Benthem, and
F. Wolter, editors, Handbook of Modal Logic, volume 3. Elsevier Science, 2006.
3. G. Aucher, P. Balbiani, L. Fariñas Del Cerro, and A. Herzig. Global and local
graph modifiers. Electronic Notes in Theoretical Computer Science (ENTCS),
Special issue “Proceedings of the 5th Workshop on Methods for Modalities (M4M5
2007)” , 231:293–307, 2009.
4. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University
Press, 1998.
5. H. Barendregt, M. van Eekelen, J. Glauert, R. Kenneway, M. J. Plasmeijer, and
M. Sleep. Term graph rewriting. In PARLE’87, pages 141–158. Springer Verlag
LNCS 259, 1987.
6. R. Caferra, R. Echahed, and N. Peltier. A term-graph clausal logic: Completeness
and incompleteness results. Journal of Applied Non-classical Logics, 18:373–411,
2008.
7. R. Echahed. Inductively sequential term-graph rewrite systems. In 4th International Conference on Graph Transformations (ICGT), volume 5214 of Lecture
Notes in Computer Science, pages 84–98. Springer, 2008.
8. H. Ehrig, G. Engels, H.-J. Kreowski, and G. Rozenberg, editors. Handbook of Graph
Grammars and Computing by Graph Transformations, Volume 2: Applications,
Languages and Tools. World Scientific, 1999.
9. H. Ehrig, H.-J. Kreowski, U. Montanari, and G. Rozenberg, editors. Handbook of
Graph Grammars and Computing by Graph Transformations, Volume 3: Concurrency, Parallelism and Distribution. World Scientific, 1999.
10. D. Plump. Term graph rewriting. In H. Ehrig, G. Engels, H. J. Kreowski, and
G. Rozenberg, editors, Handbook of Graph Grammars and Computing by Graph
Transformation, volume 2, pages 3–61. World Scientific, 1999.
11. G. Rozenberg, editor. Handbook of Graph Grammars and Computing by Graph
Transformations, Volume 1: Foundations. World Scientific, 1997.
12. J. Tiuryn. Fixed-points and algebras with infinitely long expression, part 1, regular
algebras. Fundamenta Informaticae, 2:103–127, 1978.
13. J. Tiuryn. Fixed-points and algebras with infinitely long expression, part 2, µclones of regular algebras. Fundamenta Informaticae, 2(3):317–335, 1979.

