The Universal Tangle for Spatial Reasoning

Abstract

The topological $\mu$-calculus has gathered attention in recent years as a powerful framework for representation of spatial knowledge. In particular, spatial relations can be represented over finite structures in the guise of weakly transitive (wK4) frames. In this paper we show that the topological $\mu$-calculus is equivalent to a simple fragment based on a variant of the ‘tangle’ operator. Similar results were proven for transitive frames by Dawar and Otto, using modal characterisation theorems for the corresponding classes of frames. However, since these theorems are not available in our setting, which has the upshot of providing a more explicit translation and upper bounds on formula size.

Supported by the FWO-FWF Lead Agency grant G030620N (FWO)/I4513N (FWF) and by the SNSF–FWO Lead Agency Grant 200021L_196176/G0E2121N.

1 Introduction

Qualitative spatial reasoning aims to capture basic relations between regions in space in a way that is computationally efficient and thus suitable for knowledge representation and AI (see [4, 17] for overviews). The region connection calculus ($\textsf{RCC8}$) [6, 16] deals with relations such as ‘partially overlaps’ (e.g. Mexico and Mesoamerica) or ‘is a non-tangential proper part’ (e.g. Paraguay and South America) while avoiding undecidability phenomena by not allowing for quantification over points or regions.

$\textsf{RCC8}$ can be embedded into modal logic ($\textsf{ML}$) with a universal modality [18]. This allows us to import many techniques from $\textsf{ML}$, including the representation of regions using transitive Kripke frames, i.e. pairs $\langle W,\sqsubset \rangle$, where W is a set of points and $\sqsubset$ is a transitive relation representing ‘nearness’. It also tells us that little is lost by omitting quantifiers, due to so-called modal characterization theorems [14], which state that $\textsf{ML}$ is the bisimulation-invariant fragment of first order logic ($\textsf{FOL}$), while its extension to the modal $\mu$-calculus is the bisimulation-invariant fragment of monadic second order logic ($\textsf{MSO}$) [12].

However, these results apply to frames where $\sqsubset$ is an arbitrary relation, whereas Dawar and Otto [5] showed that the situation over finite, transitive frames is subtle. In this setting, the bisimulation-invariant fragments of $\textsf{FOL}$ and $\textsf{MSO}$ coincide, but are stronger than modal logic. They are in fact equal to the $\mu$-calculus, but this in turn can be greatly simplified to its tangled fragment, which adds expressions of the form $\diamond ^\infty \{\varphi _1,\ldots ,\varphi _n\}$, stating that there is an accessible cluster of reflexive points where each $\varphi _i$ is satisfied.

Finite, transitive frames are suitable for representing spatial relations on metric spaces, such as Euclidean spaces or the rational numbers [10, 13]. However, for the more general setting of topological spaces, one must consider a wider class of frames called weakly transitive frames: a relation $\sqsubset$ is weakly transitive if $x\sqsubset y\sqsubset z$ implies $x\sqsubseteq z$. The modal logic of finite, weakly transitive frames is precisely that of all topological spaces [7], and this result extends to the full $\mu$-calculus [2]. In this spatial setting, Dawar and Otto’s tangled operator becomes the tangled derivative, the largest subspace in which two or more sets are dense: for example, the tangle of $\mathbb Q$ and $\mathbb R\setminus \mathbb Q$ is the full real line, since the rationals and the irrationals are both dense in $\mathbb R$. In the case of a single subset A, $\Diamond ^\infty \{A\}$ is the perfect core of A, i.e. its largest perfect subset, a notion useful in describing the limit of learnability after iterated measurements [1].

Alas, over the class of weakly transitive frames, the tangled derivative is not as expressive as the $\mu$-calculus [2], which is in turn less expressive than the bisumulation-invariant fragment of $\textsf{MSO}$, so Dawar and Otto’s result fails. Gougeon [11] proposed a more expressive operator, which here we simply dub the tangle and denote by , which coincides with the tangled derivative over metric spaces (and other spaces satisfying a regularity property known as $T_D$ spaces), but is strictly more expressive over the class of topological spaces. While this tangle cannot be as expressive as the bisimulation-invariant fragment of $\textsf{MSO}$, it was still conjectured to be as expressive as the $\mu$-calculus, thus providing a streamlined framework for representing spatial properties relevant for the learnability framework of [1]. This conjecture is supported by the recent result stating that the topological $\mu$-calculus collapses to its alternation-free fragment [15].

In this paper we give an affirmative answer to this conjecture. Moreover, since we cannot use games for $\textsf{FOL}$ to establish our results, our proof uses new methods which have the advantage of providing an explicit translation of the $\mu$-calculus into tangle logic. Among other things, we provide an upper bound on formula size, which is doubly exponential. It is not clear if this can be greatly improved, given the exponential lower bounds of [8].

Despite the spatial motivation for the $\mu$-calculus over wK4, the results of [2] allow us to work within the class of weakly transitive frames; since their logic is that of all topological spaces, our expressivity results lift to that context as well. The upshot is that background in topology is not needed to follow the text.

Layout

In Sect. 2 we review the $\mu$-calculus, present Gougeon’s tangle and some basic semantic notions over path-finite weakly transitive (wK4) frames. Section 3 begins with a review of finality as used in [2], as well as establishing additional properties we need. In Sect. 4 we construct some formulae in the tangle logic that peer into the structure of a given Kripke model, which we use to show that the $\mu$-calculus is equivalent to the tangle logic and strictly weaker than the bisimulation invariant part of first order logic over finite and path finite wK4 frames.

2 Preliminaries

As is often the case when working with $\mu$-calculi, it will be convenient to define the $\mu$-calculus with each of the positive operations, including $\nu x. \varphi$, as primitive, and with negation being only subsequently defined.

Definition 1

The language of the modal $\mu$-calculus $\mathcal {L}_{\mu }$ is defined by the following syntax:

$$\begin{aligned} \varphi {::}= \top \, | \, x \, | \, p \, | \, \lnot p\, |\, \varphi \wedge \varphi \, |\, \varphi \vee \varphi \, |\, \Diamond \varphi \,|\, \Box \varphi \,|\, \nu x. \varphi (x) \,|\, \mu x. \varphi (x) \end{aligned}$$

where x belongs to a set of ‘variables’ and p to a set of ‘constants’, denoted $\mathbb {P}$.

Under this presentation of the language, the formulas are said to be in negation normal form. Negation is defined classically as usual with $\lnot \nu x. \varphi (x) := \mu x. \lnot \varphi (\lnot x)$ and $\lnot \mu x. \varphi (x) := \nu x. \lnot \varphi (\lnot x)$. We also write and similarly .

The following is the standard semantics for the $\mu$-calculus over frames with a single relation $\sqsubset$ (or $\sqsubset _M$, to specify the frame).

Definition 2

A Kripke frame is a tuple $\mathcal {F}= \langle M,\sqsubset _M\rangle$ where ${\sqsubset _M} \subseteq M\times M$. A Kripke model is a triple $\mathcal {M}= \langle M,\sqsubset _M,\Vert \cdot \Vert _M\rangle$ where $\langle M,\sqsubset _M \rangle$ is a Kripke frame with a valuation $\Vert \cdot \Vert _M:\mathbb {P}\rightarrow \mathcal {P}(M)$. In the sequel, we will use $\mathcal {M}$ and M interchangeably. We denote the reflexive closure of $\sqsubset _M$ by $\sqsubseteq _M$.

Given $A \subseteq M$, we denote the irreflexive and reflexive upsets of A as $A{\uparrow _M} := \{ w \in M : \exists v \in A \ v \sqsubset _M w\}$ and $A{\uparrow ^*_M} := A{\uparrow _M} \cup A$ respectively. The downsets are similarly denoted as $A{\downarrow _M}:= \{ w \in M : \exists v \in A \ w \sqsubset _M v\}$ and $A{\downarrow ^*_M}:= A{\downarrow _M} \cup A$ respectively. We will omit the M in the subscript when we will be only referring to a single model.

The valuation $\Vert \cdot \Vert = \Vert \cdot \Vert _M$ is defined as usual on Booleans with:

$$\begin{array}{lcl} \Vert \Diamond \varphi \Vert := \Vert \varphi \Vert {\downarrow } &{} \ \ \ \ \ {} &{} \Vert \mu x. \varphi (x)\Vert := \bigcap \{ X \subseteq M : X = \Vert \varphi (X)\Vert \} \\ \Vert \Box \varphi \Vert := M\setminus (( M\setminus \Vert \varphi \Vert ) {\downarrow }) &{}&{} \Vert \nu x. \varphi (x)\Vert := \bigcup \{ X \subseteq M : X = \Vert \varphi (X)\Vert \} \end{array}$$

Given a Kripke model M and a world $w \in M$ we say a formula $\varphi$ is satisfied by M at the world w and write $w \vDash _M \varphi$ iff $w \in \Vert \varphi \Vert _M$.

A formula $\varphi$ is valid over a class of models $\varOmega$ if for every $M\in \varOmega$, $\Vert \varphi \Vert _M=M$.

We note that $\mu x. \varphi (x)$ and $\nu x. \varphi (x)$ are the least and greatest fixed points, respectively, of the operator $X\mapsto \varphi (X)$.

We will mostly concern ourselves only with weakly transitive frames. A relation R is weakly transitive iff for all a, b, c where $a \ne c$, if aRb and bRc then aRc. A frame or model is weakly transitive if its accessibility relation is.

Example 1

Consider a frame $\mathcal F$ consisting of two irreflexive points $\{0,1\}$ such that $0\sqsubset 1$ and $1\sqsubset 0$; this frame is weakly transitive since $x\sqsubset y\sqsubset z$ implies $x=z$, but it is not transitive since e.g. $0\sqsubset 1\sqsubset 0$ but . To extend this frame into a model, we assign subsets of $\{0,1\}$ to each propositional variable. Assume that our variables are e (even), o (odd), p (positive) and i (integer). We obtain a valuation $\Vert \cdot \Vert$ if we let $\Vert e\Vert = \{0\}$, $\Vert o\Vert = \{1\}$, $\Vert p\Vert = \{1\}$, and $\Vert i\Vert = \{0,1\}$. Then, $\Vert o\vee \Diamond p\Vert =\{0,1\}$, since every element of our model is either odd or has an accessible positive point. We may say that this formula is valid in our model.

Recall that a topological space is a pair $\langle X,\mathcal T\rangle$, where $\mathcal T$ is a family of subsets of X (called the open sets) closed under finite intersections and arbitrary unions. If $A\subseteq X$, d(A) is the set of points $x\in X$ such that whenever $x\in U$ and U is open, there is $y\in A\cap U\setminus \{x\}$; this is the set of limit points of A. The topological semantics for the $\mu$-calculus is obtained by modifying Definition 2 by setting $\Vert \Diamond \varphi \Vert =d\Vert \varphi \Vert$. This is the basis to the modal approach to spatial reasoning, but the following allows us to work with weakly transitive frames instead.

Theorem 1

([2]). For $\varphi \in \mathcal L_\mu$, the following are equivalent:

• $\varphi$ is valid over the class of all topological spaces.

• $\varphi$ is valid over the class of all weakly transitive frames.

• $\varphi$ is valid over the class of all finite, irreflexive, weakly transitive frames.

This extends results of Esakia for the purely modal setting [7]. Next we recall bisimulations (see e.g. [3]), which are binary relations preserving truth of $\mu$-calculus formulas that will be very useful in the rest of the text.

Definition 3

Given $P\subseteq \mathbb {P}$ a P-bisimulation is a relation $\iota \subseteq M \times N$ such that, whenever $\langle u,v \rangle \in \iota$:

atoms:

$w\vDash _M p \, \Leftrightarrow v \vDash _M p$ for all $p \in P$;

forth:

If $u \sqsubset _M u'$, then there is $v \sqsubset _N v'$ such that $\langle u' , v' \rangle \in \iota$;

back:

If $v \sqsubset _N v'$, then there is $u \sqsubset _M u'$ such that $\langle u' , v' \rangle \in \iota$;

global:

$dom(\iota )= M$ and $rng(\iota ) = N$.

Two models are called P-bisimilar and we write $M \rightleftharpoons _P N$ if there is some P-bisimulation relation between them. Given subsets $A\subseteq M$ and $B \subseteq N$, we write $A \rightleftharpoons _P B$ when $M\upharpoonright A \rightleftharpoons _P N \upharpoonright B$, where $\upharpoonright$ denotes the usual restriction to a subset of the domain.

In the sequel we will omit the P in the subscript and assume it to be the set of constants occurring in some ‘target’ formula $\varphi$. As mentioned, bisimulations are useful because they preserve the truth of all $\mu$-calculus formulas, i,e. if $\langle w,v\rangle \in \iota$ and $\varphi$ is any formula (with constants among P), then $w\in \Vert \varphi \Vert$ iff $v\in \Vert \varphi \Vert$. As such, since every weakly transitive model is bisimilar to an irreflexive weakly transitive model, we will make the convention that every arbitrary model mentioned in this paper is irreflexive.

As a general rule, the $\mu$-calculus is more expressive than standard modal logic: for example, in a frame (W, R), reachability via the transitive closure of R is expressible in the $\mu$-calculus, but not in standard modal logic. However, in the setting of transitive frames, reachability is already modally definable (since R is its own transitive closure), which means that the familiar examples to show that the $\mu$-calculus is more powerful than modal logic do not apply. Dawar and Otto [5] exhibited an operator, since dubbed the tangle, which is $\mu$-calculus expressible but not modally expressible. They showed the surprising result that every formula of the $\mu$-calculus can be expressed in terms of tangle. In this paper, we will use a variant introduced by Gougeon [11]. When working with multisets¹, if x occurs n times in A then it occurs $\max \{0,n-1\}$ times in $A\setminus \{x\}$.

Definition 4

Given a finite multiset of formulae $\varGamma \subseteq \mathcal {L}_{\mu }$, the tangle modality is defined as follows:

where x does not appear free in any $\varphi \in \varGamma$.

We can then define the tangle logic whose language is defined by the syntax, where is a multiset:

It can be checked that over transitive frames, is equivalent to the ‘tangled derivative’ $\Diamond ^\infty \varGamma$ [10], given by $\Diamond ^{\infty }\varGamma := \nu x. \bigwedge _{ \varphi \in \varGamma } \Diamond (\varphi \wedge x)$. The two are also equivalent over familiar spaces such as the real line, but not over arbitrary topological spaces or weakly transitive frames, in which case can define $\Diamond ^\infty$ but not vice-versa [11]. In metric spaces such as the real line (and a wider class known as $T_D$ spaces), holds on x if there is a perfect set A (i.e., A has no isolated points) containing x such that for each $\varphi \in \varGamma$, $\Vert \varphi \Vert \cap A$ is dense in A.

Example 2

Consider a topological model based on the real line $\mathbb R$ with $\Vert r\Vert$ being the set of rational points and $\Vert i\Vert$ the set of irrational points. Then, is valid on the real line, given that the sets of rational and irrational numbers are both dense. In contrast, if we let $\Vert z\Vert$ be the set of integers, we readily obtain that evaluates to the empty set, given that the subspace of the integers consists of isolated points and hence we will not find any common perfect core between $\Vert z\Vert$ and $\Vert i\Vert$.

The tangle simplifies a bit when working over finite transitive frames. In this case, this operator is best described in terms of clusters. A cluster C of a model $\mathcal {M}=\langle M, \sqsubset , \Vert \cdot \Vert \rangle$ is a subset of M such that $\forall u,v\in C \, u \sqsubseteq v$. Note that we don’t define clusters to be maximal (with respect to set inclusion). In contrast, the cluster of w in M is the set $C_w= \bigcup \{ C : C \text { is a cluster of M and } w \in C \}$.

It is well known that a transitive relation (and indeed even a weakly transitive relation) can be viewed as a partial order on its set of maximal clusters. To this end, define $w\prec v$ if , and for $A,B \subseteq M$, we write:

• $A \prec B$ iff

• $A \preceq B$ iff $\forall v \in B\, \exists u \in A \, u \sqsubseteq v$.

Then, $\prec$ is a strict partial order on the maximal clusters of M. In the sequel, A, B will usually be nonempty clusters. We also define e.g. $w\prec A$ by identifying w with $\{w\}$.

Lemma 1

Fix a multiset $\varGamma$ and a finite pointed model (M, w), we have that iff there is a cluster C of M such that $w \preceq C$ and a map $f:C\rightarrow \varGamma$ such that $u\in \Vert f(u)\Vert$ for all $u \in C$, and whenever $\varphi \in \varGamma \setminus \{f(u)\}$, then there is $v\in C$ such that $u\sqsubset v \in C$ and $v \in \Vert \varphi \Vert$.

Example 3

Recall the model of Example 1, consisting of an irreflexive cluster $\{0,1\}$ with $\Vert e\Vert = \{0\}$, $\Vert o\Vert = \{1\}$, $\Vert p\Vert = \{1\}$, and $\Vert i\Vert = \{0,1\}$. We then have that , since each point is either even and has an accessible point that is odd, or vice-versa. On the other hand, , since we cannot assign any atom $a\in \{o,p\}$ to 1 in such a way that 1 satisfies , where $a'$ is the complementary atom to a. And if 0 were to satisfy , then 1 would also have to satisfy , something we have already shown to be impossible. Thus it is not enough for each element of $\varGamma$ to be satisfied in a cluster in order to make true: instead, each point w must have an accessible world satisfying all but possibly one element $\varphi _w$ of $\varGamma$, in which case it must also satisfy $\varphi _w$.

3 Final Submodels

The technique of final worlds is a powerful tool in establishing the finite model property for many transitive modal logics [9], and is also applicable to the $\mu$-calculus over weakly transitive frames [2]. The idea here is that only a few worlds in a model contain ‘useful’ information, and the rest can be deleted. These ‘useful’ worlds are those that are maximal (or final) with respect to $\sqsubseteq$, among those satisfying a given formula of $\varSigma$.

Definition 5

($\varSigma$-final). Given a model M and a set of formulas $\varSigma$, a world $w\in M$ is $\varSigma$-final if there is some formula $\varphi \in \varSigma$ such that $w \vDash _M \varphi$ and if $w\sqsubset u$ and $u \vDash _M \varphi$, then $u \sqsubset w$.

A set $A\subseteq M$ will be called $\varSigma$-final iff every $w\in A$ is $\varSigma$-final. The $\varSigma$-final part of M is the largest $\varSigma$-final subset of M and we denote it by $M^\varSigma$.

Sometimes we need to ‘glue’ a root cluster to a $\varSigma$-final model. To this end, a rooted model (M, w) will be called $\varSigma$-semifinal if $M\setminus C_w$ is $\varSigma$-final.

Baltag et al. [2] built on ideas of Fine [9] to show via final submodels that the topological $\mu$-calculus has the finite model property. While final submodels are not necessarily finite (if M is infinite), they do have finite depth. Given a model M, a set of formulas $\varSigma$ and $w \in M$, we define the depth of w in M, denoted $dpt ^M (A)$, as the supremum of all n such that $w=w_0 \prec w_1\prec w_2\prec \ldots \prec w_n$ (recall that $\prec$ is the strict part of $\sqsubset$); note that this is finite on finite weakly transitive models but could be infinite on infinite ones. For $A \subseteq M$ we define the depth of A in M to be $dpt ^M(A) = \sup (0\cup \{ dpt ^M (w):w\in A \})$. The $\varSigma$-depth of w is defined analogously, except that here we only consider chains such that $w_1,\ldots ,w_n\in M^\varSigma$ (note that w itself need not be $\varSigma$-final). Then we define $dpt_\varSigma ^M(A)$ as before. It is not hard to check that $dpt_\varSigma ^M(w)$ is bounded by $|\varSigma |$, and thus if $\varSigma$ is finite we can immediately control the depth of any $\varSigma$-final model. From a model of finite depth, it is easy to obtain a finite model.

In order to use this idea towards a proof of the finite model property (and also for our own results), one must carefully choose $\varSigma$ so that for any $\varphi \in \varSigma$ and $w\in M^\varSigma$, we have that $M^\varSigma ,w\equiv _\varSigma M,w$. For example, $\varSigma$ should be closed under subformulas, but since we are in the $\mu$-calculus, we will have to find a way to treat the free variables that show up in said subformulas. Because of this, we define a variant of the set of subformulas of a given formula where any free occurrence of a variable is labelled according to its binding formula, thus making sure that the same variable does not appear free with different meanings. We also need to treat reflexive modalities as if they were primitive.

Definition 6

We define the modified subformula operator $sub^*:\mathcal {L}_{\mu }\rightarrow \mathcal {P}(\mathcal {L}_{\mu })$ recursively by

• $sub^*(r) = \{r\}$ if $r = \top , p, x$;

• $sub^*(\lnot p) = \{ \lnot p , p\}$;

• $sub^*(\varphi \ocircle \psi ) = \{ \varphi \ocircle \psi \} \cup sub^*(\varphi )\cup sub^* (\psi )$ where $\ocircle = \wedge \text { or } \vee$ and for some $\sigma$;²

• $sub^*(\ocircle \psi ) = \{ \psi \}\cup sub^*(\psi )$ where or ;

• $sub^* (\nu x. \varphi ) = \{ \varphi (x_{\nu x.\varphi })\}\cup sub^*(\varphi (x_{\nu x.\varphi }))$ where $x_{\nu x.\varphi }$ is a fresh propositional variable named after $\nu x. \varphi$;

• $sub^* (\mu x. \varphi ) = \{ \varphi (x_{\mu x.\varphi })\}\cup sub^*(\varphi (x_{\mu x.\varphi }))$ where $x_{\mu x.\varphi }$ is a fresh propositional variable named after $\mu x. \varphi$.

Given a set of formulae $\varSigma$, we can define a partial order on $sub^*[\varSigma ]$ by $\varphi <_{sub^*} \psi$ iff $\varphi \in sub^* (\psi )$ and $\varphi \ne \psi$.

Observe that if $x_\psi$ is a free variable of $\varphi$, then $\varphi <_{sub^*} \psi$. So we will work with these altered subformulas, but we also need to close $\varSigma$ under some further operations. Given a set $\mathbb {X}$, some $Y \subseteq \mathbb {X}$ and a set $\mathcal {A}$ of mappings $a: \mathbb {X} \rightarrow \mathcal {P}(\mathbb {X})$, we define the closure of Y over $\mathbb {X}$ inductively as follows:

• $Cl^0_\mathcal {A}(Y)=Y$;

• $Cl^{\alpha +1}_\mathcal {A}(Y)=Cl^\alpha _\mathcal {A}(Y)\cup \{a (x): a \in \mathcal {A} \ \& \, x \in Cl^\alpha _\mathcal {A}(Y)\}$;

• $Cl^\lambda _\mathcal {A}(Y)=\displaystyle \bigcup _{\alpha <\lambda } Cl^\alpha _\mathcal {A}(Y)$ for $\lambda \in Lim$.

$Cl_\mathcal {A}(Y) = Cl^\alpha _\mathcal {A}(Y)$ where $\alpha$ is any ordinal such that $Cl^\alpha _\mathcal {A}(Y)=Cl^{\alpha +1}_\mathcal {A}(Y)$.

For the remainder of the paper, unless stated otherwise, we will be working with a set of formulae $\varSigma$ such that . Observe that any finite set $\varSigma _0$ can be extended to a $\varSigma$ with this property that is finite up to modal equivalence of formulae since in $\textsf{S4}$ there are only finitely many non equivalent modalities and is an $\textsf{S4}$ modality [3].

Since we have labelled our variables by their binding formula, we can substitute this formula back and obtain a ‘closed’ version of this formula.

Lemma 2

Fix a finite set of formulas $\varSigma$ closed under $sub^*$ and some $\varphi \in \varSigma$, we let $\lfloor \varphi \rfloor$ denote the closed form of $\varphi$; that is every instance of $x_\psi$ is substituted by $\psi$ recursively until there are no free variables left.

It holds that $\lfloor \varphi \rfloor \in \mathcal {L}_\mu$ for each $\varphi \in \varSigma$.

Observe that additionally $\lnot \lfloor \varphi \rfloor$ is equivalent to $\lfloor \lnot \varphi \rfloor$ for all $\varphi \in \varSigma$. In the sequel, given a model M and a set of formulae $\varSigma$ closed under $sub^*$, we will read $w \vDash _M \varphi$ to mean $w \vDash _M \lfloor \varphi \rfloor$. In particular, this means that w is final for $\varphi$ in M iff it is final for $\lfloor \varphi \rfloor$ in M.

Definition 7

Fix a finite rooted model (M, w) and a set of formulas $\varSigma$, we will write

$$\begin{aligned} w \vDash _M \overline{\langle n \rangle } \varphi :\Leftrightarrow \exists v \in M^{\varSigma } \, ( v \sqsupseteq w \wedge dpt_{\varSigma }(v)=n \wedge \,v\vDash _M \varphi ). \end{aligned}$$

Since for a given cluster C of M and $u,v \in C, \, u\vDash _M \overline{\langle n \rangle }\varphi \Leftrightarrow v \vDash _M \overline{\langle n \rangle }\varphi$, we will occasionally make an abuse of notation and write $C \vDash _M \overline{\langle n \rangle }\varphi$ to mean $\exists u \in C \, u \vDash _M \overline{\langle n \rangle }\varphi$.

The formulas $\overline{\langle n \rangle }\varphi$ provide all the information needed to evaluate truth on C:

Theorem 2

Let (M, w), (N, w) be finite rooted models with root clusters C and $C'$ respectively. Assume that $dpt_{\varSigma }^M(w) = dpt_{\varSigma }^N(w)$ and $\forall \varphi \in \varSigma$ $w\vDash _M \overline{\langle n \rangle } \varphi \Leftrightarrow w \vDash _N \overline{\langle n \rangle } \varphi$ for all $n < dpt_{\varSigma }^M(w)$, and

• if C is $\varSigma$-final then $C'=C$

• if C is not $\varSigma$-final then $C'\subseteq C$

then $\forall v \in C' \, \forall \varphi \in \varSigma \ v\vDash _M \varphi$ iff $v\vDash _N \varphi$.

As an immediate corollary, we get the following, where we write $M,u \equiv _{\varSigma }N,v$ to mean $\forall \varphi \in \varSigma$ $u \vDash _M \varphi \Leftrightarrow v\vDash _N \varphi$. In case $M=N$, we may abbreviate this by $u\equiv _{\varSigma }v$.

Theorem 3

Given a finite model M, a model N with $M \supseteq N \supseteq M^{\varSigma }$ and any $w \in N$, it holds that $M,w\equiv _{\varSigma } N,w$.

4 Structural Evaluation

The strategy we will follow to obtain an equivalence is to describe the parts of the world and the model that are relevant to Theorem 2. In particular we will define formulae in equivalent to the $\overline{\langle n \rangle }\varphi$ ‘formulae’, as well as a formula which approximates the statement “w is $\varSigma$-final”.

Theorem 2 tells us that we need very little information to evaluate truth of formulas on a given cluster, provided we have already evaluated them on clusters of lower depth. This information is recorded by (semi-)satisfaction pairs:

Definition 8

Given a model M say that $\langle C,\varTheta \rangle$ is a semi-satisfaction pair for M if $\exists w \in M$ such that $C = C_w$ and $\varTheta = \{ \overline{\langle m \rangle } \psi : w \vDash _M \overline{\langle m \rangle } \psi$ for $\psi \in \varSigma \wedge m<dpt_{\varSigma }(w) \}$. A pair $\langle C, \varTheta \rangle$ is called a semi-satisfaction pair if it is a semi-satisfaction pair for some finite pointed $\varSigma$-semifinal model. A satisfaction pair for M is a semi-satisfaction pair $\langle C,\varTheta \rangle$ such that C is $\varSigma$-final in M.

Given a semi-satisfaction pair $\langle C,\varTheta \rangle$ for some model M, we define³

$$\begin{aligned} \displaystyle \varTheta ^C := \{ \overline{\langle m \rangle } \psi : C \vDash _M \overline{\langle m \rangle } \psi \text { for } \psi \in \varSigma \wedge m\le dpt_{\varSigma }(C) \}. \end{aligned}$$

We extend the definition of $dpt_{\varSigma }$ by saying $dpt_{\varSigma }(\varTheta )= sup\{n: \overline{\langle n \rangle }\varphi \in \varTheta$ for some $\varphi \in \varSigma \}$. Let $Sat_n$ be the set of satisfaction pairs $\langle C , \varTheta \rangle$ such that $dpt_{\varSigma } (\varTheta ) = n$ and let $Sat^0_n, \, Sat^1_n$ be the first and second projections of $Sat_n$ respectively. Similarly, $Sat^*_n, Sat^{*0}_n, Sat^{*1}_n$ are the corresponding sets for semi-satisfaction pairs.

We will need to compare clusters and semi-satisfaction pairs. Roughly, indicates that C is a smaller cluster than $C'$ (up to bisimulation), and $\langle C , \varTheta \rangle \vartriangleleft \langle C' , \varTheta ' \rangle$ indicates that the two pairs vary only in their root cluster, where $C'$ is larger.

Let us make this precise. Fix $P\subseteq \mathbb {P}$ and clusters C and $C'$ from models $\mathcal {M}= \langle M, \sqsubset _\mathcal {M}, \Vert \cdot \Vert _\mathcal {M} \rangle$ and $\mathcal {N}=\langle N, \sqsubset _\mathcal {N}, \Vert \cdot \Vert _\mathcal {N} \rangle$ respectively, we write to mean that there is some $C'' \subseteq C'''$ such that $C' \rightleftharpoons _P C''$. Similarly is defined for when additionally $C \not \rightleftharpoons _P C'$. As with the bisimilarity notation, the P subscript is omitted in the sequel. Define $\vartriangleleft _n \, \subseteq Sat_n \times Sat_n$ by $\langle C' , \varTheta ' \rangle \vartriangleleft _n \langle C , \varTheta \rangle$ iff and $\varTheta ' = \varTheta$. Let $\trianglelefteq _n$ be the reflexive closure of $\vartriangleleft _n$. We will write $\vartriangleleft$, $\trianglelefteq$ instead of $\vartriangleleft _n$, $\trianglelefteq _n$ when n is clear.

Satisfaction pairs are sufficient to evaluate truth, but our definition of $\overline{\langle n \rangle }\varphi$ in tangle logic will be sensitive to depth (i.e., to n), and thus we need to control the $\varSigma$-depth of the model we are working in. This is achieved by considering chains of satisfaction pairs: if a chain of length n lies above a given world, that means that the depth of that world is at least n. Since the property ‘there is a chain of length n’ will be expressible in , this will allow us to have the desired control over depth.

To formally define chains, we need to consider root clusters glued to a model. Fix a finite model M and a cluster C with $M\cap C = \varnothing$, we denote by $\left[ \begin{array}{l}M \\ C\end{array}\right]$ the model N with domain $M\cup C$, accessibility relation $\sqsubset _N := {\sqsubset _M}\cup {\sqsubset _C} \cup {(C\times M)}$ and $\Vert \cdot \Vert _N := \Vert \cdot \Vert _M\cup \Vert \cdot \Vert _C$.

Lemma 3

For every $\varSigma$-final model M of depth n with a root cluster C, there is some chain $\mathcal {C}=\{ \langle C_i , \varTheta _i \rangle \}_{i\le n}$ such that

• 1. $C_n = C$

• 2. $\langle C_i, \varTheta _i \rangle$ is a satisfaction pair for M for each $i\le n$

• 3. $C_{i+1} \prec C_i$ for each $i <n$

• 4. For all $i<n$, if then $\varTheta _{i+1} \ne \varTheta _i ^{C_i}$.

We will call a chain as in Lemma 3 a witnessing chain of depth n; witnessing chains will be denoted as $\mathcal {C}$, $\mathcal {C'}$ or $\mathcal {C}_i$. Let $Chain_n$ be the set of witnessing chains of depth n. We extend $\vartriangleleft _n$ to $Chain_n \times Chain_n$ by setting $\mathcal {C}\vartriangleleft _n \mathcal {C}'$ iff the following hold:

• $\langle C_i, \varTheta _i\rangle = \langle C_i',\varTheta _i'\rangle$ for $i<n$

•  

• $\varTheta _n = \varTheta _n'$

and let $\trianglelefteq _n$ be its reflexive closure. We will identify $\vartriangleleft$ and $\trianglelefteq$ to be the appropriate $\vartriangleleft _n$ and $\trianglelefteq _n$ respectively. Finally, given n and a formula $\varphi \in \varSigma$, we write

$$\begin{aligned} supp(\overline{\langle n \rangle } \varphi )= \big \{ \mathcal {C} \in Chain_n : \exists (M,w) \text { finite pointed } \varSigma \text {-final model where } \\ w\vDash _M \varphi \wedge \, C_n=C_w \, \wedge \mathcal {C} \text { is a witnessing chain of depth } n \text { for } M \big \}. \end{aligned}$$

The definition of witnessing chains can be further expanded to semifinal models, however the analogue of Lemma 3 for semi-witnessing chains will not necessarily hold for any $\varSigma$-semifinal model as we cannot guarantee that we can always find a chain in that case for which condition 4 will hold for the root cluster. In this setting, we instead use a weaker notion.

Definition 9

Given a $\varSigma$-semifinal model M of depth n with root cluster C, a semi-witnessing chain for M of depth n (if it exists) is some chain $\mathcal {C}=\{ \langle C_i , \varTheta _i \rangle \}_{i\le n}$ such that

• 1. $C_{n} = C$

• 2. $\langle C_i, \varTheta _i \rangle$ is a semi-satisfaction pair for M for each $i\le n$

• 3. $C_{i+1} \prec C_i$ for each $i <n$

• 4. For all $i<n$, if then $\varTheta _{i+1} \ne \varTheta _i ^{C_i}$.

We will denote by $Chain_n^*$ the set of all semi-witnessing chains of depth n. For M an arbitrary finite model, a (semi-)witnessing chain on M of depth n will be a (semi-)witnessing chain on the $\varSigma$-(semi)final part of $w\uparrow ^*_M$ for some $w\in M$. Finally for $\mathcal {C} \in Chain^*_n$, let $dpt(\mathcal {C}):=n$ denote its depth.

Fig. 1.

On the left, a witnessing chain. On the right, a witnessing chain ensures that the $\varSigma$-depth of a point where $\langle n \rangle \varphi$ holds is at least n.

We can now define formulas equivalent to the “$\overline{\langle n \rangle } \varphi$” in the language of . This is done inductively by having the formula $\alpha$ express the existence of a witnessing chain $\mathcal {C}$ with a satisfaction pair $\langle C,\varTheta \rangle$ underneath it. Then the formulae $\beta$ and $\gamma$ ensure that the extension $\mathcal {C}^\frown \langle C,\varTheta \rangle$ is also a witnessing chain (i.e. the pair $\langle C,\varTheta \rangle$ is as high as it can possibly be while remaining below $\mathcal {C}$). At this point it is important to note that if we were to simply use satisfaction pairs, we would run the risk of having the $\varSigma$-depth of worlds satisfying $\langle n \rangle \varphi$ being smaller than n; with witnessing chains, we ensure that the depth does not collapse (Fig. 1).

Definition 10

Fix $w\in M$ and a set of formulae $\varSigma$ let $\tau _w := \bigwedge _{p \in P(w)} p \wedge \bigwedge _{p\not \in P(w)}\lnot p$, where $p\in \varSigma$. We will, as a convention, not include the model M and the set $\varSigma$ in the notation. Below we define the formulas , along with some auxiliary formulas and notation.

• $Ir(\mathcal {C}):= \langle C_{n},\varTheta _{n}\rangle \trianglelefteq \langle C_{n-1},\varTheta _{n-1}^{C_{n-1}}\rangle \wedge \exists w \in C_{n} \forall u \in C_{n} \cap w \uparrow \ P(w) \ne P(u)$ where $n=dpt(\mathcal {C})$

• $\displaystyle A(\varTheta ) := \bigwedge _{\overline{\langle m \rangle } \psi \in \varTheta } \langle m \rangle \psi \wedge \bigwedge _{\overline{\langle m \rangle } \psi \not \in \varTheta } \lnot \langle m \rangle \psi$

• $\displaystyle \tau _w ^\mathcal {C} := {\left\{ \begin{array}{ll} \tau _w \wedge A(\varTheta _{dpt(\mathcal {C})}) \wedge \Diamond \big ( \tau _w \wedge \delta (\mathcal {C}{\upharpoonright } dpt(\mathcal {C})) \big ) &{} \text { if } Ir(\mathcal {C})\\ \tau _w \wedge A(\varTheta _{dpt(\mathcal {C})}) \wedge \Diamond \delta (\mathcal {C}{\upharpoonright } dpt(\mathcal {C})) &{} \text { otherwise } \end{array}\right. }$

•  

• $\beta (\mathcal {C}) := \Box \big ( \displaystyle \bigvee _{\mathcal {C}' \vartriangleleft \mathcal {C}} \alpha (\mathcal {C}') \rightarrow \alpha (\mathcal {C}) \big )$

• $\gamma (\mathcal {C}) := \displaystyle \lnot \bigvee _{\mathcal {C}' \not \trianglelefteq \mathcal {C}} \alpha (\mathcal {C}')$

• $\delta (\mathcal {C}) := \alpha (\mathcal {C}) \wedge \beta (\mathcal {C}) \wedge \gamma (\mathcal {C})$

•  

Here, A describes the $\overline{\langle m\rangle }$-formulas in a given $\varTheta$, Ir tells us when a bottom-most cluster in a chain has an ‘irreflexive point’⁴ which we can use to be able to jump to cluster in the chain above it, $\tau ^\mathcal C_w$ describes the ‘local state’ at w, $\alpha$ ensures that the desired chain is present, and $\beta$ and $\gamma$ rule out any unwanted chains. By following step by step the definitions above, we can prove the following lemma:

Lemma 4

Fix a finite model M a set of formulas $\varSigma$ and $w \in M$, it holds that $w\vDash _M \langle n \rangle \varphi \Leftrightarrow w \vDash _M \overline{\langle n \rangle } \varphi$ for all $\varphi \in \varSigma$.

Corollary 1

Fix a finite model M, some $w \in M$ and $C\in Chain_n^* \setminus Chain_n$, then $w\vDash _M \alpha (\mathcal {C})$ iff $\mathcal {C}{\upharpoonright } n$ is a witnessing chain of depth n for M strictly above w (i.e. $w\prec C_{n-1}$) and there is some cluster $C = C_u$ for some $u\in M$ such that

• (a) $w \preceq C \prec C_{n-1}$

• (b)  

• (c) $C \vDash _M A(\varTheta _n)$

The formulas $\langle n \rangle \varphi$ thus defined are the central ingredient in proving our main result. The translation $\chi (\varphi )$ of $\varphi$ itself into requires a case distinction according to whether we are evaluating on a final world or not. Since a completely accurate definition of finality is impossible to obtain, even in $\mathcal {L}_\mu$, we will instead approximate one with the following. The formula split(n) roughly states that there are two incomparable final worlds of depth n above w, or there is a semi-witnessing chain of depth higher than n above w; in either case, w itself cannot be a final world of depth n.

Definition 11

We define formulas

Now, suppose we have access to the valuation at w, a chain $\mathcal C$ witnessing that w is $\varSigma$-final of depth n (with $\mathcal C=\varnothing$ if w is not $\varSigma$-final), as well as the set $\varTheta$ of formulas $\langle m\rangle \varphi$ with $m<n:= dpt_\varSigma (w)$ which are true on w. For such a tuple $(w,\mathcal C,\varTheta ,n)$, we define a formula $\chi _0(w,\mathcal {C},\varTheta ,n )$ stating the above-mentioned properties, depending on whether split(n) holds on w:

We are almost ready to define $\chi (w)$. To do so, we first define $eval(\varphi ,n)$ to be the set of all triples $\langle w, \mathcal {C}, \varTheta \rangle$ for which there exists a rooted $\varSigma$-semifinal model (M, w) such that

• 1. $w\in M$

• 2. $w\vDash _M \varphi$

• 3. $\varTheta = \{ \overline{\langle m \rangle }\psi : w\vDash _M \overline{\langle m \rangle }\psi \text { for } \psi \in \varSigma \wedge m < dpt_{\varSigma }(w)\}$

• 4. If $w \not \in M^{\varSigma }$ then $dpt_{\varSigma } (\varTheta )=n$ and $\mathcal {C} = \varnothing$

• 5. If $w \in M^{\varSigma }$ then $dpt_{\varSigma } (\varTheta )=n-1$ and $\mathcal {C}$ is a witnessing chain for M of depth n with $\langle C_w,\varTheta \rangle = \langle C_n,\varTheta _n\rangle$.

And let $eval(\varphi ) := \displaystyle \bigcup _n eval(\varphi ,n)$. Since w satisfies $\varphi$ if and only if we can find $\mathcal C$ and $\varTheta$ such that $\langle w, \mathcal {C}, \varTheta \rangle \in eval(\varphi )$, we may define the characteristic formula $\chi (\varphi )$ of $\varphi$ by

$$\begin{aligned} \chi (\varphi ) := \bigvee _{\langle w,\mathcal {C},\varTheta \rangle \in eval(\varphi )} \chi _0 \big (w,\mathcal {C},\varTheta , dpt_{\varSigma }(\varTheta )\big ). \end{aligned}$$

Theorem 4

Given a formula $\varphi$ and a finite rooted model (M, w), we have that $w \vDash _M \varphi \Leftrightarrow w \vDash _M \chi (\varphi )$.

In view of [2], this also applies to the class of topological spaces. Moreover, can be expressed by a first order formula in all path-finite weakly transitive frames, where path-finite means that the ordering $\prec$ and its inverse $\prec ^{-1}$ are well-founded. So we get a first order expressibility of $\mathcal {L}_\mu$ in frames analogous to the ones in [5]. Thus we obtain the following.

Theorem 5

  over the class of topological spaces and the class of weakly transitive frames, and so $\mathcal {L}_\mu \subset {\textsf{FOL}}{/}{\rightleftharpoons }$ over finite and path-finite weakly transitive frames.

In-fact, we fail to get a characterization theorem for the $\mu$ calculus over finite and path-finite weakly transitive frames. We show this via a bisimulation invariant formula of FOL whose modal class is not definable via a $\mathcal {L}_\mu$ formula.

Theorem 6

$\mathcal {L}_\mu \subsetneq {\textsf{FOL}}{/}{\rightleftharpoons }$ over finite and path-finite weakly transitive frames.

We can obtain a rough estimate of $|\chi (\varphi )| \le 2^{(14|\varphi |+1)2^{14|\varphi |+6}}$. This upper bound also applies in the transitive setting, whereas it is more difficult to extract from the methods of [5]. This bound is reasonably close to the known lower bound, which is exponential [8]. Finding the optimal size of a translation remains an interesting open problem.

5 Conclusion

We have shown that the topological $\mu$-calculus is equi-expressive to its tangled fragment, provided it’s defined in a way that better captures its intended behaviour on arbitrary topological spaces while retaining its original value on metric spaces and other ‘nice’ topological spaces. Given the much more transparent syntax of tangle logic, this suggests that the latter is more suitable for applications in spatial KR than the full $\mu$-calculus.

This begs the question of whether the topological $\mu$-calculus, or its tangled fragment, can be enriched in a natural way to obtain the full expressive power of the bisimulation-invariant fragments of $\textsf{FOL}$ or $\textsf{MSO}$. Perhaps something in the spirit of hybrid logics can bridge this gap, but at this point the question remains a challenging open problem.