Modal Separability of Fixpoint Formulae

Abstract

We study modal separability for fixpoint formulae: given two mutually exclusive fixpoint formulae $\varphi,\varphi^{\prime}$, decide whether there is a modal formula $\psi$ that separates them, that is, that satisfies $\varphi\models\psi\models\neg\varphi^{\prime}$. This problem has applications for finding simple reasons for inconsistency. Our main contributions are tight complexity bounds for deciding modal separability and optimal ways to compute a separator if it exists. More precisely, it is ExpTime-complete in general and PSpace-complete over words. Separators can be computed in doubly exponential time in general and in exponential time over words, and this is optimal as well. The results for general structures transfer to arbitrary, finitely branching, and finite trees. The word case results hold for finite, infinite, and arbitrary words.

1 Introduction

For given logics $\mathcal{L},\mathcal{L}^{+}$, the $\mathcal{L}$-separability problem for $\mathcal{L}^{+}$ is to decide given two $\mathcal{L}^{+}$-formulae $\varphi,\varphi^{\prime}$ whether there is an $\mathcal{L}$-formula $\psi$ that separates $\varphi$ and $\varphi^{\prime}$ in the sense that $\varphi\models\psi$ and $\psi\models\neg\varphi^{\prime}$. Obviously, a separator can only exist when $\varphi$ and $\varphi^{\prime}$ are mutually exclusive, and the problem is only meaningful when $\mathcal{L}$ is less expressive than $\mathcal{L}^{+}$. Intuitively, a separator formulated in a “simpler” logic $\mathcal{L}$ explains a given inconsistency in a “complicated” logic $\mathcal{L}^{+}$. Note that, for logics $\mathcal{L}^{+}$ closed under negation, $\mathcal{L}$-separability generalizes the $\mathcal{L}$-definability problem for $\mathcal{L}^{+}$: decide whether a given $\mathcal{L}^{+}$-formula is equivalent to an $\mathcal{L}$-formula. Indeed, $\varphi\in\mathcal{L}^{+}$ is equivalent to an $\mathcal{L}$-formula iff $\varphi$ and $\neg\varphi$ are $\mathcal{L}$-separable. Since separability is more general than definability, solving it requires an even better understanding of the expressive power of the logics under consideration.

Example 1.

Consider $\mathcal{L}$ being the modal logic $\mathsf{ML}$, also known under the name ${\cal ALC}$ in the context of description logics. Expressions of the logic (called formulae in $\mathsf{ML}$ terminology and concepts in description logic parlance) describe properties of colored, directed graphs with a distinguished point called the root. As the more expressive $\mathcal{L}^{+}$ take $\mathsf{PDL}$: the extension of $\mathsf{ML}$ with regular modalities (in DL terms: the extension ${\cal ALC}_{\textit{reg}}$ of ${\cal ALC}$ with regular role expressions). Assume the graphs under consideration have edges labelled with colors $A$, $B$ and $C$ and consider properties:

• “There is a path from the root whose labeling belongs to $A^{+}B$.”

• “The labeling of every (finite) path from the root belongs to $C^{*}$.”

These (contradictory) properties are expressed by $\mathsf{PDL}$-formulae $\varphi$ and $\varphi^{\prime}$ and it is easy to see that none of them can be expressed in the weaker $\mathsf{ML}$. Nonetheless, $\varphi$ and $\varphi^{\prime}$ are separated by a simple $\mathsf{ML}$-formula $\psi$ that says: “there is an $A$-labelled edge from the root”. Thus, $\psi$ serves as an easy explanation of the inconsistency of $\varphi$ and $\varphi^{\prime}$.

Generalizing the example, in this paper we investigate $\mathsf{ML}$-separability of formulae in the modal $\mu$-calculus $\mu\mathsf{ML}$ [19, 11], which extends $\mathsf{PDL}$ [6]. $\mu\mathsf{ML}$ is a general framework capturing logics supporting fixpoints that is relevant both for knowledge representation and reasoning and for verification. It describes all bisimulation-invariant properties definable in ${\sf MSO}$ [8, Theorem 11] and thus encompasses virtually all specification languages such as $\mathsf{LTL}$ and $\mathsf{CTL}$ [2].

Our results generalize the $\mathsf{ML}$-definability problem for $\mu\mathsf{ML}$ which was shown decidable by Otto [16, Main Theorem]. The adaptation of the argument to the more general separability is relatively easy. However, Otto’s paper is focussed on deciding the existence of modal definitions. The problem of computing a definition when it exists is not discussed, and it seems that the formula which can be read off from the proof is at least tower-exponential big. This issue was addressed in [13]. Unfortunately, in this case the approach, although constructive, does not easily generalize from definability to separability. Matching lower bounds are also missing. We fill the gap by providing a procedure which is both fully constructive and works for the more general separation case. Both the constructed formulae and the running time are optimal, as illustrated by suitable examples and reductions.

We consider both general models and “word models” which are Kripke structures in which each point has at most one successor. The latter are relevant from a verification perspective and for temporal reasoning. In order to obtain our results we first prove model-theoretic characterizations in terms of bisimulations. We then exploit the close connection of $\mu\mathsf{ML}$ to nondeterministic parity tree automata to give (1) optimal procedures for the separability problem and (2) upper bounds on the modal depth of a separator, if it exists. In (1) we show ExpTime-completeness of modal separability in general and PSpace-completeness over words. The lower bounds are essentially inherited from satisfiability. The upper bounds derived in (2) are then used together with the automata to compute so-called $n$-uniform consequences, that is, modal formulae that have exactly the same modal consequences as a given $\mu\mathsf{ML}$-formula, up to modal depth $n$. These $n$-uniform consequences are then used as separators. Also here, our procedures are optimal: they compute separators of at most double exponential size, and we show that there are $\mu\mathsf{ML}$-formulae that are expressible in $\mathsf{ML}$ but any equivalent $\mathsf{ML}$-formulae must have doubly exponential size. This means that there is a double exponential succinctness gap between $\mu\mathsf{ML}$ and $\mathsf{ML}$. In the word case, our procedures compute exponentially sized separators and there is only an exponential succinctness gap. All lower bounds (both computational and succinctness) already hold for $\mathsf{PDL}$ (${\cal ALC}_{\textit{reg}}$) in place of $\mu\mathsf{ML}$, and for definability in place of separability.

It is interesting to note that our results hold over classes of models definable by $\mu\mathsf{ML}$-formulae. This observation allows us to cover the more general notion of separation in presence of an ontology (i.e. a background theory imposing some conditions on models). As long as the ontology is expressible in $\mu\mathsf{ML}$, separability and computation of separators reduce to the ontology-free setting. Without much effort the same observation lets us transfer our results to finite words, infinite words, and finite trees.

Missing proofs can be found in the appendix.

Related Work.

Separability has been intensively studied in formal language theory. A seminal result in this area is that separability of regular word languages by a first-order language is decidable in ExpTime [17]. Since $\mu\mathsf{ML}$ over words defines precisely the regular languages and first-order logic captures $\mathsf{ML}$, this is particularly related to our results over words.

In logic, a recent work investigates the complexity of separating between formulae supporting counting quantifiers by formulae that do not support them [12]. The used techniques exploit compactness, which makes them inapplicable to our case and inherently non-constructive.

Another related problem is the question of interpolant existence. An interpolant of two $\mathcal{L}$-formulae $\varphi$ and $\varphi^{\prime}$ is an $\mathcal{L}$-formula $\psi$ with $\varphi\models\psi\models\varphi^{\prime}$ and such that the signature of $\psi$ is contained in the signatures of both $\varphi$ and $\varphi^{\prime}$. Thus, the problem resembles separability but the restriction on $\psi$ is in terms of the signature instead of in terms of the logic. Sometimes this question reduces to entailment, as many logics enjoy the Craig interpolation property: an interpolant of $\varphi$ and $\varphi^{\prime}$ exists whenever $\varphi\models\varphi^{\prime}$. Interpolant existence for logics that lack Craig interpolation has recently been studied in [10, 1]. The used tools, however, are similar in nature to the ones from [12] and therefore inapplicable to our problem.

Finally, a related problem is separability of data examples. There, the task is to separate sets of pointed structures instead of formulae (see [14, 9] and the references therein). Separability of data examples can be cast as an instance of (our logical notion of) separability if $\mathcal{L}^{+}$ is expressive enough to describe the data examples. Conversely, $\mathcal{L}$-separability of formulae $\varphi$ and $\varphi^{\prime}$ is the same as data separability of the (possibly infinite) sets of their models by an $\mathcal{L}$-formula.

2 Preliminaries

Assuming familiarity of the reader with modal logic and the modal $\mu$-calculus, we recall here only the main notions and refer to [3] for more details.

Syntax.

We consider modal logic $\mathsf{ML}$ and its fixpoint extension $\mu\mathsf{ML}$ over a modal signature consisting of two finite sets: actions $\mathsf{Act}$ and propositions $\mathsf{Prop}$. The syntax of $\mathsf{ML}$ is given as:

$$\varphi::=\top\ |\ \bot\ |\ \tau\ |\ \neg\tau\ |\ \varphi\vee\varphi\ |\ \varphi\wedge\varphi\ |\ \langle\mathsf{a}\rangle\varphi\ |\ [\mathsf{a}]\varphi\$$

with $\tau\in\mathsf{Prop}$ and $\mathsf{a}\in\mathsf{Act}$. If $\mathsf{Act}=\{\mathsf{a}\}$ is a singleton, we use $\Diamond\varphi$ and $\Box\varphi$ in place of $\langle\mathsf{a}\rangle\varphi$ and $[\mathsf{a}]\varphi$. The syntax of $\mu\mathsf{ML}$ is obtained by extending the above with additional clauses:

$$\varphi::=x\ |\ \mu x.\varphi\ |\ \nu x.\varphi$$

where $x$ belongs to a fixed set $\mathsf{Var}$ of variables. The restriction to a fixed finite signature is only for the sake of readability. All results in the paper remain true with arbitrary signature.

Semantics.

The models we consider are pointed Kripke structures. That is, a model $\mathcal{M}$ consists of a set $M$ (called its universe) with a distinguished point $v_{I}\in M$ called the root, an interpretation ${\stackrel{{\scriptstyle\mathsf{a}}}{{\to}}}\subseteq M\times M$ for every $\mathsf{a}\in\mathsf{Act}$ and a valuation $\mathsf{val}:M\to\mathcal{P}(\mathsf{Prop})$. We call the set $\mathcal{P}(\mathsf{Prop})$ colors and denote it by $\Sigma$. Both $\mathsf{ML}$ and $\mu\mathsf{ML}$ are interpreted in points of models in a standard way. Since models are by definition pointed we write $\mathcal{M}\models\varphi$ meaning that the root of $\mathcal{M}$ satisfies $\varphi$. The same symbol denotes entailment: $\varphi\models\psi$ means that every model of $\varphi$ is a model of $\psi$. In the case only models from some fixed class $\mathcal{C}$ are considered we talk about satisfiability and entailment over $\mathcal{C}$ and in the latter case write $\varphi\models_{\mathcal{C}}\psi$.

A particularly relevant class of models are trees. A model $\mathcal{M}$ is a tree if the underlying directed graph $(M,\bigcup\{\stackrel{{\scriptstyle\mathsf{a}}}{{\to}}\ |\ \mathsf{a}\in\mathsf{Act}\})$ is a tree with $v_{I}$ as its root. The branching or outdegree of a point is the number of its children in this underlying graph. The class of all trees is denoted by $\mathsf{Trees}$. We identify words (both finite and infinite) over alphabet $\Sigma$ with trees over a single action of outdegree at most one. Points of such models are interpreted as positions in the word, the unique accessibility relation represents the successor relation, and the valuation determines the letter at each position. A prefix of a tree is a subset of its universe closed under taking ancestors. When no confusion arises we identify a prefix $N\subseteq M$ with the induced subtree $\mathcal{N}$ of $\mathcal{M}$ that has $N$ as its universe. The depth of a point is the distance from the root. The prefix of depth $n$ (or just $n$-prefix) is the set of all points at depth at most $n$ and is denoted by $M_{|_{n}}$ (and the corresponding subtree by $\mathcal{M}_{|_{n}}$).

We define bisimulations and bisimilarity in a standard way except that in the case of trees for convenience we assume that bisimulations only link points at the same depth. An $n$-step bisimulation (or just $n$-bisimulation) between trees $\mathcal{M}$ and $\mathcal{N}$ is a bisimulation between their $n$-prefixes. We denote $n$-bisimilarity by $\leftrightarroweq^{n}$.

Size of formulae.

The size of a formula $\varphi$, denoted $|\varphi|$, is the number of nodes in its syntax tree. Similarly, its depth is the maximal length of paths in the syntax tree. The depth of a formula should not be confused with its modal depth which is the maximal nesting of modal operators; all formulae of modal depth at most $n$ are denoted $\mathsf{ML}^{n}$.

When we specify formulae in the paper, we use syntactic sugar $\bigvee\Phi$, $\bigwedge\Phi$, and nabla $\nabla\Phi$, for finite sets of formulae $\Phi$. The first two are self-explanatory and allow for higher branching in the syntax tree. The last one, $\nabla\Phi$, intuitively means that “every formula in $\Phi$ is true in some child and every child satisfies some formula from $\Phi$” and is an abbreviation for

$$\textstyle\nabla\Phi=\bigwedge_{\varphi\in\Phi}\Diamond\varphi\wedge\Box\bigvee_{\varphi\in\Phi}\varphi.$$ (1)

It is well-known that $\bigvee\Phi$ and $\bigwedge\Phi$ can be rewritten into basic syntax under polynomial cost. We also include the colors $\Sigma$ directly in the syntax: $c\in\Sigma$ is a shorthand for the formula $\bigwedge\{\tau,\neg\tau^{\prime}\ |\ \tau\in c,\tau^{\prime}\notin c\}$. Rewriting colors increases the size only by a factor linear in $|\mathsf{Prop}|$.

Automata.

Throughout the paper we use automata over tree models of both bounded and arbitrary outdegree. A nondeterministic parity tree automaton (NPTA) is a tuple $\mathcal{A}=(Q,\Sigma,q_{I},\delta,\mathsf{rank})$ where $Q$ is a finite set of states, $q_{I}\in Q$ is the initial state, $\Sigma$ is the alphabet fixed above, and $\mathsf{rank}$ assigns each state a priority. The transition function $\delta$ is of type:

$$\delta:Q\times\Sigma\to\mathcal{P}(\mathcal{P}(Q)).$$

Intuitively, $\delta(q,c)=\{S_{1},...,S_{l}\}$ means that in the state $q$ upon reading color $c$ the automaton (i) chooses a transition $S_{i}$ and (ii) labels all the children of the current point with states from $S_{i}$ so that every $p\in S_{i}$ is assigned to some child. A run of $\mathcal{A}$ on a tree $\mathcal{M}$ is an assignment $\rho:M\to Q$ consistent with $\delta$ in such sense and sending the root of the tree to $q_{I}$. The run is accepting if for every infinite path $v_{0},v_{1}\ldots$ in $\mathcal{M}$ the sequence $\mathsf{rank}(\rho(v_{0})),\mathsf{rank}(\rho(v_{1})),\ldots$ satisfies the parity condition. We write $\mathcal{M}\models\mathcal{A}$ in case $\mathcal{A}$ has an accepting run on $\mathcal{M}$. An automaton that is identical to $\mathcal{A}$ except that the original initial state is replaced with $q$ is denoted $\mathcal{A}[q_{I}\mapsfrom q]$. We refer with NPWA to an NPTA working over words.

In NPTAs over trees of bounded outdegree $k$ it might be more common to use a transition function of type $\delta:Q\times\Sigma\to\mathcal{P}(Q^{k})$, but the difference is not essential: our NPTAs can be represented in this way and conversely, all relevant constructions for such NPTAs can be adapted to our setting. Most importantly, we rely on the following classical result (see for example the discussion in [21] and the well-presented Dealternation Theorem 5.7 in [4]):

Theorem 1.

For every $\mu\mathsf{ML}$-formula $\varphi$, we can construct an equivalent NPTA $\mathcal{A}$, that is, $\mathcal{M}\models\varphi$ iff $\mathcal{M}\models\mathcal{A}$, for every tree $\mathcal{M}$, with number of states at most exponential in $|\varphi|$. If we consider models of bounded outdegree $k$ then $\mathcal{A}$ is computed in exponential time, otherwise in doubly exponential time.

3 Foundations of Separability

We start with recalling the notion of separability and discuss some of its basic properties.

Definition 1.

Given $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$, a modal separator of $\varphi,\varphi^{\prime}$ is $\psi\in\mathsf{ML}$ with $\varphi\models\psi$ and $\psi\models\neg\varphi^{\prime}$. It is a modal separator over a class $\mathcal{C}$ if $\varphi\models_{\mathcal{C}}\psi$ and $\psi\models_{\mathcal{C}}\neg\varphi^{\prime}$.

The notion induces the problem of modal separability: given two $\mu\mathsf{ML}$-formulae $\varphi,\varphi^{\prime}$, decide whether a modal separator exists. Clearly, $\mathsf{ML}$-definability of $\varphi$ or $\varphi^{\prime}$ is a sufficient condition for the existence of a modal separator between $\varphi,\varphi^{\prime}$. However, Example 1 shows that it is not a necessary one: neither $\varphi$ nor $\varphi^{\prime}$ are $\mathsf{ML}$-definable, yet a separator exists. We make some foundational observations.

Inspired by the notion of Craig interpolation, one could also consider the notion of a Craig modal separator, which is a modal separator $\psi$ of $\varphi,\varphi^{\prime}$ which only uses symbols occurring in both $\varphi$ and $\varphi^{\prime}$. However, based on the fact that $\mathsf{ML}$ enjoys Craig interpolation, we show in Theorem 2 (proof in Appendix A) that Craig modal separability and modal separability coincide. Since $\mathsf{ML}$ enjoys Craig interpolation over many classes of models [15, Theorem 1], Theorem 2 remains true over all classes of models considered below. We thus focus on modal separability.

Theorem 2.

$\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ admit a modal separator iff they admit a Craig modal separator.

Inspired by the notion of uniform interpolation [23, 5], it is natural to ask whether every $\varphi\in\mu\mathsf{ML}$ admits a uniform modal separator, that is, a formula $\psi\in\mathsf{ML}$ that is a modal separator of $\varphi,\varphi^{\prime}$ for every $\varphi^{\prime}\in\mu\mathsf{ML}$ with $\varphi\models\neg\varphi^{\prime}$. However, substituting $\neg\varphi$ for $\varphi^{\prime}$ we get that the uniform modal separator $\psi$ for $\varphi$ is actually equivalent to $\varphi$. Consequently, a $\mu\mathsf{ML}$-formula has a uniform modal separator iff it is modally definable. This is contrast with the fact that both $\mathsf{ML}$ [23] and $\mu\mathsf{ML}$ [5] enjoy uniform interpolation.

Since $\mu\mathsf{ML}$ has both the finite model property and the (finitely branching) tree model property, the notions of a modal separator over finite models, arbitrary tree models, and finitely branching tree models all coincide with modal separator (over arbitrary models). Unsurprisingly, this does not apply to the class of all finite trees.

Example 2.

Consider a $\mu\mathsf{ML}$-formula $\varphi_{\infty}=\nu x.\Diamond x$ expressing that there exists an infinite path originating in the root. It is satisfiable, but unsatisfiable over finite trees. Thus $\bot$ is an $\mathsf{ML}$-definition of $\varphi_{\infty}$ over finite trees, but $\varphi_{\infty}$ is not $\mathsf{ML}$-definable (over arbitrary models).

We deal with separability over finite trees as follows. Call a class $\mathcal{C}$ of models $\mu\mathsf{ML}$-definable in $\mathcal{D}$ if there is a $\mu\mathsf{ML}$-formula $\theta$ such that $\mathcal{M}\in\mathcal{C}$ iff $\mathcal{M}\models\theta$, for all models $\mathcal{M}\in\mathcal{D}$.

Lemma 1.

Let $\mathcal{C}$ be $\mu\mathsf{ML}$-definable in $\mathcal{D}$ by $\theta$ and let $\psi\in\mathsf{ML}$. Then $\psi$ is a modal separator of $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ over $\mathcal{C}$ iff $\psi$ is a modal separator of $\theta\wedge\varphi$ and $\theta\wedge\varphi^{\prime}$ over $\mathcal{D}$.

Intuitively, Lemma 1 provides us with a reduction of modal separability over $\mathcal{C}$ to modal separability over (the larger) $\mathcal{D}$. It has a number of interesting consequences. First, observe that the formula $\neg\varphi_{\infty}$ from Example 2 defines the class of finite trees in the class of all finitely branching trees. Hence $\neg\varphi_{\infty}$ provides a reduction of modal separability over finite trees to modal separability over finitely branching trees, and thus to modal separability. Similarly, and again using $\varphi_{\infty}$, Lemma 1 reduces modal separability over finite words and over infinite words to modal separability over (arbitrary) words. Finally, the lemma can be used to reduce modal separability relative to background knowledge to modal separability. Call $\psi$ a modal separator of $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ relative to $\theta_{0}\in\mu\mathsf{ML}$ if it is a modal separator of $\varphi,\varphi^{\prime}$ over the class of models satisfying $\theta_{0}$ in every point. This setting is most relevant for the DL community since $\theta_{0}$ plays the role of an ontology. In particular, the question whether two ${\cal ALC}_{\textit{reg}}$-concepts $\varphi,\varphi^{\prime}$ are separable by an ${\cal ALC}$-concept relative to an ${\cal ALC}_{\textit{reg}}$-ontology is an instance of that problem (recall that every ${\cal ALC}_{\textit{reg}}$-concept can be expressed as a $\mu\mathsf{ML}$-formula). Let $\theta$ be the $\mu\mathsf{ML}$-formula expressing that $\theta_{0}$ is satisfied in every point reachable via the accessibility relations. Using Lemma 1 and bisimulation invariance of $\mu\mathsf{ML}$, it is routine to verify that $\psi$ is a modal separator of $\varphi,\varphi^{\prime}$ relative to $\theta_{0}$ iff $\psi$ is a modal separator of $\theta\wedge\varphi$ and $\theta\wedge\varphi^{\prime}$.

In view of what was said so far, we will from now on concentrate on deciding modal separability over general and word models and computing separators if they exist. A main ingredient for both tasks is to show that if there is a modal separator for $\mu\mathsf{ML}$-formula $\varphi,\varphi^{\prime}$, then there is one of modal depth $n$ at most exponential in the size of $\varphi$ and $\varphi^{\prime}$. As a necessary tool for showing this exponential bound on $n$, and for efficiently deciding if a given $n$ suffices, in Appendix B we establish the following model-theoretic characterization. Fix $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ for the rest of the paper and denote their size by $k=|\varphi|+|\varphi^{\prime}|$.

Proposition 1.

Let $n\in\mathbb{N}$. The following are equivalent:

1. There is $\psi\in\mathsf{ML}$ of modal depth $n$ separating $\varphi$ and $\varphi^{\prime}$;

2. For all models $\mathcal{M}$ and $\mathcal{M}^{\prime}$ bisimilar up to depth $n$: $\mathcal{M}\models\varphi$ implies $\mathcal{M}^{\prime}\not\models\varphi^{\prime}$;

3. For all trees $\mathcal{M}$ and $\mathcal{M}^{\prime}$ identical up to depth $n$: $\mathcal{M}\models\varphi$ implies $\mathcal{M}^{\prime}\not\models\varphi^{\prime}$;

4. For all trees $\mathcal{M}$ and $\mathcal{M}^{\prime}$ identical up to depth $n$ and whose branching is bounded by $k$:
   $\mathcal{M}\models\varphi$ implies $\mathcal{M}^{\prime}\not\models\varphi^{\prime}$.

Based on Proposition 1, we show that $\mathsf{ML}$-separability of $\mu\mathsf{ML}$-formulae is ExpTime-complete and thus not harder than $\mathsf{ML}$-definability.

Theorem 3.

Modal separability of $\mu\mathsf{ML}$-formulae is ExpTime-complete over arbitrary models.

ExpTime-hardness already holds for $\mathsf{ML}$-definability and is proved by an immediate reduction from $\mu\mathsf{ML}$-satisfiability, which is ExpTime-complete already for its fragment $\mathsf{PDL}$ [6, Section 4]. It is not hard to modify the original hardness proof for $\mathsf{PDL}$-satisfiability to work over finite trees, so Theorem 3 remains valid over finite trees as well. For the upper bound, we mostly follow the technical development in [16]. Thanks to Proposition 1 separability is equivalent to the existence of $n\in\mathbb{N}$ for which condition (iv) holds. This can be expressed as an ${\sf MSO}$ statement about the full $k$-ary tree, and thus decided. However, for optimal complexity and to extract bounds that we use later, in Appendix C we apply a lower-level automata-theoretic analysis.

Over words, we essentially follow the same approach. Since the tree automata used in the proof of Theorem 3 can be replaced by word automata, the complexity drops to PSpace (see Appendix D). A matching lower bound can be derived as above by a reduction from satisfiability in $\mathsf{LTL}$ over words [20, Theorem 4.1] (which, in fact, can be rephrased in terms of $\mathsf{PDL}$).

Theorem 4.

Modal separability of $\mu\mathsf{ML}$-formulae is PSpace-complete over words.

As announced, an important step in the proofs of the upper bounds, both in the case with arbitrary models and with words, is the following proposition which we will also use later.

Proposition 2.

If $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ are separable then they are separable by a formula of modal depth $l$ exponential in their size $k$. The same is true over words.

In the remainder of the paper we will deal with computing separators based on Proposition 2. Before we proceed let note that our approach differs from the treatment of modal definability from [13]. There, the authors rewrite given $\varphi$ into modal $\psi$ in such a way that if the initial $\varphi$ is modally definable then $\varphi$ and $\psi$ are equivalent. In the case when $\varphi$ is not modally definable, however, the output $\psi$ is rather random. For example, $\psi$ obtained from the formula $\varphi_{\infty}$ from Example 2 is equivalent to $\bot$ which is not even a consequence of $\varphi_{\infty}$. Thus, a different construction is needed to obtain separators. We will actually compute something slightly stronger that might be of independent interest.

Definition 2.

Given $\varphi\in\mu\mathsf{ML}$ and $n\in\mathbb{N}$, a formula $\psi\in\mathsf{ML}^{n}$ is an $n$-uniform consequence of $\varphi$ if, for all $\theta\in\mathsf{ML}^{n}$:

$$\varphi\models\theta\hskip 14.22636pt\iff\hskip 14.22636pt\psi\models\theta$$

An analogous notion relative to a fixed class $\mathcal{C}$ of models is obtained by replacing $\models$ with $\models_{\mathcal{C}}$.

In words: $\psi$ is an $n$-uniform consequence of $\varphi$ if it has modal depth $n$, is a consequence of $\varphi$, and entails every other consequence of $\varphi$ of modal depth $n$. In particular, if $\varphi$ and $\varphi^{\prime}$ are separable by some modal formula of modal depth $n$ and $\psi$ is an $n$-uniform consequence of $\varphi$, then this $\psi$ separates $\varphi$ from $\varphi^{\prime}$ as well. Observe that $n$-uniform consequences exist for every $\varphi\in\mu\mathsf{ML}$ and $n\in\mathbb{N}$. Indeed, given $\varphi$ and $n$ we can obtain an $n$-uniform consequence $\psi$ of $\varphi$ by taking the disjunction of all $\mathsf{ML}^{n}$-types consistent with $\varphi$. Here, by an $\mathsf{ML}^{n}$-type we mean a maximal consistent subset of $\mathsf{ML}^{n}$. Since up to equivalence there are only finitely many formulae in $\mathsf{ML}^{n}$, each $\mathsf{ML}^{n}$-type can be represented as a single $\mathsf{ML}^{n}$-formula and the mentioned disjunction $\psi$ is well-defined.

In view of Proposition 2, it thus suffices to compute $n$-uniform consequences of $\varphi$. Unfortunately, the naive construction given above is nonelementary in the size of the separated formulae $\varphi$ and $\varphi^{\prime}$. In the next sections we give better constructions.

4 Optimal Separators: Arbitrary Models

We construct doubly exponentially sized separators and provide matching lower bounds.

4.1 Construction

Theorem 5.

If $\varphi$ and $\varphi^{\prime}$ are modally separable then a separator $\varphi$ of size doubly exponential in $k=|\varphi|+|\varphi^{\prime}|$ exists and can be computed in doubly exponential time.

The above is a consequence of the following lemma.

Lemma 2.

For every $\varphi\in\mu\mathsf{ML}$ and $n\in\mathbb{N}$, one can construct an $n$-uniform consequence $\psi_{n}\in\mathsf{ML}^{n}$ of $\varphi$ with branching doubly exponential in $|\varphi|$ and depth linear in $n$.

We show how Theorem 5 follows from Lemma 2. Proposition 2 guarantees that if a modal separator for $\varphi$ and $\varphi^{\prime}$ exists then there is one with modal depth $l$ exponential in $k$. Since $\psi_{l}$ entails this separator it follows that $\psi_{l}$ is a separator itself.

The branching $m$ of $\psi_{l}$ is at most doubly exponential in $|\varphi|$ and thus also in $k$: $m\leq 2^{2^{k^{x}}}$ for some constant $x$. The depth $d$ of $\psi_{l}$ is linear in $l$ and therefore $d\leq 2^{k^{y}}$ for some $y$. Altogether this means that the size of $\psi_{l}$:

$$|\psi_{l}|\leq m^{d}\leq(2^{2^{k^{x}}})^{2^{k^{y}}}$$

is at most doubly exponential in $k$. It remains to prove Lemma 2.

Proof.

Let $\mathcal{A}=(Q,\Sigma,q_{I},\delta,\mathsf{rank})$ be the NPTA equivalent to $\varphi$ with exponentially many states, which exists due to Theorem 1. For each $n\in\mathbb{N}$ and $q\in Q$ we construct $\psi_{n,q}\in\mathsf{ML}^{n}$ of branching $2^{2^{|Q|}}$ such that:

$$\mathcal{M}\models\psi_{n,q}\text{\hskip 14.22636pt $\iff$ \hskip 14.22636pt there exists $\mathcal{N}\models\mathcal{A}[q_{I}\mapsfrom q]$ with $\mathcal{M}\leftrightarroweq^{n}\mathcal{N}$}$$ (2)

for every structure $\mathcal{M}$. Then, $\psi_{n,q_{I}}$ is our desired $n$-uniform consequence $\psi_{n}$ of $\varphi$.

We proceed by induction on $n\in\mathbb{N}$. For the base case we put:

$$\psi_{0,q}=\bigvee\{c\in\Sigma\ |\ \text{there is $\mathcal{N}\models\mathcal{A}[q_{I}\mapsfrom q]$ with $\mathcal{N}\models c$}\}$$

which clearly satisfies the induction goal (2). For the induction step define:

$$\psi_{n+1,q}=\bigvee_{c\in\Sigma}\bigvee_{S\in\delta(q,c)}c\wedge\nabla\{\psi_{n,p}\ |\ p\in S\}.$$

Fix $\mathcal{M}$, denote the color of the root by $c$ and the set of all children of the root by $M_{0}$. If $\mathcal{M}$ satisfies $\psi_{n+1,q}$ then there is $\{p_{1},...,p_{l}\}=S\in\delta(q,c)$ such that nabla of $\Phi=\{\psi_{n,p}\ |\ p\in S\}$ is satisfied in the root. By invariance under bisimulation we may assume that the root of $\mathcal{M}$ has sufficiently many children to find a separate witness for each $\psi_{n,p}\in\Phi$. That is, we assume a surjective assignment $h:M_{0}\to\Phi$ that maps every $v\in M_{0}$ to some formula $\psi_{n,p}$ true in $v$. By induction hypothesis, for each $v\in M_{0}$ with $h(v)=\psi_{n,p}$ there is a model $\mathcal{N}_{p}\models\mathcal{A}[q_{I}\mapsfrom p]$ $n$-bisimilar to the subtree of $\mathcal{M}$ rooted in $v$. Define $\mathcal{N}$ as follows: first take the disjoint union $\{v\}\sqcup\mathop{\mathop{\mbox{\bigmathxx\char 116\relax}}}\limits\{\mathcal{N}_{p}\ |\ p\in S\}$ of all the $\mathcal{N}_{p}$’s and a fresh point $v$ of color $c$; then for every $\mathcal{N}_{p}$ add an edge from $v$ to the root of $\mathcal{N}_{p}$ and set $v$ as the new root. It is easy to see that $\mathcal{N}\models\mathcal{A}[q_{I}\mapsfrom q]$ and $\mathcal{M}\leftrightarroweq^{n+1}\mathcal{N}$, as desired.

Conversely, assume $\mathcal{M}\leftrightarroweq^{n+1}\mathcal{N}$ and $\mathcal{N}\models\mathcal{A}[q_{I}\mapsfrom q]$ witnessed by an $(n+1)$-bisimulation $Z$ and a run $\rho:N\to Q$. Denote the children of the root of $\mathcal{N}$ by $N_{0}$. Since $\rho$ is a run, the set $S=\rho[N_{0}]$ of states assigned to $N_{0}$ belongs to $\delta(q,c)$. Every $v\in M_{0}$ is $n$-bisimilar to some $w\in N_{0}$ and hence by the induction hypothesis satisfies $\psi_{n,p}$ for $p=\rho(w)\in S$. Symmetrically, for every $p\in S$ there is $w\in N_{0}$ accepted by $\mathcal{A}[q_{I}\mapsfrom p]$. Since that $w$ is $n$-bisimilar to some $v\in M_{0}$, by induction hypothesis $v$ satisfies $\psi_{n,p}$. It follows that the root of $\mathcal{M}$ satisfies $\nabla\{\psi_{n,p}\ |\ p\in S\}$ and therefore also $\psi_{n+1,q}$. ∎

Let us remark that Lemma 2 can be easily adapted to deal with vocabulary restrictions. That is, given $P\subseteq\mathsf{Prop}$ we could construct $\psi_{n}^{P}$ similar to $\psi_{n}$ but only using atomic propositions from $P$ and only entailing $\mathsf{ML}^{n}$-consequences of $\varphi$ whose vocabulary is contained in $P$. To that end, it suffices to project-out atomic propositions not in $P$ from the automaton $\mathcal{A}$ and only then proceed with our construction. The automaton $\mathcal{A}^{P}$ obtained by such a projection accepts a model $\mathcal{M}$ iff $\mathcal{M}$ is $P$-bisimilar to some $\mathcal{N}\models\mathcal{A}$. It follows that for every $\theta\in\mathsf{ML}^{n,P}$:

$$\psi_{n}^{P}\models\theta\hskip 14.22636pt\iff\hskip 14.22636pt\mathcal{A}^{P}\models\theta\hskip 14.22636pt\iff\hskip 14.22636pt\mathcal{A}\models\theta$$

where the first equivalence uses $\theta\in\mathsf{ML}^{n}$ and the latter $\theta\in\mathsf{ML}^{P}$. Such $(P,n)$-uniform consequence $\psi_{n}^{P}$ of $\varphi$ can then be taken as a Craig modal separator, in the same way as $\psi_{n}$ serves as a modal separator.

4.2 Lower bounds

For the lower bounds, we show that over arbitrary structures (in fact, already binary trees) $\mu\mathsf{ML}$ is doubly exponentially more succinct than $\mathsf{ML}$. The example is essentially taken from [7, Section 3.1]. There the authors use game-theoretic tools which are later applied to more complicated cases. Since we are only interested in this example, we provide a straightforward self-contained argument.

Proposition 3.

There is a sequence $(\varphi_{n})_{n\in\mathbb{N}}$ of $\mu\mathsf{ML}$-formulae of size polynomial in $n$ such that each $\varphi_{n}$ is equivalent to a $\mathsf{ML}$-formula but every $\psi\in\mathsf{ML}$ equivalent to $\varphi_{n}$ has size at least $2^{2^{n}}$.

Proof.

We only give a sketch, the details are found in Appendix E. We assume two different actions $\mathsf{a}$ and $\mathsf{b}$. For each $n\in\mathbb{N}$ consider the property:

• “No path (over all actions) longer than $2^{n}$ starts in the root.”

This can be enforced by encoding an $n$-bit binary counter into the structure of the model, and requiring that on every path the counter values are strictly increasing. Let $C_{n}$ be this (technically stronger) property expressing the behavior of the encoded counter. Assuming that the encoding is reasonably efficient, $C_{n}$ can be easily expressed by a $\mu\mathsf{ML}$-formula $\varphi_{n}$ of size polynomial in $n$ (in fact, a weak fragment of $\mathsf{PDL}$ is already sufficient). Since the lengths of paths are bounded, $C_{n}$ can be also expressed in $\mathsf{ML}$.

However, every $\psi\in\mathsf{ML}$ equivalent to $\varphi_{n}$ has size at least $2^{2^{n}}$. The reason is that for every sequence of actions $\mathsf{a}$ and $\mathsf{b}$ of length $2^{n}$, the syntax tree of $\psi$ must contain a descending sequence of subformulae of length $2^{n}$ such that the $i$-th subformula begins with a modal operator corresponding to the $i$-th action. This allows to embed a binary tree of height $2^{n}$ into the syntax tree of $\psi$. ∎

Note that the presence of two different actions $\mathsf{a}$ and $\mathsf{b}$ is essential for the argument. We conjecture that $\mu\mathsf{ML}$ is doubly exponentially more succinct than $\mathsf{ML}$ already in the monomodal setting. Consider the following Property $P_{n}$, parameterized by $n\in\mathbb{N}$:

• “$C_{n}$ and there exists a maximal path on which the number of points satisfying $\tau$ is even.”

where $C_{n}$ is the same as in Proposition 3. It is not difficult to come up with small, that is, of size polynomial in $n$, $\mu\mathsf{ML}$-formulae $\varphi^{\prime}_{n}$ expressing $P_{n}$. Unfortunately, proving that no small $\mathsf{ML}$ formula can be equivalent to $\varphi_{n}^{\prime}$ seems difficult. For instance, consider models where every non-leaf point has a child satisfying $\tau$ and a child satisfying $\neg\tau$. Then a trick similar to the famous example of Potthoff (showing, roughly, that the language of all binary trees of even depth is first-order definable) [18, Example 1] can be exploited to get a modal formula equivalent to $\varphi_{n}^{\prime}$ (over such models), but of size only single exponential in $n$. Moreover, the results in the next Section 5 show that looking at words only is not sufficient either.

5 Optimal Separators: Word Case

In this section we show that optimal modal separators (over words) can be computed exponentially faster and are exponentially smaller compared to the case with arbitrary models.

Theorem 6.

If $\varphi$ and $\varphi^{\prime}$ are modally separable over words, then a separator of size exponential in $|\varphi|+|\varphi^{\prime}|$ exists and can be computed in exponential time.

As with arbitrary models, Proposition 2 gives an upper bound on the modal depth of a separator and so it suffices to construct $n$-uniform consequences of $\varphi$ of small size.

We illustrate the idea first. Consider the classes EVEN_n and ODD_n, $n\in\mathbb{N}$ of all word structures of length $n$ in which proposition $a$ is satisfied in an even and odd, respectively, number of points. Constructing modal formulae $\varphi_{n}$ and $\varphi^{\prime}_{n}$ defining EVEN_n and ODD_n in the following, naive way leads to exponential formulae since $\varphi_{i+1}$ contains both and $\varphi_{i}$ and $\varphi^{\prime}_{i}$:

$$\varphi_{0} =\neg a\wedge\Box\bot \varphi_{i+1} =\Diamond\top\wedge\big{(}(a\wedge\varphi_{i}^{\prime})\vee(\neg a\wedge\varphi_{i})\big{)}$$

$$\varphi_{0}^{\prime} =a\wedge\Box\bot \varphi_{i+1}^{\prime} =\Diamond\top\wedge\big{(}(a\wedge\varphi_{i})\vee(\neg a\wedge\varphi_{i}^{\prime})\big{)}$$

This exponential blow-up can be avoided, however, using “divide-and-conquer” as follows:

$$\varphi_{2n}=\big{(}\varphi_{n}\wedge\Diamond^{n}\varphi_{n}\big{)}\vee\big{(}\varphi_{n}^{\prime}\wedge\Diamond^{n}\varphi_{n}^{\prime}\big{)}$$

$$\varphi_{2n}^{\prime}=\big{(}\varphi_{n}\wedge\Diamond^{n}\varphi_{n}^{\prime}\big{)}\vee\big{(}\varphi_{n}^{\prime}\wedge\Diamond^{n}\varphi_{n}\big{)}$$

Although several copies of formulae of smaller index are used as well, but since the index is halved, we end up with formulae of roughly quadradic size. The proof of the following analogue of Lemma 2 relies on this idea.

Lemma 3.

For every $n\in\mathbb{N}$ and every NPWA $\mathcal{A}$ with states $Q$, one can construct a formula $\psi_{n}\in\mathsf{ML}^{n}$ which is $\mathcal{A}$’s $n$-uniform consequence over words and has size polynomial in $n$ and $|Q|$. The construction requires polynomial time.

To see that Lemma 3 implies Theorem 6, let $\varphi$ and $\varphi^{\prime}$ admit a modal separator over words. Let $\mathcal{A}$ be an NPWA that is equivalent to $\varphi$. By Theorem 1, $\mathcal{A}$ has exponentially many states and can be computed in exponential time. Proposition 2 implies that there is a modal separator of modal depth $l$ at most exponential in $k=|\varphi|+|\varphi^{\prime}|$. As with arbitrary models, $\mathcal{A}$’s $l$-uniform consequence $\psi_{l}$ from Lemma 3 is the sought separator. We now prove the lemma.

Proof.

Let $\mathcal{A}=(Q,\Sigma,\delta,q_{I},\mathsf{rank})$ be an NPWA. The main idea is to construct, for every $p,q\in Q$ and $m\in\mathbb{N}$, a formula $\psi_{p,q}^{m}$ such that for every input word $\mathcal{M}$:

$$\mathcal{M}\models\psi_{p,q}^{m}\iff\text{there is a run from $p$ to $q$ over the $m$-prefix of $\mathcal{M}$},$$

The key step is the recursive splitting similar to the definitions of EVEN_n and ODD_n above. Intuitively, $\psi_{p,q}^{2m}$ is the disjunction over all $s\in Q$ of the conditions “there is a run from $p$ in the initial position to $s$ in position $m$, and a run from $s$ in position $m$ to $q$ in position $2m$.” The latter conditions are recursively expressed using $\psi_{p,s}^{m}$ and $\psi_{s,q}^{m}$. The constructed formulas $\psi_{q_{I},q}^{m}$, $m\leq n$ are then used to describe all possible $n$-prefixes of models of $\mathcal{A}$. The details of the construction can be found in Appendix F. ∎

We conclude the section with the comment that Theorem 6 is optimal in the sense that there are modally separable formulae which require a large separator. We actually show the following stronger statement implying that, over words, $\mu\mathsf{ML}$ is exponentially more succinct than $\mathsf{ML}$.

Proposition 4.

There is a sequence of $\mu\mathsf{ML}$-formulae $(\varphi_{n})_{n\in\mathbb{N}}$ of size polynomial in $n$ such that each $\varphi_{n}$ is equivalent to a $\mathsf{ML}$-formula but every $\psi\in\mathsf{ML}$ equivalent to $\varphi_{n}$ has size at least $2^{n}$.

The proof is entirely standard. The main idea is that, already in $\mathsf{PDL}$ one can stipulate (with a small formula) a finite word of exponential length. Clearly, any $\mathsf{ML}$-formula expressing this requires exponential size. The only difficulty is doing it with a fixed signature: instead of encoding $i$-bit counters using $i$ propositions, we use just two propositions and encode numbers in $i$ consecutive points.

6 Conclusion and Open Problems

We have studied the problem of deciding separability of $\mu\mathsf{ML}$-formulae by fixpoint free formulae from $\mathsf{ML}$, and computing separators if they exist. Our results cover several interesting classes of models such as trees, finite trees, and words. Due to the great expressivity of $\mu\mathsf{ML}$ the results remain valid in the presence of ontologies.

A notably missing case is the class of trees of fixed outdegree $d$ independent from formulae. This is surprisingly different from the classes we studied. The key difficulty here lies in the fact that the implication (iii) $\Rightarrow$ (ii) from Proposition 1 is not true over such trees.

An intriguing challenge left for future study is to look at extensions of $\mu\mathsf{ML}$ and/or $\mathsf{ML}$. Natural extensions are inverse modalities, the universal modality, graded modalities, and constants (corresponding to inverse roles, the universal role, counting quantifiers, and nominals in DL speech). We expect the adaptation to inverse modalities to be only minor. Also graded modalities look innocent if they are allowed both in the larger logic and in the separator logic. If we only extend $\mu\mathsf{ML}$ with graded modalities and ask for separators in $\mathsf{ML}$ (without graded modailites), we would have to combine our techniques with the ones from [12], which is potentially challenging. We expect universal modality and/or constants to pose more technical difficulties as well. Intuitively, adding a universal modality or constants leads to the loss of the strong locality underlying Proposition 1.

Throughout the appendix we use the term tallness. The tallness of a tree is the distance from the root to the closest leaf (or $\infty$ if it the tree has no leafs).

Appendix A Separability Coincides with Craig Separability

We prove Theorem 2 which says that $\varphi,\varphi^{\prime}$ are modally separable iff they are Craig modally separable.

Proof.

Clearly, any Craig modal separator is also a modal separapator.

Conversely, suppose there is a modal separator $\psi$ of $\varphi,\varphi^{\prime}$, and let $n$ be its modal depth. We use the $n$-uniform consequences as defined in Definition 2. Let $\theta$ be the $n$-uniform consequence of $\varphi$ and $\theta^{\prime}$ the $n$-uniform consequence of $\varphi^{\prime}$ (both exist, see the discussion after Definition 2). Note that $\neg\theta^{\prime}\models\neg\varphi^{\prime}$. By definition of $n$-uniform consequence, we have $\theta\models\psi$ and $\psi\models\neg\theta^{\prime}$, and thus $\theta\models\theta^{\prime}$. Since $\mathsf{ML}$ enjoys Craig interpolation, there is an interpolant $\psi^{\prime}$ for $\theta,\theta^{\prime}$ which is also a Craig modal separator of $\varphi,\varphi^{\prime}$. ∎

Appendix B Model-theoretic Characterization

We prove Proposition 1.

The implication (i) $\Rightarrow$ (iv) is straightforward. Separator $\psi\in\mathsf{ML}^{n}$ cannot distinguish models identical up to depth $n$. If $\mathcal{M}\models\varphi$ then $\mathcal{M}\models\psi$ and so $\mathcal{M}^{\prime}\models\psi$ which in turn implies $\mathcal{M}^{\prime}\models\neg\varphi^{\prime}$.

Our argument for (iv)$\implies$(iii) uses a classical characterization of the semantics of $\mu\mathsf{ML}$ formulae in terms of parity games. Since we do not want to introduce games we only sketch the (easy) construction; the necessary definitions can be found in [22].

We prove the implication by contrapositive. Assume $\mathcal{M}\models\varphi$ and $\mathcal{M}^{\prime}\models\varphi^{\prime}$ identical up to depth $n$. The fact that $\mathcal{M}\models\varphi$ is equivalent to existence of a winning strategy in an appropriately defined parity game $\mathcal{G}_{\varphi}$. Positions of the game are pairs: $(v,\theta)$ with $v\in M$ and $\theta$ subformula of $\varphi$ and a move from $(v,\theta)$ to $(v^{\prime},\theta^{\prime})$ is only allowed if $v\stackrel{{\scriptstyle}}{{\to}}v^{\prime}$. A similar game $\mathcal{G}_{\varphi^{\prime}}$ captures the semantics of $\varphi^{\prime}$.

Take positional winning strategies $\sigma$ and $\sigma^{\prime}$ for $\exists\text{ve}$ in the games $\mathcal{G}_{\varphi}$ and $\mathcal{G}_{\varphi^{\prime}}$. We trim $\mathcal{M}$: only keep the points that belong to a position chosen by $\exists\text{ve}$ in either a $\sigma$- or $\sigma^{\prime}$-play, and remove all the other ones. After that, also remove points that become inaccessible from the root so that the resulting structure is a tree. The tree $\mathcal{N}$ obtained this way still satisfies $\varphi$ because the strategy $\sigma$ remains winning. For every $v\in M$ both games together only have $k$ positions containing $v$. Thus, by positionality, among the children of $v$ only at most $k$ many belong to a position chosen by $\sigma$ or $\sigma^{\prime}$. Since only such points belong to $N$, it follows that $\mathcal{N}$ has branching at most $s$. We trim $\mathcal{M}^{\prime}$ to $\mathcal{N}^{\prime}\models\varphi^{\prime}$ in the same way. By construction $\mathcal{N}$ and $\mathcal{N}^{\prime}$ are identical up to depth $n$ which violates (iv).

To prove (iii) $\Rightarrow$ (ii) assume towards contradiction that there are models $\mathcal{M}\models\varphi$ and $\mathcal{M}^{\prime}\models\varphi^{\prime}$ linked by an $n$-bisimulation $Z$. We construct trees $\mathcal{M}_{Z}\models\varphi$ and $\mathcal{M}_{Z}^{\prime}\models\varphi^{\prime}$ identical up to depth $n$, therefore reaching a contradiction with (iii).

Without loss of generality we assume that $\mathcal{M}$ and $\mathcal{M}^{\prime}$ are trees, otherwise they can be unravelled. The tree $\mathcal{M}_{Z}$ is as follows. It has universe:

$$M_{Z}=M\cup Z$$

and the pair consisting of the roots of $\mathcal{M}$ and $\mathcal{M}^{\prime}$ (which by assumption belongs to $Z$) is taken as the new root. Edges between pairs from $Z$ are defined pointwise (that is: $(v,v^{\prime})\stackrel{{\scriptstyle}}{{\to}}(w,w)$ iff $v\stackrel{{\scriptstyle}}{{\to}}w$ and $v^{\prime}\stackrel{{\scriptstyle}}{{\to}}w^{\prime}$). Edges between points in $M$ are taken from $\mathcal{M}$. On top of that, we add $(v,v^{\prime})\stackrel{{\scriptstyle}}{{\to}}w$ iff in $\mathcal{M}$ the point $v$ is at depth precisely $n$ and $v\stackrel{{\scriptstyle}}{{\to}}w$. The colors are inherited from $\mathcal{M}$ on $M$ and from whichever coordinate on $Z$ (points linked by $Z$ always have the same color).

Consider the function $f:M_{Z}\to M$ defined as the left projection on $Z$ and identity on $M$:

$$f(v,v^{\prime}) =v$$

$$f(v) =v.$$

The graph of $f$ is a bisimulation between $\mathcal{M}_{Z}$ and $\mathcal{M}$. In particular, $\mathcal{M}_{Z}$ satisfies $\varphi$. We define $\mathcal{M}_{Z}^{\prime}$ satisfying $\varphi^{\prime}$ symmetrically. Then $\mathcal{M}_{Z}$ and $\mathcal{M}_{Z}^{\prime}$ satisfy $\varphi$ and $\varphi^{\prime}$ and are identical up to depth $n$ (the $n$-prefixes of both $\mathcal{M}_{Z}$ and $\mathcal{M}_{Z}^{\prime}$ are equal $Z$). Technically, $\mathcal{M}_{Z}$ and $\mathcal{M}_{Z}^{\prime}$ are directed acyclic graphs but not necessarily trees. However, they can be turned into trees by removing inaccessible points and unravelling. Both these operations preserve satisfaction of $\varphi$ and $\varphi^{\prime}$ and identity of $n$-prefixes.

For the implication (ii) $\Rightarrow$ (i) one can define $\psi$ as (any) $n$-uniform consequence of $\varphi$. An explicit instance of such $n$-uniform consequence is the disjunction of all $\mathsf{ML}^{n}$-types consistent with $\varphi$ (see Definition 2 of $n$-uniform consequences and the following discussion).

Appendix C Separability over All Models is in ExpTime

We prove the upper bounds in Theorem 3. By Proposition 1 deciding modal separability boils down to checking if there is $n\in\mathbb{N}$ for which (iv) holds. Using well-known properties of $\mathsf{ML}$ and $\mu\mathsf{ML}$ (namely, closure under relativization) we may reduce the problem to the special case when models under consideration are full $k$-ary trees, meaning that every point has precisely $k$ children. Under this assumption the graphs underlying models are all isomorphic to the (unlabelled) full $k$-ary tree $\mathcal{K}=(K,\stackrel{{\scriptstyle}}{{\to}})$. Hence, we identify models with valuations $\mathsf{val}:K\to\Sigma$. Let us call a finite prefix $X\subseteq K$ sufficient for separation if for every $\mathsf{val},\mathsf{val}^{\prime}:K\to\Sigma$ identical on $X$: $\mathsf{val}\models\varphi$ implies $\mathsf{val}^{\prime}\models\neg\varphi^{\prime}$. Denote the set of such prefixes:

$$\mathsf{SEP}=\{X\subseteq K\ |\ \text{$X$ is a finite prefix of $K$ sufficient for separation}\}.$$

It follows directly from the definition that for every $n\in\mathbb{N}$:

The $$n K_{|_{n}} K \mathsf{SEP} \iff n$$-prefix of is in Condition (iv) is true for . (3)

The set $\mathsf{SEP}$ can be viewed as a language of finite trees. This language is closed under taking finite supermodels, so it contains $K_{|_{n}}$ for some $n$ iff it is nonempty. It follows that separability of $\varphi$ and $\varphi^{\prime}$ is equivalent to nonemptiness of $\mathsf{SEP}$.

We construct an automaton $\mathcal{B}$ that accepts finite trees not belonging to $\mathsf{SEP}$. Take automata $\mathcal{A}$ and $\mathcal{A}^{\prime}$ equivalent to $\varphi$ and $\varphi^{\prime}$ of size exponential in $k$. The idea is that given a finite tree $X\subseteq K$ the automaton $\mathcal{B}$ guesses $\mathsf{val}:X\to\Sigma$, $\rho:X\to Q$ and $\rho^{\prime}:X\to Q^{\prime}$ that can be extended to a valuation $\mathsf{val}_{+}:K\to\Sigma$ and accepting runs $\rho_{+}:K\to Q$ of $\mathcal{A}$ and $\rho_{+}^{\prime}:K\to Q^{\prime}$ of $\mathcal{A}^{\prime}$ consistent with $\mathsf{val}_{+}$. $\mathcal{B}$ has the set $Q^{\mathcal{B}}=Q\times Q^{\prime}$ as states and $(q_{I},q_{I}^{\prime})$ is the initial one. Transition function is defined in two steps. First take:

$$R\in\delta_{0}^{\mathcal{B}}(q,q^{\prime})$$

$$\iff$$

There is $$c\in\Sigma R$$, such that the left projection of

$$\text{belongs to $\delta(q,c)$ and the right one to $\delta^{\prime}(q^{\prime},c)$}.$$

This describes guessing a coloring on the full $\mathcal{K}$ and runs of both $\mathcal{A}$ and $\mathcal{A}^{\prime}$ consistent with that coloring. To handle points with less than $k$ children we put:

$$R\in\delta^{\mathcal{B}}(q,q^{\prime})$$

$$\iff$$

$$R R^{\prime}\in\delta_{0}^{\mathcal{B}}(q,q^{\prime})$$ can be obtained from some

by removing some consistent pairs.

Here consistency of a pair of states $(p,p^{\prime})$ means that there exists a model accepted by both $\mathcal{A}[q_{I}\mapsfrom p]$ and $\mathcal{A}^{\prime}[q_{I}^{\prime}\mapsfrom p^{\prime}]$. The (trivial) rank function of $\mathcal{B}$ assigns a bad rank to every state so that only finite trees are accepted.

To finish the proof let us first prove Proposition 2.

Proof.

Put $l=|Q|\times|Q^{\prime}|+1$. The proposition follows directly from (3) and:

$$\mathsf{SEP} \iff l K_{|_{l}} K$$ is nonempty it contains the -prefix of . (4)

Only the left-to-right implication is nontrivial and we prove it by contrapositive. If $K_{|_{l}}$ does not belong to $\mathsf{SEP}$ then this is witnessed by a run $\rho$ of $\mathcal{B}$ on $K_{|_{l}}$. Since every leaf $v$ of $K_{|_{l}}$ is at depth greater then $|Q^{\mathcal{B}}|$, on the path from the root to $v$ some state must repeat. Hence, the run can be pumped to finite prefixes of $K$ of arbitrarily big tallness. It follows that $\mathsf{SEP}$ is empty. This completes the proof of Proposition 2. ∎

The language of $\mathcal{B}$ is closed under taking submodels. Hence, the right hand side of (4) is equivalent to $\mathcal{B}$ not accepting any tree of tallness at least $l$ ($l$ is the exponential bound given by Proposition 2). This can be easily checked in time polynomial in the size of $\mathcal{B}$.

Appendix D Separability over Words is in PSpace

We prove the upper bounds in Theorem 4. We proceed with the same argument as in the case with general models, with two major simplifications. First, over words bisimilarity and identity coincide. Thus the equivalence of items (ii), (iii) and (iv) of Proposition 1 becomes trivial in the word case. Second, bounded tallness (which over words is the same as finiteness) of the language of the appropriate word automaton $\mathcal{B}$ can be checked more easily. Instead of writing down the automaton we construct it on the fly, and only remember a single state at every moment. This yields a PSpace (and not ExpTime) decision procedure.

Appendix E Lower Bounds over All Models

We construct formulae of $\mu\mathsf{ML}$ for which there exist equivalent formulae in $\mathsf{ML}$ but only doubly exponentially larger.

Consider the nonstandard modal operator $\langle\exists^{r}\rangle$ which means “there exists a point reachable from the root and satisfying”. It is straightforward to encode such modality (and its dual $[\exists^{r}]$ meaning “for every reachable point”) by a $\mu\mathsf{ML}$ formula of constant size. It therefore suffices to define the sequence $(\varphi_{n})_{n\in\mathbb{N}}$ in the extension $\mathsf{ML}+\exists^{r}$ of $\mathsf{ML}$ with such operators.

We construct $\varphi_{n}$. For convenience assume $n+1$ atomic propositions $\tau_{0},...,\tau_{n}$ (otherwise we encode these without a significant blowup in the size of $\varphi_{n}$). The propositions can be seen as an encoding of an $(n+1)$-bit binary counter. Consider the following property $C_{n}$ of models: the color of the root encodes counter value $0$ and for every (reachable) point $v$ if the color of $v$ encodes number $i$ then either $i=2^{n}$ and $v$ has no children or all $v$’s children have a color that encodes $i+1$. The property $C_{n}$ can be easily expressed by a $\mathsf{ML}+\exists^{r}$ formula $\varphi_{n}$ of size polynomial in $n$. Such $\varphi_{n}$ is equivalent to a modal formula. This follows immediately from Proposition 1 since property $C_{n}$ implies that there are no paths longer than $2^{n}$.

However, no $\mathsf{ML}$ formula smaller than $2^{2^{n}}$ can be equivalent to $\varphi_{n}$. To see this assume $\psi\in\mathsf{ML}$ equivalent to $\varphi_{n}$. For every sequence of colors $\mathsf{a}_{1},...\mathsf{a}_{2^{n}}$ of length $2^{n}$, $\psi$ must contain a sequence $\xi_{1},...,\xi_{2^{n}}$ of subformulae such that:

• $\xi_{i}$ is a strict subformula of $\xi_{j}$ whenever $i>j$;

• each $\xi_{i}$ begins with $\langle\mathsf{a}_{i}\rangle$ or $[\mathsf{a}_{i}]$;

• the least strict superformula of $\xi_{i}$ beginning with a modal operator is $\xi_{i+1}$.

If $\psi$ did not contain such sequence $\xi_{1},...,\xi_{2^{n}}$, it would be indifferent to what happens in points only reachable via paths labelled with $\mathsf{a}_{1},...\mathsf{a}_{2^{n}}$. It follows that there is an embedding of the $2^{n}$-prefix of the full binary tree to the syntax tree of $\psi$ and so it has size at least $2^{2^{n}}$.

Note that the use of multiple atomic propositions in the above construction is only for convenience. With any reasonable encoding the proof could be adapted even to the setting with $\mathsf{Prop}=\emptyset$.

Appendix F Optimal Separators over Words

We prove Lemma 3. Recall that $\mathcal{A}=(Q,\Sigma,\delta,q_{I},\mathsf{rank})$ is the automaton under consideration. Since we are working over words, $\delta(q,c)$ contains only singleton sets and possibly the emtpy set. The latter case, $\emptyset\in\delta(q,c)$, is of particular interest because this means that the automaton in state $q$ reading color $c$ can “accept” even if it has not finished reading the input; in particular, the automaton can accept finite words as well. Denote with $\textit{Acc}_{q}$ the set of colors $c$ with $\emptyset\in\delta(q,c)$. Further denote with $\textit{Cont}_{q}$ the set of all $c$ such that $\mathcal{A}[q_{I}\mapsfrom q]$ accepts a word starting with color $c$.

We first construct $\mathsf{ML}$ formulae $\psi^{m}_{pq}$, for $m\in\mathbb{N},p,q\in Q$ such that for every word $\mathcal{M}$:

• $\mathcal{M}\models\psi^{m}_{pq}$ iff there is a run of $\mathcal{A}$ from $p$ to $q$ on the $m$-prefix of $\mathcal{M}$.

The definition is by induction on $m$:

$$\psi^{0}_{pq} =\text{ if $p\neq q$ then $\bot$ else $\top$}$$

$$\psi^{1}_{pq} =\bigvee\{c\ \mid\ c\in\Sigma,\{q\}\in\delta(p,c)\}$$

$$\psi^{m}_{pq} =\bigvee_{q^{\prime}\in Q}\psi^{\lfloor m/2\rfloor}_{pq^{\prime}}\wedge\psi^{\lceil m/2\rceil}_{q^{\prime}q}$$

It is routine to verify that $\psi^{m}_{pq}$ satisfies $(\ast)$ and is of size $|\psi^{m}_{pq}|\in O(|Q|\cdot m^{2})$.

We finish the construction by setting:

$$\psi_{n}=\bigvee_{q\in Q}\left(\psi^{n}_{q_{I}q}\wedge\Box^{n}\bigvee_{c\in\textit{Cont}_{q}}c\right)\vee\bigvee_{m\leq n}\bigvee_{q\in Q}\left(\psi^{m}_{q_{I}q}\wedge\Box^{m+1}\bot\wedge\Box^{m}\bigvee_{c\in\textit{Acc}_{q}}c\right).$$

It is readily checked that $\psi_{n}$ satisfies the required size bounds. To verify that $\psi_{n}\models\theta$ for every $\theta\in\mathsf{ML}^{n}$ with $\mathcal{A}\models\theta$, we show the following equivalence for all words $\mathcal{M}$:

$$\mathcal{M}\models\psi_{n}\text{\hskip 14.22636pt $\iff$ \hskip 14.22636pt there exists $\mathcal{N}\models\mathcal{A}$ with $\mathcal{N}\leftrightarroweq^{n}\mathcal{M}$.}$$ (5)

For $\Rightarrow$, let $\mathcal{M}$ be a word structure with $\mathcal{M}\models\psi_{n}$. If $\mathcal{M}\models\psi^{n}_{q_{I}q}\wedge\Box^{n}\bigvee_{c\in\textit{Cont}_{q}}c$ for some $q$, then by $(\ast)$, there is a run of $\mathcal{A}$ from the initial state $q_{0}$ to some state $q\in Q$ when reading the $n$-prefix of $\mathcal{M}$, and the last color in the prefix is $c$. Since $c\in\textit{Cont}_{q}$, we can extend the $n$-prefix of $\mathcal{M}$ to a word $\mathcal{N}$ accepted by $\mathcal{A}$. If $\mathcal{M}\models\psi^{m}_{q_{I}q}\wedge\Box^{m+1}\bot\wedge\bigvee_{c\in\textit{Acc}_{q}}c$, for some $m\leq n$ and $q\in Q$, then $\mathcal{M}$ is a finite word of depth $m$ that is accepted by the automaton. We can take $\mathcal{N}=\mathcal{M}$ in this case.

For $\Leftarrow$, let $\mathcal{M}$ be a word such that there is some $\mathcal{N}\models\varphi$ with $\mathcal{N}\leftrightarroweq^{n}\mathcal{M}$. The former condition implies that $\mathcal{N}\models\mathcal{A}$ and thus there is an accepting run $\rho$ of $\mathcal{A}$ on $\mathcal{N}$, and the latter implies that $\mathcal{N}$ and $\mathcal{M}$ coincide on their $n$-prefixes. We distinguish cases. If the depth of $\mathcal{N}$ is greater than $n$, then the $n$-prefix of $\rho$ ending in state $q$ witnesses $\mathcal{M}\models\psi^{n}_{q_{I}q}\wedge\Box^{n}\bigvee_{c\in\textit{Cont}_{q}}c$. Otherwise, the depth of $\mathcal{N}$ is $m\leq n$ and the run $\rho$ ending in $q$ witnesses that $\mathcal{M}\models\psi^{m}_{q_{I}q}\wedge\Box^{m+1}\bot\wedge\bigvee_{c\in\textit{Acc}_{q}}c$.