# Global and local graph modifiers

Guillaume Aucher, Philippe Balbiani, Luis Fariñas del Cerro, Andreas Herzig

## ► To cite this version:

Guillaume Aucher, Philippe Balbiani, Luis Fariñas del Cerro, Andreas Herzig. Global and local graph modifiers. Electronic Notes in Theoretical Computer Science, 2009, Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007), 231, 10.1016/j.entcs.2009.02.042. inria-00556034

HAL Id: inria-00556034

https://inria.hal.science/inria-00556034

Submitted on 15 Jan 2011

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est destinée au dépôt et à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

<figure><img src="image_1.png" /></figure>
Replace this file with *prentcsmacro.sty* for your meeting,
or with *entcsmacro.sty* for your meeting. Both can be
found at the ENTCS Macro Home Page.

Global and local graph modifiers

Guillaume Aucher<sup>5,1</sup>

IRIT-LILaC, Université Paul Sabatier, Toulouse, France
and Dept. of CS, Otago University, Dunedin, NZ

Philippe Balbiani<sup>2</sup>

IRIT-LILaC, CNRS, Toulouse, France

Luis Fariñas del Cerro<sup>3</sup>

IRIT-LILaC, CNRS, Toulouse, France

Andreas Herzig<sup>4</sup>

IRIT-LILaC, CNRS, Toulouse, France

Global and local graph modifiers

Abstract

We define two modal logics that allow to reason about modifications of graphs. Both have a universal modal operator. The first one only involves global modifications (of some state label, or of some edge label) everywhere in the graph. The second one also allows for modifications that are local to states. The global version generalizes logics of public announcements and public assignments, as well as a logic of preference modification introduced by van Benthem et Liu. By means of reduction axioms we show that it is just as expressive as the underlying logic without global modifiers. We then show that adding local modifiers dramatically increases the power of the logic: the logic of global and local modifiers is undecidable. We finally study its relation with hybrid logic with binder.

Keywords: Public Announcement Logic, graph modifiers.

<footnote n="1">¹ Email: aucher@irit.fr</footnote>

<footnote n="2">² Email: balbiani@irit.fr</footnote>

<footnote n="3">³ Email: farinas@irit.fr</footnote>

<footnote n="4">⁴ Email: herzig@irit.fr</footnote>

<footnote n="5">⁵ This work was supported by the French ANR project ARROWS. Rachid Echahed submitted to us the problem of formalizing graph modifications in modal logic. We would like to thank him for inspiring discussions. We are grateful to the anonymous reviewers whose comments helped to improve the paper.</footnote>
# 1 Introduction: modal logic as a language to talk about graphs

Consider a rooted graph, whose nodes are labelled by subsets of a countable set of labels PROP, and whose edges are labelled by subsets of a countable set of labels REL. Such a graph can be represented as a 4-tuple $M = \langle W, w, R, V \rangle$ where

* $W$ is a set of states (nodes);

* $w \in W$ is a particular state ('the actual state');

* $R: REL \to 2^{W \times W}$ associates to every edge label $a$ a binary relation on $W$ ('the interpretation of $a$');

* $V: PROP \to 2^W$ associates to every state label $p$ a subset of $W$ ('the interpretation of $p$').

The language of modal logic is a tool to talk about such labelled graphs. The formulas $\varphi$ and the modalities $\alpha$ are defined by the BNFs

$$ \varphi ::= p \mid \neg \varphi \mid \varphi \lor \varphi \mid [\alpha]\varphi $$

$$ \alpha ::= a \mid \alpha; \alpha \mid \varphi? $$

where $p$ ranges over PROP and $a$ over REL.

Given a rooted graph (alias a model) $M = \langle W, w, R, V \rangle$, we say that $p \in PROP$ holds in $M$ (noted $M \models p$) if and only if $w \in V(p)$; and a disjunction $\varphi \lor \psi$ holds in $M$ ($M \models \varphi \lor \psi$) iff $\varphi$ holds in $M$ ($M \models \varphi$) or $\psi$ holds in $M$ ($M \models \psi$). The other boolean operators can be defined likewise. For the modal operators we have the standard definition of truth of a formula in a model:

$$ M \models [a]\varphi \text{ iff } \langle W, w', R, V \rangle \models \varphi, \text{ for every } w' \text{ such that } \langle w, w' \rangle \in R(a) $$

Given $M = \langle W, w, R, V \rangle$, we say that the set $\|\varphi\|_M = \{w' \mid \langle W, w', R, V \rangle \models \varphi\}$ is the interpretation of the formula $\varphi$.

As has been pointed out by many authors, modal languages are quite poor as compared to that of predicate logic: we cannot directly talk about states in the language, and we can only quantify in a restricted way. The benefit of that restriction is that modal logics are ‘so robustly decidable’ [13]. The aim of this paper is to study how the basic modal language can be extended in order to talk not only about graphs, but also *modifications* of graphs. To that aim we shall introduce new modalities into the above basic language, whose semantics will be in terms of graph modifications.

Generally speaking, one can think of the following graph modifications: add or delete a state, add or delete a state label of some state, or add or delete an edge label between some states. In the sequel we shall consider all these operations, where the label modifications will come in a global and in a local version. The *modification of state labels* can be done by adding particular action expressions to the language, viz. assignments of the form $p := \varphi$. Such an assignment stipulates that the interpretation of $p$ is modified such that it now matches the last interpretation of $\varphi$: the assignment $p := \varphi$ transforms $M = \langle W, w, R, V \rangle$ into $M' = \langle W, w, R, V' \rangle$, where
$V'(q) = V(q)$ for $q \neq p$, and $V'(p) = \|\varphi\|_M$. This has been studied in PDL and more recently by van Ditmarsch et al. [12]. The modification of edge labels can be said to be the topic of the family of dynamic epistemic logics [10]. In the simplest case, public announcements are added to the language. For example in Kooi's logic [4], an announcement $\varphi!_K$ eliminates all those edges leading to states that are not in the interpretation of $\varphi$: $\varphi!_K$ transforms $M = \langle W, w, R, V \rangle$ into $M' = \langle W, w, R', V \rangle$, where $R'(a) = R(a) \cap (W \times \|\varphi\|_M)$ for every label $a \in REL$. In public announcement logic PAL it is not only the edges leading to $\neg\varphi$-states that are eliminated, but also the $\neg\varphi$-states themselves [6]. If there is no universal modality then the announcement of $\varphi$ à la Plaza (noted $[\varphi!]$) can be considered to be an abbreviation of the sequence $\varphi?; \varphi!_K$. Theorem 2.1 at the end of Section 2.2 shows how public announcements à la Plaza can be expressed in the presence of the universal modal operator.

We here go beyond all these approaches:

* We generalize assignments to state label modifications $p+\varphi$ and $p-\varphi$ stipulating that the interpretation of $p$ is augmented (resp. diminished) by that of $\varphi$. If $p$ does not occur in $\varphi$ then the above $p := \varphi$ corresponds to the sequence $p-\top; p+\varphi$. More generally, $p := \varphi$ can be simulated by the sequence $q-\top; q+\varphi; p-\top; p+q$, for some $q$ not appearing in $\varphi$ (which is used to store the value of $\varphi$).<fnref n="6" />

* We generalize announcements to edge label modifications $a+(\varphi, \psi)$ and $a-(\varphi, \psi)$ stipulating that the interpretation of $a$ is augmented (resp. diminished) by all edges leading from $\varphi$-states to $\psi$-states. If REL is a finite set $\{a_1, \dots, a_n\}$ then the above announcement à la Kooi $\varphi!_K$ corresponds to the elimination of all edges leading to $\neg\varphi$-states, i.e. to the sequence $a_1-(\top, \neg\varphi); \dots; a_n-(\top, \neg\varphi)$.<fnref n="7" /> In the context of preference relations as studied by van Benthem and Liu [11], this allows to express modification of preferences such as “prefer $\varphi$-worlds over $\psi$-worlds”, implemented by $a-(\psi, \varphi)$ followed by $a+(\varphi, \psi)$ (where $a$ is the preference relation).

* We moreover consider addition of a state, augmenting the set of states $W$ by a new state (without state labels and without edge labels). We consider two options, $nw$ and $\overrightarrow{nw}$: the modifier $nw$ leaves the root state unchanged, while after $\overrightarrow{nw}$ the actual state is the new state. No edge will leave the new state, nor arrive at it.

Note that we do not consider suppression of states. A natural operation would be to eliminate all those states characterized by some label. Theorem 2.1 of Section 2.2 shows that such an operation can be simulated by the others.

Finally, we need the universal modality $[U]$, whose truth condition is:

$$M \models [U]\varphi \text{ iff } \langle W, w', R, V \rangle \models \varphi, \text{ for every } w' \in W.$$

The paper is organized as follows: in Section 2 we introduce global graph modifiers, and give a proof procedure in terms of reduction axioms. In Section 3 we add local modifiers to the picture: we show that its fragment without state creators

<footnote n="6">⁶ The converse also holds: $p+\varphi$ can be simulated by $p := p \lor \varphi$, and $p-\varphi$ can be simulated by $p := p \land \neg\varphi$.</footnote>

<footnote n="7">⁷ The other way round, it seems that our label modifications can only be expressed in terms of announcements at the price of more complex devices such as local modifiers (as introduced Section 3).</footnote>
and edge modifiers is as expressive as hybrid logic with binder, i.e. as expressive as first-order logic.<fnref n="8" /> Section 4 is about the link with hybrid logic with binder. Section 5 contains related work.

## 2 Global graph modifiers

We now define the logic of global graph modifiers GML. We define the language $\mathcal{L}_{GML}$ by defining formulas $\varphi$ and modalities $\alpha$:

$$ \varphi ::= p | \neg\varphi | \varphi \lor \varphi | [\alpha]\varphi $$

$$ \alpha ::= a | \alpha; \alpha | \varphi? | \mathbf{U} | \mathbf{nw} | \overrightarrow{\mathbf{nw}} | p-\varphi | p+\varphi | a-(\varphi, \psi) | a+(\varphi, \psi) $$

where $p$ ranges over PROP and $a$ over REL. As usual $\langle\alpha\rangle\varphi$ abbreviates $\neg[\alpha]\neg\varphi$.

We call the operators $\mathbf{nw}$, $\overrightarrow{\mathbf{nw}}$, $p+\varphi$, $p-\varphi$, $a+(\varphi, \psi)$, and $a-(\varphi, \psi)$ graph modifiers.

### 2.1 Semantics

Models are as before of the form $M = \langle W, w, R, V \rangle$. The boolean connectives are interpreted as usual. For the modal connective we stipulate:

$$ M \models [\alpha]\varphi \text{ iff } M' \models \varphi, \text{ for every } M' \text{ such that } M \xrightarrow{\alpha} M' $$

where the transition relation $M \xrightarrow{\alpha} M'$ is recursively defined as follows (where we have highlighted the relevant parts of each case by underlining them):

* $\langle W, w, R, V \rangle \xrightarrow{a} \langle W', w', R', V' \rangle$ iff $W' = W, \langle w, w' \rangle \in R(a), R' = R, V' = V$;

* $\langle W, w, R, V \rangle \xrightarrow{\alpha_1;\alpha_2} \langle W', w', R', V' \rangle$ iff there is $M''$ such that $\langle W, w, R, V \rangle \xrightarrow{\alpha_1} M''$ and $M'' \xrightarrow{\alpha_2} \langle W', w', R', V' \rangle$;

* $\langle W, w, R, V \rangle \xrightarrow{\varphi?} \langle W', w', R', V' \rangle$ iff $W' = W, w' = w, R' = R, V' = V$, and $M \models \varphi$;

* $\langle W, w, R, V \rangle \xrightarrow{\mathbf{U}} \langle W', w', R', V' \rangle$ iff $W' = W, w' \in W, R' = R, V' = V$;

* $\langle W, w, R, V \rangle \xrightarrow{\mathbf{nw}} \langle W', w', R', V' \rangle$ iff $W' = W \cup \{w_{new}\}, w_{new} \notin W, w' = w, R' = R, V' = V$;

* $\langle W, w, R, V \rangle \xrightarrow{\overrightarrow{\mathbf{nw}}} \langle W', w', R', V' \rangle$ iff $W' = W \cup \{w_{new}\}, w_{new} \notin W, w' = w_{new}, R' = R, V' = V$;

* $\langle W, w, R, V \rangle \xrightarrow{p\to\varphi} \langle W', w', R', V' \rangle$ iff $W' = W, w' = w, R' = R, V'(q) = V(q)$ for $q \neq p$, and $V'(p) = V(p) \setminus \|\varphi\|_M$;

* $\langle W, w, R, V \rangle \xrightarrow{p+\varphi} \langle W', w', R', V' \rangle$ iff $W' = W, w' = w, R' = R, V'(q) = V(q)$ for $q \neq p$, and $V'(p) = V(p) \cup \|\varphi\|_M$;

* $\langle W, w, R, V \rangle \xrightarrow{a-(\varphi, \psi)} \langle W', w', R', V' \rangle$ iff $W' = W, w' = w, R'(b) = R(b)$ for $b \neq a, R'(a) = R(a) \setminus (\|\varphi\|_M \times \|\psi\|_M)$, and $V' = V$;

* $\langle W, w, R, V \rangle \xrightarrow{a+(\varphi, \psi)} \langle W', w', R', V' \rangle$ iff $W' = W, w' = w, R'(b) = R(b)$ for $b \neq a, R'(a) = R(a) \cup (\|\varphi\|_M \times \|\psi\|_M)$, and $V' = V$.

<footnote n="8">⁸ A previous version of the paper (submitted to HyLo’07) claimed that the entire logic of global and local modifiers is more expressive than hybrid logic. The proof was erroneous, and we currently do not know the exact relation.</footnote>
Validity and satisfiability in a class of models are defined as usual. An example of a validity is $[\mathbf{U}]\chi \leftrightarrow [a+(\top, \top)][a]\chi$ for any $a \in REL$ such that $a$ does not occur in $\chi$.<fnref n="9" /> Other examples of validities are: $[p+p]\psi \leftrightarrow \psi$; $[p-p]\psi \leftrightarrow [p-\top]\psi$; $[p+\neg p]\psi \leftrightarrow [p+\top]\psi$; $[p-\neg p]\psi \leftrightarrow \psi$. Note that $[p-\varphi]$ is not equivalent to $[p+\neg \varphi]$, and that $[p+\varphi]$ is not equivalent to $[p-\neg \varphi]$.

## 2.2 Global modifier logic contains PAL

As announced in Section 1, Plaza's public announcement of $\varphi$ cannot be expressed any longer in terms of Kooi's $\varphi?; \varphi!_K$ when the universal modality is in the language. To witness $[p!][\mathbf{U}]p$ is valid, while $[p?; p!_K][\mathbf{U}]p$ is not. (Related to the latter is that $\langle\mathbf{U}\rangle\neg p \to [p?; p!_K]\langle\mathbf{U}\rangle\neg p$ is valid.)

Consider an extension of Plaza's public announcement logic PAL with the universal modality, that we call PALU. Its language is defined by the following BNF:

$$ \varphi ::= p \mid \neg \varphi \mid \varphi \lor \varphi \mid [a]\varphi \mid [\mathbf{U}]\varphi \mid [\psi!]\varphi $$

This language is interpreted over the same models as before, where announcements have the transition relation

$$ \bullet \langle W, w, R, V \rangle \xrightarrow{\psi!} \langle W', w', R', V' \rangle \quad \text{iff} \quad w \in \|\psi\|_M, \quad W' = W \cap \|\psi\|_M, \quad w' = w, \quad R'(a) = R(a) \cap (\|\psi\|_M \times \|\psi\|_M), \quad \text{and} \quad V'(p) = V(p) \cap \|\psi\|_M. $$

Observe that when $\psi$ does not hold in $M$ then the set of accessible models is empty.

We give a polynomial translation from PALU into GML. Let $S$ be any subset of PROP.

$$ \begin{align*} \tau_S(p) &= p \\ \tau_S(\neg \varphi) &= \neg \tau_S(\varphi) \\ \tau_S(\varphi \lor \psi) &= \tau_S(\varphi) \lor \tau_S(\psi) \\ \tau_S([a]\varphi) &= [a]((\bigwedge S) \rightarrow \tau_S(\varphi)) \\ \tau_S([\mathbf{U}]\varphi) &= [\mathbf{U}]((\bigwedge S) \rightarrow \tau_S(\varphi)) \\ \tau_S([\psi!]\varphi) &= \tau_S(\psi) \rightarrow [p-\top][p+\psi](p \rightarrow \tau_{S \cup \{p\}}(\varphi)) \quad \text{where } p \text{ does not occur in } \varphi \text{ or } \psi \end{align*} $$

Let $M|_S$ be the restriction of $M$ to $S$ defined as in PAL: $M|_S = \langle W|_S, w, R|_S, V|_S \rangle$, where

$$ \begin{align*} W|_S &= \{w \in W : M, w \models p \text{ for every } p \in S\} \\ R|_S(a) &= R(a) \cap (W|_S \times W|_S) \\ V|_S(p) &= V(p) \cap W|_S \end{align*} $$

Note that $\langle W|_S, w', R|_S, V|_S \rangle \models p$ for every $w' \in W|_S$ and $p \in S$.

**Lemma 2.1** $M|_S \models \varphi \text{ iff } M \models \tau_S(\varphi)$, for every finite set of labels $S \subseteq PROP$.

<footnote n="9">⁹ If $a$ occurs in $\chi$ then the equivalence is not valid: for example, $[\mathbf{U}][a]p$ is not equivalent to $[a+(\top, \top)][a][a]p$.</footnote>
**Proof.** The proof is by induction on the form of $\varphi$. For the case of $[a]$:

$$M|_S \models [a]\varphi$$

iff $\langle W|_S, w', R|_S, V|_S \rangle \models \varphi$ for every $w'$ such that $\langle w, w' \rangle \in R|_S(a)$;

iff $\langle W|_S, w', R|_S, V|_S \rangle \models \varphi$ for every $w'$ such that $\langle w, w' \rangle \in R(a)$ and $\langle W|_S, w', R|_S, V|_S \rangle \models p$ for every $p \in S$;

iff (by induction hypothesis) $\langle W|_S, w', R|_S, V|_S \rangle \models \tau_S(\varphi)$ for every $w'$ such that $\langle w, w' \rangle \in R(a)$ and $\langle W|_S, w', R|_S, V|_S \rangle \models \wedge S$;

iff $M \models [a]((\wedge S) \rightarrow \tau_S(\varphi))$.

For the case of $[\psi!]$, from the left to the right: suppose $M|_S \models [\psi!]\varphi$, i.e. $M'' \models \varphi$ for every $M''$ such that $M|_S \xrightarrow{\psi!} M''$. Let $p$ be some fresh label, and let $M'$ be just as $M|_S$, except that $V'(p) = \|\psi\|_{M|_S}$. Observe that for every $M'''$ such that $M' \xrightarrow{\psi!} M'''$ we have $M''' = M'|_{S \cup \{p\}}$. Therefore $M'|_S \models \psi$ implies $M'|_{S \cup \{p\}} \models \varphi$. By induction hypothesis $M' \models \tau_S(\psi)$ implies $M' \models \tau_{S \cup \{p\}}(\varphi)$, i.e. $M' \models \tau_S(\psi) \rightarrow \tau_{S \cup \{p\}}(\varphi)$. Observe that $M \xrightarrow{p \rightarrow p+\psi} M'$. Therefore $M \models \tau_S(\psi) \rightarrow [p \rightarrow p+\psi](\tau_{S \cup \{p\}}(\varphi))$. We leave the right-to-left direction to the reader. $\square$

It follows that *PAL* is an extension of global modifier logic *GML*.

**Theorem 2.2** Let $\varphi$ be a formula of *PALU*, and let $M$ be any model. $M \models \varphi$ iff $M \models \tau_\emptyset(\varphi)$.

In the next section we shall introduce a proof procedure *GML* that uses reduction axioms.

## 2.3 Decidability of GML via reduction axioms

In this section we show that the new modalities that we have introduced in order to speak about modifications of graphs have reduction axioms in the style of *PAL* that allows to eliminate them.

First, if $\alpha$ is a graph modifier then the following equivalences are valid.

$$ \begin{align*} [\alpha] \neg \chi &\leftrightarrow \neg [\alpha] \chi \\ [\alpha](\chi \lor \chi') &\leftrightarrow [\alpha] \chi \lor [\alpha] \chi' \end{align*} $$

This is the case because the transition relation $M \xrightarrow{\alpha} M'$ associated to graph modifiers is a function.

The next series of valid equivalences guarantees that each of our graph modifiers
can be moved across the abstract $a$ operators.

$$[\mathbf{n}\mathbf{w}][a]\chi \leftrightarrow [a][\mathbf{n}\mathbf{w}]\chi$$

$$[\mathbf{n}\mathbf{w}][\mathbf{U}]\chi \leftrightarrow [\vec{\mathbf{n}\mathbf{w}}]\chi \wedge [\mathbf{U}][\mathbf{n}\mathbf{w}]\chi$$

$$[\vec{\mathbf{n}\mathbf{w}}][a]\chi \leftrightarrow \top$$

$$[\vec{\mathbf{n}\mathbf{w}}][\mathbf{U}]\chi \leftrightarrow [\mathbf{n}\mathbf{w}]\chi \wedge [\mathbf{U}][\mathbf{n}\mathbf{w}]\chi$$

$$[p-\varphi][a]\chi \leftrightarrow [a][p-\varphi]\chi$$

$$[p-\varphi][\mathbf{U}]\chi \leftrightarrow [\mathbf{U}][p-\varphi]\chi$$

$$[p+\varphi][a]\chi \leftrightarrow [a][p+\varphi]\chi$$

$$[p+\varphi][\mathbf{U}]\chi \leftrightarrow [\mathbf{U}][p+\varphi]\chi$$

$$[b-(\varphi, \psi)][a]\chi \leftrightarrow [a][b-(\varphi, \psi)]\chi \quad \text{if } b \neq a \\ \leftrightarrow (\neg\varphi \wedge [a][a-(\varphi, \psi)]\chi) \vee (\varphi \wedge [a](\neg\psi \rightarrow [a-(\varphi, \psi)]\chi)) \quad \text{else}$$

$$[b-(\varphi, \psi)][\mathbf{U}]\chi \leftrightarrow [\mathbf{U}][b-(\varphi, \psi)]\chi$$

$$[b+(\varphi, \psi)][a]\chi \leftrightarrow [a][b+(\varphi, \psi)]\chi \quad \text{if } b \neq a \\ \leftrightarrow [a][a+(\varphi, \psi)]\chi \wedge (\varphi \rightarrow [\mathbf{U}](\psi \rightarrow [a+(\varphi, \psi)]\chi)) \quad \text{else}$$

$$[b+(\varphi, \psi)][\mathbf{U}]\chi \leftrightarrow [\mathbf{U}][b+(\varphi, \psi)]\chi$$

Finally, once we have moved all graph modifiers 'inwards', they can be eliminated by the following equivalences.

$$[\mathbf{n}\mathbf{w}]p \leftrightarrow p$$

$$[\vec{\mathbf{n}\mathbf{w}}]p \leftrightarrow \bot$$

$$[p-\varphi]q \leftrightarrow q \quad \text{if } q \neq p \\ \leftrightarrow p \wedge \neg\varphi \quad \text{else}$$

$$[p+\varphi]q \leftrightarrow q \quad \text{if } q \neq p \\ \leftrightarrow p \vee \varphi \quad \text{else}$$

$$[a-(\varphi, \psi)]p \leftrightarrow p$$

$$[a+(\varphi, \psi)]p \leftrightarrow p$$

Putting all this together we obtain:

**Theorem 2.3** For every formula $\varphi$ there is a formula $\varphi'$ without graph modifiers such that $\varphi \leftrightarrow \varphi'$ is valid.

Moreover the above equivalences provide an effective procedure. Therefore modal logics extended with graph modifiers have the same status as their underlying 'static' modal logic w.r.t. completeness and decidability.
# 3 Local graph modifiers

Our modifiers are global in the sense that they modify the labels at every state and at every edge. In this section we have a look at local versions. These turn out to be very powerful.

In this paper we investigate state label modifiers, leaving edge label modifiers to future work. We note $p+\varphi_{loc}$ and $p-\varphi_{loc}$ the operators which only modify the truth value of $p$ in the actual state, and call $\mathcal{L}_{locGML}$ the language resulting from their addition to $\mathcal{L}_{GML}$.

## 3.1 Semantics

The transition relations $M \xrightarrow{\alpha} M'$ for local modifiers are defined as follows:

* $\langle W, w, R, V \rangle \xrightarrow{p+\varphi_{loc}} \langle W', w', R', V' \rangle$ iff
  $W' = W, w' = w, R' = R, \frac{w'' \in V'(q) \text{ iff } w'' \in V(q) \text{ for } q \neq p \text{ or } w \neq w''}{\text{and } w \in V'(p) \text{ iff } w \in V(p) \text{ or } w \in \|\varphi\|_M}$;

* $\langle W, w, R, V \rangle \xrightarrow{p-\varphi_{loc}} \langle W', w', R', V' \rangle$ iff
  $W' = W, w' = w, R' = R, \frac{w'' \in V'(q) \text{ iff } w'' \in V(q) \text{ for } q \neq p \text{ or } w \neq w''}{\text{and } w \in V'(p) \text{ iff } w \in V(p) \text{ and } w \notin \|\varphi\|_M}$.

(Remember that the relevant parts of the cases are highlighted by underlining them.)

Validity of a formula $\varphi$ in locGML is defined as usual.

## 3.2 Expressivity of locGML

In order to demonstrate the expressive power of local modifiers we give some examples.

(i) We can express that a relation is deterministic: consider the formula $\varphi_a =$

$$[p-\top][q-\top][\mathbb{U}][p+\top_{loc}][a][q+\top_{loc}][\mathbb{U}](p \to [a]q)$$

Then for any model $M = \langle W, w, R, V \rangle$, $M \models \varphi_a$ iff $R(a)$ is deterministic.

(ii) We can speak about the converse of relations. Consider the extension of the language $\mathcal{L}_{locGML}$ with the converse operator, allowing for formulas of the form $[a^{-1}]\varphi$, where $a^{-1}$ is interpreted as the converse of $a$. Then the equivalence

$$\langle a^{-1} \rangle \varphi \leftrightarrow [p-\top][p+\top_{loc}][b-(\top, \top)][b+(p, \varphi)]\langle b \rangle \langle a \rangle p$$

is valid if $p$ and $b$ do not occur in $\varphi$.

(iii) We can speak about the complement of relations. Consider the extension of the language $\mathcal{L}_{locGML}$ with the complement operator, allowing for formulas of the form $[\bar{a}]\varphi$, where $\bar{a}$ is interpreted as the complement of $a$. Then the equivalence

$$\langle \bar{a} \rangle \varphi \leftrightarrow [p-\top][p+\top_{loc}][q-\top][q+\langle a^{-1} \rangle p][b-(\top, \top)][b+(p, \neg q)]\langle b \rangle \varphi$$

is valid if $p$ and $q$ do not occur in $\varphi$.
(iv) We can define graded modal operators. For example $\langle a_{\ge 2} \rangle \varphi$ expresses that there are at least two distinct accessible states where $\varphi$ holds. Then

$$ \langle a_{\ge 2} \rangle \varphi \leftrightarrow [p-\top][p+\top_{loc}]\langle a \rangle (\varphi \wedge [q-\top][q+\top_{loc}]\langle u \rangle) (p \wedge \langle a \rangle (\varphi \wedge \neg q)) $$

is valid if $p$ and $q$ do not occur in $\varphi$.

(v) We can express that a relation $a$ is irreflexive: for any model $M = \langle W, w, R, V \rangle$, $M \models [U][p-\top][p+\top_{loc}][a] \neg p$ iff $\langle v, v \rangle \notin R(a)$ for every $v \in W$.

(vi) We can express that a relation $a$ is locally reflexive: for any model $M = \langle W, w, R, V \rangle$, $M \models [p-\top][p+\top_{loc}]\langle a \rangle p$ iff $\langle w, w \rangle \in R(a)$. This cannot be reduced to a single formula in propositional modal logic.<fnref n="10" />

Just as for global modifiers, we have the following equivalences for local modifiers w.r.t. state labels, negations and disjunctions.

$$ [p-\varphi_{loc}]q \leftrightarrow q \quad \text{if } q \neq p $$

$\leftrightarrow p \wedge \neg \varphi$ else

$$ [p+\varphi_{loc}]q \leftrightarrow q \quad \text{if } q \neq p $$

$\leftrightarrow p \vee \varphi$ else

But it is not possible to formulate reduction axioms for the cases $[p-\varphi_{loc}][a]\chi$ and $[p+\varphi_{loc}][a]\chi$.

**Theorem 3.1** *The formula $\varphi_0 = [U][p-\top][p+\top_{loc}][a] \neg p$ is not definable in GML.*

**Proof.** This formula $\varphi_0$ exactly characterizes irreflexivity of accessibility relation $a$ in models (see example (v) in Section 3.2). It is known that irreflexivity cannot be modally defined in ordinary modal logic with the universal modality. Since GML is reducible to ordinary modal logic with universal modality, the formula $\varphi_0$ cannot be definable in GML. □

**Remark 3.2** It can also be shown directly that there are no reduction axioms for locGML, by showing that there are no reduction axioms for the cases of the local modifiers. Indeed, consider the formula $[p+\top_{loc}][a]p$, and suppose there exists a formula $\varphi$ without graph modifiers such that $[p+\top_{loc}][a]p \leftrightarrow \varphi$ is valid. Now consider the models $M_1 = \langle \{w\}, w, R_1, V_1 \rangle$ and $M_2 = \langle \{w, w'\}, w, R_2, V_2 \rangle$ such that $R_1(a) = \langle \langle w, w \rangle \rangle$, $R_2(a) = \langle \langle w, w' \rangle, \langle w', w' \rangle \rangle$, and $V_1(p) = V_2(p) = \emptyset$. We have that $M_1 \models [p+\top_{loc}][a]p$. According to our hypothesis we thus must have $M_1 \models \varphi$. Since $M_1$ and $M_2$ are bisimilar, and $\varphi$ is a formula without graph modifiers we must also have $M_2 \models \varphi$, and hence $M_2 \models [p+\top_{loc}][a]p$. This is not the case, and therefore there is no formula without graph modifiers $\varphi$ such that $[p+\top_{loc}][a]p \leftrightarrow \varphi$ is valid. Similarly, it can be proved that there is no formula without modifiers that is equivalent to $[p-\top_{loc}][a]p \leftrightarrow \varphi$: just change the valuations to $V_1(p) = \{w\}$ and $V_2(p) = \{w, w'\}$.

<footnote n="10">¹⁰ The example was suggested by an anonymous reviewer of HyLo’07.</footnote>
In the next section we show that satisfiability of a formula containing local modifiers is undecidable. To that end we will reduce satisfiability in hybrid logic with binder (which is known to be undecidable) to locGML.

# 4 The relation with hybrid logics

We now investigate the relation between local modifier logic and hybrid logic.

## 4.1 Hybrid logic with binder

We recall the definition of the hybrid language with binder $\mathcal{H}(\mathbf{U}, @, \downarrow)$; for more details see [1].

Let the sets PROP and REL be as before, and let NOM = {$i_1, \dots$} (the nominals) and SVAR = {$x_1, \dots$} (the state variables). The language of $\mathcal{H}(\mathbf{U}, @, \downarrow)$ is defined by the following BNF:

$$ \varphi ::= p \mid i \mid x \mid \neg \varphi \mid \varphi \lor \varphi \mid [a]\varphi \mid [\mathbf{U}]\varphi \mid @_i \varphi \mid @_x \varphi \mid \downarrow x.\varphi $$

where p ranges over PROP, a over REL, i over NOM, and x over SVAR.

It is known that the problem of deciding satisfiability of $\mathcal{L}_{\mathcal{H}(\mathbf{U}, @, \downarrow)}$-formulas is undecidable.

Models for $\mathcal{H}(\mathbf{U}, @, \downarrow)$ are the usual ones for modal logic, i.e. 4-tuples $M = \langle W, w, R, V \rangle$ as defined in Section 1, where the valuation $V$ not only maps atoms $p$ to subsets of $W$, but also maps nominals $i$ to unique elements of $W$. An assignment $g$ for $M$ is a mapping $g : SVAR \to M$. Given $x \in SVAR$ and $w \in W$, an assignment $g_w^x$ is an $x$-variant of $g$ iff $g_w^x(x) = w$ and $g_w^x(y) = g(y)$ for all $y \neq x$.

Truth of a formula $\varphi$ given a model $M = \langle W, w, R, V \rangle$ and an assignment $g$ is defined as follows:

$$ M, g \models p \quad \text{iff} \quad w \in V(p) $$

$$ M, g \models i \quad \text{iff} \quad w = V(i) $$

$$ M, g \models x \quad \text{iff} \quad w = g(x) $$

$$ M, g \models [a]\varphi \quad \text{iff} \quad \langle W, w', R, V \rangle, g \models \varphi, \text{ for every } w' \text{ such that } \langle w, w' \rangle \in R(a) $$

$$ M, g \models [\mathbf{U}]\varphi \quad \text{iff} \quad \langle W, w', R, V \rangle, g \models \varphi, \text{ for every } w' \in W $$

$$ M, g \models @_i \varphi \quad \text{iff} \quad \langle W, V(i), R, V \rangle, g \models \varphi $$

$$ M, g \models @_x \varphi \quad \text{iff} \quad \langle W, g(x), R, V \rangle, g \models \varphi $$

$$ M, g \models \downarrow x.\varphi \quad \text{iff} \quad \langle W, g, R, V \rangle, g_w^x \models \varphi $$

and as usual for the boolean operators.

Validity of a formula $\varphi$ is defined as usual, and is noted $\models_{\mathcal{H}(\mathbf{U}, @, \downarrow)} \varphi$.
## 4.2 Local graph modifier logic is undecidable

Here is a translation from the language of $\mathcal{H}(U, @, \downarrow)$ into $\mathcal{L}_{locGML}$. Let $\varphi_0$ be a given $\mathcal{L}_{\mathcal{H}(U, @, \downarrow)}$-formula. We recursively define the following mapping $\tau$ on the set of subformulas of $\varphi_0$.

$$ \tau(p) = p $$

$$ \tau(i) = p_i \text{ where } p_i \in \text{PROP} \text{ does not occur in } \varphi_0 $$

$$ \tau(x) = p_x \text{ where } p_x \in \text{PROP} \text{ does not occur in } \varphi_0 $$

$$ \tau(\neg\varphi) = \neg\tau(\varphi) $$

$$ \tau(\varphi \lor \psi) = \tau(\varphi) \lor \tau(\psi) $$

$$ \tau([a]\varphi) = [a]\tau(\varphi) $$

$$ \tau([\mathbf{U}]\varphi) = [\mathbf{U}]\tau(\varphi) $$

$$ \tau(@_i\varphi) = \langle\mathbf{U}\rangle(p_i \land \tau(\varphi)) $$

$$ \tau(@_x\varphi) = \langle\mathbf{U}\rangle(p_x \land \tau(\varphi)) $$

$$ \tau(\downarrow x.\varphi) = [p_x - \top][p_x + \top_{loc}]\tau(\varphi) $$

We state the following lemma without proof.

**Lemma 4.1** Let $\varphi_0$ be a $\mathcal{L}_{\mathcal{H}(U, @, \downarrow)}$-formula. Let $M = \langle W, w, R, V \rangle$ be a $\mathcal{H}(U, @, \downarrow)$-model, and let $g$ be an assignment of variables on $M$. Let $M' = \langle W', w', R', V' \rangle$ be a locGML-model corresponding with $M$ and $g$, in the sense that $W' = W$, $w = w'$, $a = a'$, $V'(p) = V(p)$ for every $p$ occurring in $\varphi_0$, $V'(p_i) = V(i)$ for $i \in \text{NOM}$, and $V'(p_x) = g(x)$ for $x \in \text{SVAR}$. Then $M, g \models \varphi_0$ iff $M' \models \tau(\varphi_0)$.

## Corollary 4.2 The logic locGML is undecidable.

## 4.3 $\mathcal{H}(U, @, \downarrow)$ contains a fragment of local graph modifier logic

Now we give a translation of the fragment of the language $\mathcal{L}_{locGML}$ without edge modifiers $a-(\varphi, \psi)$ and $a+(\varphi, \psi)$ and without state creators $\mathbf{nw}$ and $\overrightarrow{\mathbf{nw}}$, into the language of hybrid logic with binder.

Given countably infinite sets PROP of state labels, REL of edge labels, and SVAR of variables, our translation will be parametrized by sequences $\sigma$ that keep track of the modifiers that have occurred. Its elements are of the form $\langle p, -\varphi \rangle$, $\langle x, p, -\varphi \rangle$, $\langle p, +\varphi \rangle$, and $\langle x, p, +\varphi \rangle$. For example, the first element stores that the interpretation of $p$ has been globally diminished by that of $\varphi$, and the last one stores that at the state $g(x)$, the interpretation of $p$ has been locally augmented by that of $\varphi$. The empty such sequence is noted $\epsilon$, and concatenation is noted “;”.

Consider the set of $\mathcal{L}_{locGML}$-formulas which do not contain any occurrence of edge modifiers or state creators. Here is a translation mapping this fragment into $\mathcal{L}_{\mathcal{H}(U, @, \downarrow)}$. The first 8 cases ‘stack’ the modifiers in the sequence $\sigma$, while the last 6
cases ‘unstack’ the modifiers.

$$
\begin{align*}
\tau_{\sigma}(\neg\varphi) &= \neg\tau_{\sigma}(\varphi) \\
\tau_{\sigma}(\varphi \lor \psi) &= \tau(\varphi) \lor \tau_{\sigma}(\psi) \\
\tau_{\sigma}([a]\varphi) &= [a]\tau_{\sigma}(\varphi) \\
\tau_{\sigma}([\mathbf{U}]\varphi) &= [\mathbf{U}]\tau_{\sigma}(\varphi) \\
\tau_{\sigma}([p+\varphi]\psi) &= \tau_{\sigma;\langle p,+\varphi\rangle}(\psi) \\
\tau_{\sigma}([p+\varphi_{\text{loc}}]\psi) &= \searrow x.\tau_{\sigma;\langle x,p,+\varphi\rangle}(\psi) \quad \text{where } x \text{ is new} \\
\tau_{\sigma}([p-\varphi]\psi) &= \tau_{\sigma;\langle p,-\varphi\rangle}(\psi) \\
\tau_{\sigma}([p-\varphi_{\text{loc}}]\psi) &= \searrow x.\tau_{\sigma;\langle x,p,-\varphi\rangle}(\psi) \quad \text{where } x \text{ is new} \\
\tau_{\epsilon}(p) &= p \\
\tau_{\sigma;\langle p,+\varphi\rangle}(q) &= \tau_{\sigma}(q) \\
&= \tau_{\sigma;\langle p,-\varphi\rangle}(q) = \tau_{\sigma;\langle x,p,+\varphi\rangle}(q) = \tau_{\sigma;\langle x,p,-\varphi\rangle}(q) = \tau_{\sigma;\langle p,+\varphi\rangle}(p) \\
&\qquad \text{if } q \neq p \\
\tau_{\sigma;\langle p,+\varphi\rangle}(p) &= \tau_{\sigma}(p) \lor \tau_{\sigma}(\varphi) \\
\tau_{\sigma;\langle x,p,+\varphi\rangle}(p) &= \tau_{\sigma}(p) \lor (x \land \tau_{\sigma}(\varphi)) \\
\tau_{\sigma;\langle p,-\varphi\rangle}(p) &= \tau_{\sigma}(p) \land \neg\tau_{\sigma}(\varphi) \\
\tau_{\sigma;\langle x,p,-\varphi\rangle}(p) &= \tau_{\sigma}(p) \land \neg(x \land \tau_{\sigma}(\varphi))
\end{align*}
$$

We can prove now that the two languages have the same expressivity.

**Theorem 4.3** Let $\varphi_0$ be a $\mathcal{L}_{\text{locGML}}$-formula that neither contains edge modifiers nor state creators. Let $M = (W, w, R, V)$ be a $\mathcal{H}(U, @, \downarrow)$-model (that is also a locGML-model). Then $M \models \varphi_0$ iff $M, g \models \tau_\epsilon(\varphi_0)$ for every variable assignment $g$ on $M$.

**Proof.** First of all, it will be useful to consider that the models of locGML are couples $(M, g)$, where $g$ is an assignment. As $g$ plays no role in the evaluation of locGML-formulas this can be done without harm; $g$ will be useful to record where the graph has been modified locally.

Given a model $M$, an assignment $g$ and a sequence of model modifications $\sigma$, we recursively define a transformation $\langle M, g \rangle^\sigma$ of $\langle M, g \rangle$ in the following way:

$$
\begin{align*}
\langle M, g \rangle^{\epsilon} &= \langle M, g \rangle \\
\langle M, g \rangle^{\sigma; \langle p, +\varphi \rangle} &= \langle M', g \rangle, \quad \text{where } \langle M', g \rangle \text{ is as } \langle M, g \rangle^{\sigma}, \text{ except } V'(p) = V^{\sigma}(p) \cup \|\varphi\|_{\langle M, g \rangle^{\sigma}} \\
\langle M, g \rangle^{\sigma; \langle x, p, +\varphi \rangle} &= \langle M', g \rangle, \quad \text{where } \langle M', g \rangle \text{ is as } \langle M, g \rangle^{\sigma}, \text{ except } V'(p) = V^{\sigma}(p) \cup (\|\varphi\|_{\langle M, g \rangle^{\sigma}} \cap \{g(x)\}) \\
\langle M, g \rangle^{\sigma; \langle p, -\varphi \rangle} &= \langle M', g \rangle, \quad \text{where } \langle M', g \rangle \text{ is as } \langle M, g \rangle^{\sigma}, \text{ except } V'(p) = V^{\sigma}(p) \setminus \|\varphi\|_{\langle M, g \rangle^{\sigma}} \\
\langle M, g \rangle^{\sigma; \langle x, p, -\varphi \rangle} &= \langle M', g \rangle, \quad \text{where } \langle M', g \rangle \text{ is as } \langle M, g \rangle^{\sigma}, \text{ except } V'(p) = V^{\sigma}(p) \setminus (\|\varphi\|_{\langle M, g \rangle^{\sigma}} \cap \{g(x)\})
\end{align*}
$$

We then prove that for every sequence $\sigma$ and atom $p$ we have:

$$ \langle M, g \rangle^{\sigma} \models p \text{ iff } M, g \models \tau_{\sigma}(p) $$

(by induction on the length of $\sigma$). This provides the base case of the next inductive
Their formula $[a - \exists]\varphi$ can be expressed in our framework as:

$$[a-(\mathit{here}, \top)][a+\mathit{here}_{\mathit{loc}}\top]\langle a \rangle[a-(\mathit{there}, \top)][a+\mathit{there}_{\mathit{loc}}\top][a-(\mathit{here}, \mathit{there})]\varphi$$

for some fresh labels *here* and *there*. The sequence $[a-(\mathit{here}, \top)][a+\mathit{here}_{\mathit{loc}}\top]$ is used to 'mark' the current node by labelling it with *here*, and similarly for *there*. It therefore comes without surprise that the logic of sabotage modal operators is undecidable.

Pucella and Weissman [7] have studied the logic of global graph modifiers in a deontic framework. Adding edges from $\varphi$- to $\psi$-worlds to the accessibility relation corresponds to granting permissions, and removing edges from $\varphi$- to $\psi$-worlds corresponds to revoking permissions.

# 6 Conclusion

We have investigated the logic of graph modifications. We have done this mainly in terms of two modal connectives. We have studied global modifications, and have shown that the resulting logic generalizes the logic of public announcements and assignments. We have then added local modifications: we have shown that the logic is undecidable, and that its fragment without edge modifiers and state creators has the same expressivity as hybrid logic with binder.

As we just said, our logic generalizes the logic of public announcements and the logic of public assignments. While in the preceding logics *all* labels of a certain kind are eliminated, the logic of Baltag et al. [2] allows a more fine-grained elimination of edges depending on their labels, in a way that is specified by a so-called event-model. We do not know yet how to simulate it with our graph modifiers.

We terminate with a list of open problems.

(i) What is the complexity of model checking?

(ii) Given that satisfiability of *locGML*-formulas is undecidable, are there fragments of the language that are decidable? For example, consider the language without global modifiers, or the language without the universal modality.

(iii) Consider the extension of PLTL by global and local modifiers (or a fragment of it). Is satisfiability in the resulting logic decidable, and what is the complexity of the decision problem?

(iv) Is satisfiability of formulas in the class of finite models decidable?

(v) Is satisfiability of formulas with only one atomic action decidable? What about restrictions to the out-degree of $R(a)$:

* for all $w$, $\mathrm{card}(R(a)(w)) < 2$

* for all $w$, $\mathrm{card}(R(a)(w)) < k$ for $k \ge 3$

* for all $w$, $\mathrm{card}(R(a)(w)) < \omega$

# References

[1] Carlos Areces and Balder ten Cate. Hybrid logics. In Patrick Blackburn, Johan van Benthem, and Frank Wolter, editors, *Handbook of Modal Logic*, volume 3. Elsevier Science, 2006.
[2] Alexandru Baltag, Lawrence S. Moss, and Slawomir Solecki. The logic of public announcements, common knowledge, and private suspicions. In *Proc. TARK'98*, pages 43–56. Morgan Kaufmann, 1998.

[3] Ronald Fagin and Moshe Y. Vardi. An internal semantics for modal logic: preliminary report. In *Proc. of the 17th Annual ACM Symposium on Theory of Computing*, pages 305–315. ACM, New York, 1985.

[4] Barteld Kooi. Expressivity and completeness for public update logic via reduction axioms. *Journal of Applied Non-Classical Logics*, 17(2):231–254, 2007.

[5] Christof Löding and Philipp Rohde. *FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science*, chapter Model Checking and Satisfiability for Sabotage Modal Logic, pages 302–313. Number 2914 in LNCS. Springer Verlag, 2003.

[6] Jan A. Plaza. Logics of public communications. In M. L. Emrich, M. Z. Pfeifer, M. Hadzikadic, and Z. W. Ras, editors, *Proc. 4th Int. Symposium on Methodologies for Intelligent Systems*, pages 201–216, 1989.

[7] Riccardo Pucella and Vicky Weissman. Reasoning about dynamic policies. In *Proc. FOSSACS'2004*, 2004.

[8] Gerard R. Renardel de Lavalette. Changing modalities. *Journal of Logic and Computation*, 14(2):253–278, 2004.

[9] Johan van Benthem. An essay on sabotage and obstruction. In Dieter Hutter and Werner Stephan, editors, *Mechanizing Mathematical Reasoning — Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday*, number 2605 in LNCS. Springer Verlag, 2005.

[10] Johan van Benthem. One is a lonely number: on the logic of communication. In Z. Chatzidakis, P. Koepke, and W. Pohlers, editors, *Logic Colloquium'02*, pages 96–129. ASL & A.K. Peters, Wellesley MA, 2006. Tech Report PP-2002-27, ILLC Amsterdam (2002).

[11] Johan van Benthem and Fenrong Liu. Dynamic logic of preference upgrade. *Journal of Applied Non-Classical Logics*, 17(2), 2007.

[12] Hans P. van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi. Dynamic epistemic logic with assignment. In *Proc. AAMAS'05*, pages 141–148, 2005.

[13] Moshe Y. Vardi. Why is modal logic so robustly decidable? In N. Immerman and Ph. Kolaitis, editors, *Descriptive Complexity and Finite Models*, volume 31 of *DIMACS Series in Discrete Mathematics and Theoretical Computer Science*, pages 149–184. American Mathematical Society, 1997.