Modal Separation of Fixpoint Formulae

Jung, Jean Christoph; Kołodziejski, Jędrzej

doi:10.4230/LIPIcs.STACS.2025.55

Modal Separation of Fixpoint Formulae

Jean Christoph Jung

TU Dortmund University, Germany Jędrzej Kołodziejski

TU Dortmund University, Germany

Abstract

Modal separability for modal fixpoint formulae is the problem to decide for two given modal fixpoint formulae $\varphi,\varphi^{\prime}$ whether there is a modal formula $\psi$ that separates them, in the sense that $\varphi\models\psi$ and $\psi\models\neg\varphi^{\prime}$ . We study modal separability and its special case modal definability over various classes of models, such as arbitrary models, finite models, trees, and models of bounded outdegree. Our main results are that modal separability is PSpace-complete over words, that is, models of outdegree $\leq 1$ , ExpTime-complete over unrestricted and over binary models, and 2-ExpTime-complete over models of outdegree bounded by some $d\geq 3$ . Interestingly, this latter case behaves fundamentally different from the other cases also in that modal logic does not enjoy the Craig interpolation property over this class. Motivated by this we study also the induced interpolant existence problem as a special case of modal separability, and show that it is coNExpTime-complete and thus harder than validity in the logic. Besides deciding separability, we also investigate the problem of efficient construction of separators. Finally, we consider in a case study the extension of modal fixpoint formulae by graded modalities and investigate separability by modal formulae and graded modal formulae.

Keywords and phrases:

Modal Logic, Fixpoint Logic, Separability, Interpolation

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Modal and temporal logics

DOI:

10.4230/LIPIcs.STACS.2025.55

Event:

42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Editors:

Olaf Beyersdorff, Michał Pilipczuk, Elaine Pimentel, and Nguyễn Kim Thắng

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

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 logics under consideration. Both separability and definability are central problems with many applications in computer science. As seminal work let us only mention definability and separability of regular word languages by first-order logic [26, 29, 9].

In this paper we study definability and separability of formulae of the modal $\mu$ -calculus $\mu\mathsf{ML}$ [27, 20] by formulae in propositional modal logic $\mathsf{ML}$ . $\mu\mathsf{ML}$ is the extension of $\mathsf{ML}$ with fixpoints that encompasses virtually all specification languages such as $\mathsf{PDL}$ [12] and $\mathsf{LTL}$ and $\mathsf{CTL}$ [3]. Let us consider an example.

Example 1.

Consider the following properties $P_{1},P_{2},P_{3}$ of vertex-labelled trees:

$\blacksquare$

$P_{1}$ : there is an infinite path starting in the root on which each point satisfies $a$ ;
$\blacksquare$

$P_{2}$ : on every path there are only finitely many points satisfying $a$ ;
$\blacksquare$

$P_{3}$ : on every path at most two points satisfy $a$ .

The properties are expressible in $\mu\mathsf{ML}$ but not in $\mathsf{ML}$ , and both $P_{1},P_{2}$ and $P_{1},P_{3}$ are mutually exclusive. The properties $P_{1},P_{3}$ are separated by the $\mathsf{ML}$ -formula $\psi=a\wedge\Diamond(a\wedge\Diamond a)$ which expresses that there is a path starting with three points satisfying $a$ . On the other hand, no $\mathsf{ML}$ -formula separates $P_{1},P_{2}$ . The intuitive reason for this is that any $\mathsf{ML}$ -formula $\psi$ only sees trees up to depth $|\psi|$ , and one can find two trees with properties $P_{1},P_{2}$ which nonetheless look the same up to depth $|\psi|$ . ∎

We explore the definability and separability problems over several classes of models relevant for computer science: all models, words, trees of bounded or unbounded outdegree; as well as restrictions of all these classes to finite models. On top of analyzing the decision problems, we also address the problem of constructing efficient definitions and separators whenever they exist. The starting point for our research is the seminal paper of Otto [24], where he solves modal definability over models of bounded and unbounded outdegree. In this paper, we continue this line of research and establish a fairly complete and interesting picture. Table 1 summarizes our results. We now explain its content further.

Table 1: Overview of our results. All complexity results are completeness results.

	all models	words	binary trees	$d$ -ary trees, $d\geq 3$
$\mathsf{ML}$ -definability	ExpTime [24]	PSpace	ExpTime [24]	ExpTime [24]
$\mathsf{ML}$ -separability	ExpTime	PSpace	ExpTime	2-ExpTime
separator construction	double exp.	single exp.	double exp.	triple exp.
$\mathsf{ML}$ interpolant existence	always	always	always	coNExpTime

The first line essentially repeats Otto’s results; we only add the observation that $\mathsf{ML}$ -definability over words is PSpace-complete. Interestingly, separability is substantially more difficult. The case of words is the easiest one, both in terms of computational complexity and required arguments. Next come the cases of binary and of unrestricted trees. These two classes possess some nice structural properties which (although true for different reasons) enable a common algorithmic treatment. Finally, the cases of trees with outdegree bounded by a number $d\geq 3$ enter the stage. These trees lack the good properties essential for previous constructions which results in higher computational complexity. The hardness result for $d\geq 3$ is interesting for two reasons. First, as it is entirely standard to encode trees of higher outdegree into binary ones, one could expect the ternary (and higher) case to have the same complexity as the binary one. And second, even though there are known cases when separation is provably harder than definability (regularity of visibly pushdown languages is decidable [23, Theorem 19] but regular separability thereof is not [19, Theorem 2.4]), to the best of our knowledge our results are the only such case known in logic.

The complexity landscape for deciding separability is also reflected in the maximal sizes of the separators that we construct. Relying on the well-known connection of $\mu\mathsf{ML}$ to automata, we provide effective constructions for the cases of all models, words, and binary trees. It is worth mentioning that equally effective constructions for definability over all models are given in [22], but they do not work for separability. The ternary case follows from a general argument. Our construction of separators over words is optimal. Under mild assumptions (there are at least two modalities) the constructions over binary and over unrestricted trees are optimal as well, but we leave it open whether these assumptions are needed for the lower bounds. In the case of ternary and higher outdegree trees we only conjecture optimality of the constructed separators.

Finally, we observe that $\mathsf{ML}$ lacks the Craig interpolation property over trees of outdegree bounded by $d\geq 3$ . Recall that a Craig interpolant for $\varphi\models\varphi^{\prime}$ in some logic $\mathcal{L}$ is a formula $\psi\in\mathcal{L}$ only using the common symbols of $\varphi$ and $\varphi^{\prime}$ and such that $\varphi\models\psi\models\varphi^{\prime}$ . A logic satisfies the Craig interpolation property (CIP) if a Craig interpolant of $\varphi\models\varphi^{\prime}$ always exists. It is known that $\mathsf{ML}$ enjoys CIP over all models and over words [15] and it follows from our techniques that this transfers to binary trees. In contrast and as mentioned above, over ternary and higher-arity trees $\mathsf{ML}$ lacks the CIP. It is worth mentioning that modal logic over frames of arity bounded by some $d$ has been studied under the name $\mathbf{K}\oplus\textit{{alt}}_{d}$ [4]. Our results imply that $\mathbf{K}\oplus\textit{{alt}}_{d}$ enjoys CIP iff $d\leq 2$ . Motivated by the lack of CIP over higher-arity trees, we study the induced interpolant existence problem – determining whether two given $\mathsf{ML}$ -formulae $\varphi,\varphi^{\prime}$ admit a Craig interpolant – as a special case of separability. We show it to be coNExpTime-complete over higher arity trees, and thus harder than validity. Interpolant existence has recently been studied for other logics without CIP [18, 1].

As an application of our results for $d$ -ary trees with $d\geq 3$ we additionally present a case study: separability in the graded setting in which we allow counting modalities saying “there are at least $k$ children such that […]” [11]. Counting modalities are a standard extension of modal logic that is especially relevant in applications in knowledge representation for conceptual modeling [2]. We show that $\mathsf{ML}$ -separability of graded $\mu\mathsf{ML}$ is 2-ExpTime-complete, while it is ExpTime-complete if we allow counting modalities also in the separator. The intuitive reason for the hardness in the former case is that trees of bounded arity are definable in graded $\mu\mathsf{ML}$ . This former case is also related with a recent study about separating logics supporting counting quantifiers by logics without these [21].

It is worth to mention that $\mathsf{ML}$ -definability of $\mu\mathsf{ML}$ -formulae generalizes the boundedness problem which asks whether a formula with a single fixpoint is equivalent to a modal formula. Boundedness has been studied for other logics such as monadic-second order logic [6], datalog [16], and the guarded fragment of first-order logic [5]. Our paper is an extension of the preliminary paper [17].

The paper is organized as follows. After this introduction 1, we set notation and recall basic facts in the preliminary Section 2. Next, we introduce some topic-specific terminology, discuss a relevant construction of Otto, and solve the case of all models in Section 3. In the following Sections 4 and 5 we deal with unary and binary trees, and in Section 6 we solve the most challenging case of trees of outdegree bounded by $d\geq 3$ . Section 7 applies our results to the case with graded modalities. The last Section 8 contains conclusions and final remarks.

2 Preliminaries

We recall the main notions about modal logic $\mathsf{ML}$ and the modal $\mu$ -calculus $\mu\mathsf{ML}$ . For the rest of this paper fix disjoint, countably infinite sets $\mathsf{Prop}$ of atomic propositions and $\mathsf{Var}$ of variables. The syntax of $\mu\mathsf{ML}$ is given by the rule

\varphi::=\tau\ |\ \neg\tau\ |\ \varphi\vee\varphi\ |\ \varphi\wedge\varphi\ |% \ \Diamond\varphi\ |\ \Box\varphi\ |\ x\ |\ \mu x.\varphi\ |\ \nu x.\varphi

where $\tau\in\mathsf{Prop}$ and $x\in\mathsf{Var}$ . We assume that formulae of $\mu\mathsf{ML}$ are in a normal form such that every $x\in\mathsf{Var}$ appears at most once in a formula, and if it does appear then its appearance has a unique superformula $\psi$ beginning with $\mu x$ or $\nu x$ . Modal logic $\mathsf{ML}$ is defined as the fragment of $\mu\mathsf{ML}$ with no fixpoint operators $\mu$ and $\nu$ nor variables. Both in $\mathsf{ML}$ and $\mu\mathsf{ML}$ , we use abbreviations like $\top$ (for $a\vee\neg a$ for some $a\in\mathsf{Prop}$ ), $\Diamond^{n}\varphi$ (for a formula $\Diamond\ldots\Diamond\varphi$ with $n$ leading $\Diamond$ ’s), and $\neg\varphi$ . We denote with $\text{sig}(\varphi)$ the set of propositions that occur in $\varphi$ , and recall that the modal depth of an $\mathsf{ML}$ formula is the maximal nesting of $\Diamond,\Box$ . With $\mathsf{ML}^{n}$ we denote the class of all $\mathsf{ML}$ -formulae of modal depth at most $n$ , and with $\mathsf{ML}^{n}_{\sigma}$ we denote its subclass restricted to signature $\sigma$ . The size $|\varphi|$ of a formula $\varphi$ is the length of $\varphi$ represented as a string. This choice of the simplest possible measure of size does not matter for most of our results. We will briefly discuss alternative notions of size in the concluding Section 8.

Both $\mathsf{ML}$ and $\mu\mathsf{ML}$ are interpreted in pointed Kripke structures. More formally, a model $\mathcal{M}$ is a quadruple $\mathcal{M}=(M,v_{I},{\to},\mathsf{val})$ consisting of a set $M$ called its universe, a distinguished point $v_{I}\in M$ called the root, an accessibility relation ${\to}\subseteq M\times M$ , and a valuation $\mathsf{val}:M\to\mathcal{P}(\mathsf{Prop})$ .

The semantics of $\mu\mathsf{ML}$ can be defined in multiple equivalent ways. The one most convenient for us is through parity games (see [32] for an introduction). Given a model $\mathcal{M}$ and a formula $\varphi\in\mu\mathsf{ML}$ we define a semantic game $\mathcal{G}(\mathcal{M},\varphi)$ played between players $\exists\text{ve}$ and $\forall\text{dam}$ . The positions are $M\times\mathsf{SubFor}(\varphi)$ . The moves depend on the topmost connective. From a position of the shape $(v,\psi\vee\psi^{\prime})$ or $(v,\psi\wedge\psi^{\prime})$ it is allowed to move to either $(v,\psi)$ or $(v,\psi^{\prime})$ . From $(v,\Diamond\psi)$ and $(v,\Box\psi)$ the allowed moves lead to all $(w,\psi)$ such that $v\rightarrow w$ . In position $(v,\tau)$ or $(v,\neg\tau)$ the game stops and $\exists\text{ve}$ wins iff $v$ satisfies the formula component $\tau$ or $\neg\tau$ , respectively. From $(v,\mu x.\psi)$ and $(v,\mu x.\psi)$ the game moves to $(v,\psi)$ , and from $(v,x)$ to $(v,\psi)$ where $\psi$ is the unique superformula of $x$ beginning with $\mu x$ or $\nu x$ . $\exists\text{ve}$ owns positions whose formula component has $\vee$ or $\Diamond$ as the topmost connective and $\forall\text{dam}$ owns all other positions. $\exists\text{ve}$ wins an infinite play $\pi$ if the outermost subformula seen infinitely often in $\pi$ begins with $\nu$ . We say that $\mathcal{M},v$ satisfies $\varphi$ and write $\mathcal{M},v\models\varphi$ if $\exists\text{ve}$ wins the game $\mathcal{G}(\mathcal{M},\varphi)$ from position $(v,\varphi)$ . Since $\mathcal{M}$ is by definition pointed, we abbreviate $\mathcal{M},v_{I}\models\varphi$ with $\mathcal{M}\models\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 $\mathbf{C}$ are considered we talk about satisfiability and entailment over $\mathbf{C}$ . Let $\mathcal{L}$ be a subset of $\mu\mathsf{ML}$ such as $\mathsf{ML}$ or $\mathsf{ML}_{\sigma}^{n}$ . If two models $\mathcal{M}$ and $\mathcal{N}$ satisfy the same formulae of $\mathcal{L}$ then we call them $\mathcal{L}$ -equivalent and write $\mathcal{M}\equiv_{\mathcal{L}}\mathcal{N}$ .

In the paper we will study models of bounded and unbounded outdegree. The outdegree of a point $w\in M$ in a model $\mathcal{M}=(M,v_{I},\to,\mathsf{val})$ is the number of successors of $w$ in the underlying directed graph $G_{\mathcal{M}}=(M,\to)$ . We say that $\mathcal{M}$ has finite outdegree if every point has finite outdegree and bounded outdegree if there is a finite uniform upper bound $d$ on the outdegree of its points. In the latter case, we will call $\mathcal{M}$ $d$ -ary, and binary or ternary if $d=2$ or $d=3$ . If $d=1$ , then we call $\mathcal{M}$ a word. A $d$ -ary model is full if each of its nodes is either a leaf (i.e. has no children) or has precisely $d$ children. A model $\mathcal{M}$ is a tree if $G_{\mathcal{M}}$ is a (directed) tree with root $v_{I}$ . We denote with $\mathbb{T}^{d}$ the class of all $d$ -ary tree models. Both $\mathsf{ML}$ and $\mu\mathsf{ML}$ are invariant under bisimulation, and every ( $d$ -ary) model is bisimilar to a ( $d$ -ary) tree. Hence, we do not loose generality by only looking at tree models.

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}}$ ).

Bisimulations

We define bisimulations and bisimilarity for trees, assuming for convenience that bisimulations only link points at the same depth. Let $\mathcal{M},\mathcal{M}^{\prime}$ be trees and $Z\subseteq M\times M^{\prime}$ a relation between $M$ and $M^{\prime}$ that relates only points of the same depth. Then, $Z$ is a bisimulation between $\mathcal{M}$ and $\mathcal{M}^{\prime}$ if it links the roots $v_{I}Zv_{I}^{\prime}$ , and for every $wZw^{\prime}$ the following conditions are satisfied:

$(\mathsf{atom})$: $\mathsf{val}(w)=\mathsf{val}^{\prime}(w^{\prime})$ ,
$(\mathsf{forth})$: for every $v\in M$ with $w\to v$ there is a $v^{\prime}\in M^{\prime}$ with $w^{\prime}\to v^{\prime}$ and $vZv^{\prime}$ , and
$(\mathsf{back})$: for every $v^{\prime}\in M^{\prime}$ with $w^{\prime}\to v^{\prime}$ there is a $v\in M$ with $w\to v$ and $vZv^{\prime}$ .

A functional bisimulation (also known as bounded morphism) is a function whose graph is a bisimulation. If $Z$ is a functional bisimulation from $\mathcal{M}$ to $\mathcal{M}^{\prime}$ then we write $Z:\mathcal{M}\stackrel{{\scriptstyle\mathsf{bis}}}{{\to}}{}\mathcal{M}^{\prime}$ and call $\mathcal{M}^{\prime}$ a bisimulation quotient of $\mathcal{M}$ . The bisimilarity quotient of $\mathcal{M}$ is a quotient $\mathcal{M}^{\prime}$ of $\mathcal{M}$ such that if $Z^{\prime}:\mathcal{M}^{\prime}\to\mathcal{M}^{\prime\prime}$ then $\mathcal{M}^{\prime}=\mathcal{M}^{\prime\prime}$ . It follows from analogous results for arbitrary models that every tree $\mathcal{M}\in\mathbb{T}^{d}$ has a unique (up to isomorphism) bisimilarity quotient $\mathcal{M}^{\prime}\in\mathbb{T}^{d}$ and that two trees are bisimilar iff their bisimilarity quotients are isomorphic.

Further, for every $n\in\mathbb{N}$ and every subset $\sigma\subseteq\mathsf{Prop}$ of the signature we consider a restricted variant of bisimulations called $(\sigma,n)$ -bisimulations. In a $(\sigma,n)$ -bisimulation the $\mathsf{atom}$ condition is only checked with respect to $\sigma$ and the $\mathsf{back}$ and $\mathsf{forth}$ conditions only for points at depth smaller than $n$ . Formally, a relation $Z\subseteq M\times M^{\prime}$ is a $(\sigma,n)$ -bisimulation if it is a bisimulation between the $n$ -prefixes of the $\sigma$ -reducts of $\mathcal{M},\mathcal{M}^{\prime}$ . We call a $(\sigma,n)$ -bisimulation between $\mathcal{M},\mathcal{M}^{\prime}$ a $(\sigma,n)$ -isomorphism if it is bijective on the $n$ -prefixes of $\mathcal{M},\mathcal{M}^{\prime}$ . We write $\mathcal{M}\leftrightarroweq_{\sigma}^{n}\mathcal{M}^{\prime}$ if there exists a $(\sigma,n)$ -bisimulation between $\mathcal{M}$ and $\mathcal{M}^{\prime}$ and $\mathcal{M}\cong_{\sigma}^{n}\mathcal{M}^{\prime}$ if there is a $(\sigma,n)$ -isomorphism between them. Crucially, over every class $\mathbf{C}$ of models and for every finite $\sigma$ the equivalences $\equiv_{\mathsf{ML}_{\sigma}^{n}}$ and $\leftrightarroweq_{\sigma}^{n}$ coincide, for every $n$ .

Automata

We exploit the well-known connection of $\mu\mathsf{ML}$ and automata that read tree models. 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=\mathcal{P}(\sigma)$ for some finite set $\sigma\subseteq\mathsf{Prop}$ , $\mathsf{rank}$ assigns each state a priority, and $\delta$ is a transition function of type:

\delta:Q\times\Sigma\to\mathcal{P}(Q^{\leq d}),

where $Q^{\leq d}$ denotes the set of all tuples over $Q$ of length at most $d$ . A run of $\mathcal{A}$ on a tree $\mathcal{M}$ is an assignment $\rho:M\to Q$ sending the root of the tree to $q_{I}$ and consistent with $\delta$ in the sense that $(\rho(v_{1}),...,\rho(v_{k}))\in\delta(\rho(v),\mathsf{val}(v)\cap\sigma)$ for every point $v$ with children $v_{1},...,v_{k}$ . On occasion when considering trees of unbounded outdegree we will use automata with transition function of type $\delta:Q\times\Sigma\to\mathcal{P}(\mathcal{P}(Q))$ . Then, consistency of $\rho$ with $\delta$ means that $\{\rho(v^{\prime})\ |\ v^{\prime}\in V\}\in\delta(\rho(v),\mathsf{val}(v)\cap\sigma)$ for every $v$ with a set $V$ of children. In either case, we call the run $\rho$ 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]$ . The size of an automaton $\mathcal{A}$ is the number of its states and is denoted by $|\mathcal{A}|$ .

An NPTA $\mathcal{A}$ is equivalent to a formula $\varphi\in\mu\mathsf{ML}$ over a class $\mathbf{C}$ of trees when $\mathcal{M}\models\varphi$ iff $\mathcal{M}\models\mathcal{A}$ for every tree $\mathcal{M}\in\mathbf{C}$ . We rely on the following classical result (see for example the discussion in [31] and the well-presented Dealternation Theorem 5.7 in [7]):

Theorem 2.

For every $\mu\mathsf{ML}$ -formula $\varphi$ and class $\mathbf{C}$ of trees, we can construct an NPTA with exponentially many states equivalent to $\varphi$ over $\mathbf{C}$ . The construction takes exponential time when $\mathbf{C}\subseteq\mathbb{T}^{d}$ for some $d$ , and doubly exponential time in the unrestricted case.

3 Foundations of Separability

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

Definition 3.

Assume a subset $\mathcal{L}$ of all $\mu\mathsf{ML}$ formulae. Given $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ , an $\mathcal{L}$ -separator of $\varphi,\varphi^{\prime}$ is a formula $\psi\in\mathcal{L}$ with $\varphi\models\psi$ and $\psi\models\neg\varphi^{\prime}$ . If additionally $\text{sig}(\psi)\subseteq\sigma$ for some signature $\sigma$ , $\psi$ is called an $\mathcal{L}_{\sigma}$ -separator.

The $\mathcal{L}$ -separability problem is to determine, given formulae $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ and a signature $\sigma$ , if they admit an $\mathcal{L}_{\sigma}$ -separator $\psi$ . $\mathcal{L}$ -definability is the special case of $\mathcal{L}$ -separability in which $\varphi^{\prime}=\neg\varphi$ , since an $\mathcal{L}$ -separator of $\varphi,\neg\varphi$ is equivalent to $\varphi$ . All notions can be relativized to a class $\mathbf{C}$ of models by considering entailment over that class. We investigate $\mathsf{ML}$ -separability and $\mathsf{ML}$ -definability over different classes of models. The reader may have expected the problems to be defined without restrictions on $\sigma$ , but in fact such versions of the problems are special instances of our problems with $\sigma=\text{sig}(\varphi)\cup\text{sig}(\varphi^{\prime})$ . Conversely, all lower bounds already hold for such special instances.

We start with observing that, by the tree model property and the finite model property of $\mu\mathsf{ML}$ , $\psi$ is an $\mathsf{ML}_{\sigma}$ -separator of $\varphi,\varphi^{\prime}$ (over all models) iff $\psi$ is an $\mathsf{ML}_{\sigma}$ -separator of $\varphi,\varphi^{\prime}$ over trees iff $\psi$ is an $\mathsf{ML}_{\sigma}$ -separator of $\varphi,\varphi^{\prime}$ over finite models. Thus, separability coincides over all these classes. Moreover, with the help of the $\mu\mathsf{ML}$ -formula $\theta_{\infty}=\nu x.\Diamond x$ expressing the existence of an infinite path originating in the root, $\mathsf{ML}$ -separability over finite trees reduces to $\mathsf{ML}$ -separability over all models. More formally:

Lemma 4.

Let $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ and $\psi\in\mathsf{ML}$ . Then $\psi$ is an $\mathsf{ML}_{\sigma}$ -separator of $\varphi,\varphi^{\prime}$ over finite trees iff $\psi$ is an $\mathsf{ML}_{\sigma}$ -separator of $\varphi\wedge\neg\theta_{\infty},\varphi^{\prime}\wedge\neg\theta_{\infty}$ . This is also true inside $\mathbb{T}^{d}$ , for $d\in\mathbb{N}$ .

This lemma allows us to transfer all upper bounds obtained in the paper also to the restrictions of the classes to finite models. The lower bounds do not follow from this lemma, but analyzing the proofs yields that they actually work as well. Thus, in the rest of the paper we focus on the classes of all models and $\mathbb{T}^{d}$ , for $d\in\mathbb{N}$ .

The starting point for the technical developments in the paper are model-theoretic characterizations for separability. Similar to what has been done in the context of interpolation, see for example [28], they are given in terms of joint consistency, which we introduce next. Let $R$ be a binary relation on some class of models, such as $(\sigma,n)$ -isomorphism $\cong_{\sigma}^{n}$ or $\mathsf{ML}_{\sigma}^{n}$ -equivalence $\equiv_{\mathsf{ML}_{\sigma}^{n}}$ . We call two formulae $\varphi,\varphi^{\prime}$ joint consistent up to $R$ (in short joint $R$ -consistent) if there are models $\mathcal{M}\models\varphi$ and $\mathcal{M}^{\prime}\models\varphi^{\prime}$ with $R(\mathcal{M},\mathcal{M}^{\prime})$ . For technical reasons we will sometimes also talk about joint consistency of automata $\mathcal{A},\mathcal{A}^{\prime}$ in place of formulae $\varphi,\varphi^{\prime}$ . Joint $R$ -consistency over a class $\mathbf{C}$ of models is defined by only looking at models from $\mathbf{C}$ . Clearly, if $R^{\prime}\subseteq R$ and $\mathbf{C}^{\prime}\subseteq\mathbf{C}$ then joint $R^{\prime}$ -consistency over $\mathbf{C}^{\prime}$ implies joint $R$ -consistency over $\mathbf{C}$ . We use the following standard equivalence:

\varphi,\varphi^{\prime}

are not

\mathsf{ML}_{\sigma}^{n}

-separable over

\mathbf{C}

\iff

\varphi,\varphi^{\prime}

are joint

\leftrightarroweq_{\sigma}^{n}

-consistent over

\mathbf{C}

.

(

\mathsf{Base}

)

for every $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ , $n\in\mathbb{N}$ , finite $\sigma$ , and class $\mathbf{C}$ . The implication from right to left is immediate. The opposite one follows from the observation that for every $n\in\mathbb{N}$ and finite $\sigma$ there are only finitely many equivalence classes of $\leftrightarroweq_{\sigma}^{n}$ , and each such class is fully described with a single modal formula.

Let us illustrate how Equivalence ( $\mathsf{Base}$ ) is used to solve $\mathsf{ML}$ -separability. Let $\varphi_{1}$ and $\varphi_{2}$ be $\mu\mathsf{ML}$ -formulae expressing the respective properties $P_{1}$ and $P_{2}$ from Example 1. Let $\mathcal{M}$ be an infinite path in which every point satisfies $a$ , and let $\mathcal{M}_{n}$ be a finite path of length $n$ in which every point satisfies $a$ . Then, for each $n$ the models $\mathcal{M},\mathcal{M}_{n}$ witness joint $\leftrightarroweq^{n}$ -consistency of $\varphi_{1},\varphi_{2}$ . By Equivalence ( $\mathsf{Base}$ ) this means that $\varphi_{1},\varphi_{2}$ are not $\mathsf{ML}^{n}$ -separable for any $n$ , and thus not $\mathsf{ML}$ -separable at all.

Definability is a special case of separability. Since the tools used for solving definability are a starting point for our work, we recall them now.

Modal Definability: A Recap

In his seminal paper [24] Otto showed that $\mathsf{ML}$ -definability of $\mu\mathsf{ML}$ -formulae is ExpTime-complete over all models and over $\mathbb{T}^{d}$ for every $d\geq 2$ .

Theorem 5 ([24, Main Theorem and Proposition 5]).

Over the class of all models, as well as over $\mathbb{T}^{d}$ for every $d\geq 2$ , $\mathsf{ML}$ -definability of $\mu\mathsf{ML}$ -formulae is ExpTime-complete.

We start by recalling and rephrasing Otto’s construction and fixing a small mistake in the original proof. The lower bound follows by an immediate reduction from satisfiability of $\mu\mathsf{ML}$ -formulae. We look at the upper bound. The first step is the following lemma, which is the heart of [24, Lemma 2].

Lemma 6.

For every $\varphi\in\mu\mathsf{ML}$ and $n,d\in\mathbb{N}$ the following are equivalent:

1.

$\varphi,\neg\varphi$ are joint $\leftrightarroweq_{\sigma}^{n}$ -consistent over $\mathbb{T}^{d}$ .
2.

$\varphi,\neg\varphi$ are joint $\cong_{\sigma}^{n}$ -consistent over $\mathbb{T}^{d}$ .

The lemma is true, but its proof in [24] is mistaken. The problem there is that the construction duplicates subtrees and hence may turn $d$ -ary models into ones with outdegree greater than $d$ . We present an easy alternative proof.

Proof.

Only the implication 1 $\Rightarrow$ 2 is nontrivial. To prove it assume $d$ -ary $\mathcal{M}\models\varphi$ , $\mathcal{N}\models\neg\varphi$ with $\mathcal{M}\leftrightarroweq_{\sigma}^{n}\mathcal{N}$ and assume towards contradiction that $\varphi,\neg\varphi$ are not $\cong_{\sigma}^{n}$ -consistent over $\mathbb{T}^{d}$ . We have $\mathcal{M}\cong_{\sigma}^{n}\mathcal{M}_{|_{n}}^{\sigma}\leftrightarroweq% \mathcal{M}^{\prime}$ where $\mathcal{M}^{\sigma}$ is the $\sigma$ -reduct of $\mathcal{M}$ , and $\mathcal{M}^{\prime}\in\mathbb{T}^{d}$ is the bisimilarity quotient of its $n$ -prefix $\mathcal{M}_{|_{n}}^{\sigma}$ . By the assumption that $\varphi,\neg\varphi$ are not joint $\cong_{\sigma}^{n}$ -consistent, $\mathcal{M}\models\varphi$ implies $\mathcal{M}_{|_{n}}^{\sigma}\models\varphi$ . By invariance of $\varphi$ under $\leftrightarroweq$ , this in turn implies $\mathcal{M}^{\prime}\models\varphi$ . We construct $\mathcal{N}^{\prime}\models\neg\varphi$ symmetrically. By definition, $\mathcal{M}\leftrightarroweq_{\sigma}^{n}\mathcal{N}$ means that $\mathcal{M}_{|_{n}}^{\sigma}$ and $\mathcal{N}_{|_{n}}^{\sigma}$ are bisimilar, which is equivalent to saying that their bisimilarity quotients $\mathcal{M}^{\prime}$ and $\mathcal{N}^{\prime}$ are isomorphic, and hence $(\sigma,n)$ -isomorphic. Thus, $\mathcal{M}^{\prime},\mathcal{N}^{\prime}$ witness joint $\cong_{\sigma}^{n}$ -consistency of $\varphi,\neg\varphi$ over $\mathbb{T}^{d}$ , a contradiction. $\hfill\blacktriangleleft$

Using automata-based techniques we to decide if Item 2 in Lemma 6 holds for all $n$ .

Proposition 7.

For every parity automata $\mathcal{A},\mathcal{A}^{\prime}$ and $d\in\mathbb{N}$ : $\mathcal{A},\mathcal{A}^{\prime}$ are joint $\cong_{\sigma}^{n}$ -consistent over $\mathbb{T}^{d}$ for all $n\in\mathbb{N}$ iff $\mathcal{A},\mathcal{A}^{\prime}$ are joint $\cong_{\sigma}^{m}$ -consistent over $\mathbb{T}^{d}$ for $m=|\mathcal{A}|+|\mathcal{A}^{\prime}|+1$ . The latter condition can be checked in time polynomial in $|\mathcal{A}|+|\mathcal{A}^{\prime}|$ .

Proof (Sketch).

Due to well-known relativization techniques we do not loose generality by only running $\mathcal{A},\mathcal{A}^{\prime}$ on full $d$ -ary trees with no leaves. Let $L$ be a language of finite full $d$ -ary trees over $\sigma$ such that $\mathcal{M}\in L$ iff $\mathcal{M}$ is a prefix of a reduct of a model of $\mathcal{A}$ . Let $L^{\prime}$ be an analogous language for $\mathcal{A}^{\prime}$ . The tallness of a finite tree is the minimal distance from the root to a leaf. Observe that $\mathcal{A},\mathcal{A}^{\prime}$ are $\cong_{\sigma}^{n}$ -consistent over $\mathbb{T}^{d}$ iff $L\cap L^{\prime}$ contains a tree of tallness $n$ . Thus, it suffices to check if $L\cap L^{\prime}$ contains trees of arbitrarily high tallness. To that end construct an automaton $\mathcal{B}$ recognizing $L\cap L^{\prime}$ of size polynomial in $|\mathcal{A}|+|\mathcal{A}^{\prime}|$ . An easy pumping argument shows that the language $L\cap L^{\prime}$ of $\mathcal{B}$ contains trees of arbitrarily high tallness iff it contains a tree of tallness $m=|\mathcal{B}|+1$ . To test the latter condition it is enough to inductively compute a sequence $S_{1}\supseteq S_{2}\supseteq...\supseteq S_{|\mathcal{B}|+1}$ of subsets of states of $\mathcal{B}$ , where $S_{i}$ is the set of all states $q$ such that $\mathcal{B}[q_{I}\mapsfrom q]$ recognizes a tree of tallness at least $i$ . $\hfill\blacktriangleleft$

We are ready to solve $\mathsf{ML}$ -definability over $\mathbb{T}^{d}$ in exponential time. Assume $\mu\mathsf{ML}$ -formula $\varphi$ . For every $n$ , we know by Equivalence ( $\mathsf{Base}$ ) that $\varphi$ is equivalent over $\mathbb{T}^{d}$ to some $\psi\in\mathsf{ML}_{\sigma}^{n}$ iff $\varphi,\neg\varphi$ are not joint $\leftrightarroweq_{\sigma}^{n}$ -consistent over $\mathbb{T}^{d}$ . By Lemma 6 this is equivalent to the lack of joint $\cong_{\sigma}^{n}$ -consistency of $\varphi,\neg\varphi$ over $\mathbb{T}^{d}$ . By Theorem 2 we can compute exponentially-sized automata $\mathcal{A}$ , $\mathcal{A}^{\prime}$ equivalent to $\varphi$ and $\neg\varphi$ over $\mathbb{T}^{d}$ . It follows that $\varphi$ is not $\mathsf{ML}_{\sigma}$ -definable over $\mathbb{T}^{d}$ iff $\mathcal{A},\mathcal{A}^{\prime}$ are joint $\cong_{\sigma}^{n}$ -consistent over $\mathbb{T}^{d}$ for every $n$ . The last condition is decided using Proposition 7. The runtime of our algorithm is polynomial in $|\mathcal{A}|+|\mathcal{A}^{\prime}|$ , and thus exponential in $|\varphi|$ . This proves the part of Theorem 5 about $\mathbb{T}^{d}$ . The remaining part concerning unrestricted models is a special case of Theorem 9, which we will prove next.

Modal Separation: the Unrestricted Case

Over unrestricted models, separability turns out to be only slightly more complicated than definability. Lemma 6 becomes false if $\neg\varphi$ is replaced with arbitrary $\varphi^{\prime}$ (which would be the statement relevant for separability). We have the following lemma, however.

Lemma 8.

For every $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ and $n\in\mathbb{N}$ the following are equivalent:

1.

$\varphi,\varphi^{\prime}$ are joint $\leftrightarroweq_{\sigma}^{n}$ -consistent over all models.
2.

$\varphi,\varphi^{\prime}$ are joint $\cong_{\sigma}^{n}$ -consistent over $\mathbb{T}^{d}$ , where $d=|\varphi|+|\varphi^{\prime}|$ .

Proof.

The implication (1) $\Leftarrow$ (2) is immediate. To prove the other one (1) $\Rightarrow$ (2) consider an intermediate property:

\varphi,\varphi^{\prime}

are joint

\cong_{\sigma}^{n}

-consistent over all models.

(1.5)

The implication (1) $\Rightarrow$ (1.5) can be read off from Otto’s original proof. The remaining one (1.5) $\Rightarrow$ (2) is a special case of a stronger claim which we prove later: the implication (3) $\Rightarrow$ (4) of Lemma 27. $\hfill\blacktriangleleft$ Lemma 8 allows us to solve $\mathsf{ML}$ -separability in exponential time.

Theorem 9.

Over all models, $\mathsf{ML}$ -separability of $\mu\mathsf{ML}$ -formulae is ExpTime-complete.

Proof.

The proof is almost the same as our proof of Theorem 5. The only difference is that we consider an arbitrary $\varphi^{\prime}$ in place of $\neg\varphi$ , and hence use Lemma 8 in place of Lemma 6. $\hfill\blacktriangleleft$ Apart from deciding separability we also construct separators when they exists. Given a subset $\mathcal{L}$ of $\mu\mathsf{ML}$ formulae, $\varphi\in\mu\mathsf{ML}$ , and $\psi\in\mathcal{L}$ , we call $\psi$ an $\mathcal{L}$ -uniform consequence of $\varphi$ if $\psi\models\theta$ for every $\theta\in\mathcal{L}$ such that $\varphi\models\theta$ . The notion relativizes to a fixed class $\mathbf{C}$ of models by only considering entailment over that class. Observe that if $\varphi,\varphi^{\prime}$ are $\mathcal{L}$ -separable and $\psi$ is an $\mathcal{L}$ -uniform consequence of $\varphi$ then $\psi$ is an $\mathcal{L}$ -separator for $\varphi,\varphi^{\prime}$ . The same is true over any class $\mathbf{C}$ .

Note that it follows from the proof of Theorem 9 that if $\varphi,\varphi^{\prime}$ are $\mathsf{ML}$ -separable then they admit a separator of modal depth $n$ at most exponential in $|\varphi|+|\varphi^{\prime}|$ . It follows that constructing an $\mathsf{ML}_{\sigma}$ -separator for $\varphi,\varphi^{\prime}$ boils down to constructing an $\mathsf{ML}_{\sigma}^{n}$ -uniform consequence of $\varphi$ . A naive construction which always works is to take the disjunction of all $\mathsf{ML}_{\sigma}^{n}$ -types consistent with $\varphi$ over $\mathbf{C}$ . Here, by an $\mathsf{ML}_{\sigma}^{n}$ -type we mean a maximal consistent subset of $\mathsf{ML}_{\sigma}^{n}$ . Since up to equivalence there are only finitely many formulae in $\mathsf{ML}_{\sigma}^{n}$ , each $\mathsf{ML}_{\sigma}^{n}$ -type can be represented as a single $\mathsf{ML}_{\sigma}^{n}$ -formula and the mentioned disjunction $\psi$ is well-defined. This construction is non-elementary in $n$ over all models and doubly exponential in $n$ over models of bounded outdegree.

We present an efficient construction of $\mathsf{ML}_{\sigma}^{n}$ -uniform consequences. The construction works over unrestricted models, over $\mathbb{T}^{1}$ and over $\mathbb{T}^{2}$ but not over $\mathbb{T}^{d}$ for $d\geq 3$ . Since in the following Section 4 we will provide a more efficient construction for $\mathbb{T}^{1}$ , now we only look at the unrestricted and binary case. For convenience, we construct $\mathsf{ML}_{\sigma}^{n}$ -uniform consequences of automata instead of formulae, with definition adapted in an obvious way.

Proposition 10.

Let $\mathbf{C}$ be the class of all models or $\mathbb{T}^{2}$ . Assume an NPTA $\mathcal{A}$ over $\mathbf{C}$ , a signature $\sigma$ and $n\in\mathbb{N}$ . An $\mathsf{ML}_{\sigma}^{n}$ -uniform consequence of $\mathcal{A}$ over $\mathbf{C}$ can be constructed in time $|A|^{O(n\cdot|\mathcal{A}|)}$ if $\mathbf{C}$ is the class of all models and in time $2^{O(n\cdot|A|)}$ if $\mathbf{C}=\mathbb{T}^{2}$ .

Proof.

Let $\mathcal{A}$ be an NPTA. Let $\mathcal{B}=(Q,\Sigma,q_{I},\delta,\mathsf{rank})$ be an automaton of the same size recognizing $\sigma$ -reducts of models of $\mathcal{A}$ . A formula $\psi$ is an $\mathsf{ML}_{\sigma}^{n}$ -uniform consequence of $\mathcal{A}$ over $\mathbf{C}$ iff it is an $\mathsf{ML}^{n}$ -uniform consequence of $\mathcal{B}$ over $\mathbf{C}$ . Thus, it suffices to construct the latter.

We construct $\psi_{n,q}$ for every $q\in Q$ and $n\in\mathbb{N}$ 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}\in\mathbf{C}$ % with $\mathcal{N}\models\mathcal{B}[q_{I}\mapsfrom q]$ and $\mathcal{N}\models c% $}\}

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\}

where $\nabla\Phi$ is an abbreviation for $\bigwedge_{\theta\in\Phi}\Diamond\theta\wedge\Box\bigvee_{\theta\in\Phi}\theta$ . Assume $\mathbf{C}$ is either the class of all models or $\mathbb{T}^{2}$ . The construction preserves the following invariant:

\displaystyle\mathcal{M}\models\psi_{n,q}\text{\hskip 14.22636pt $\iff$ \hskip 1% 4.22636pt there exists $\mathcal{N}\in\mathbf{C}$ with $\mathcal{N}\models% \mathcal{B}[q_{I}\mapsfrom q]$ and $\mathcal{M}\leftrightarroweq^{n}\mathcal{N% }$}

(1)

for every structure $\mathcal{M}\in\mathbf{C}$ . Hence, $\psi_{n,q_{I}}$ is an $\mathsf{ML}_{\sigma}^{n}$ -uniform consequence of $\mathcal{A}$ over $\mathbf{C}$ . It is routine to check that in either case the formula has the right size.

The proof of (1) proceeds by an easy induction, with slightly different details for the cases of binary and of unrestricted models. It is worth to point out, however, that the implication $\Rightarrow$ from left to right would not be valid over $\mathbb{T}^{d}$ with $d\geq 3$ . $\hfill\blacktriangleleft$

Given the exponential construction of automata from Theorem 2 and the exponential upper bound on modal depth $n$ of separators, Proposition 10 yields an efficient construction of separators.

Theorem 11.

If $\varphi,\varphi^{\prime}$ are $\mathsf{ML}_{\sigma}$ -separable, then one can compute an $\mathsf{ML}_{\sigma}$ -separator in time doubly exponential in $|\varphi|+|\varphi^{\prime}|$ .

It is not difficult to show that, in the presence of at least two accessibility relations $\Diamond_{1},\Diamond_{2}$ , the construction is optimal: one can express in $\mu\mathsf{ML}$ that the model embeds a full binary tree of depth $2^{n}$ and in which each inner node has both a $\Diamond_{1}$ - and a $\Diamond_{2}$ -successor. Using standard techniques, one can show that any modal formula expressing this property is of doubly exponential size [13]. Whether having two accessibility relations is necessary for this lower bound is an interesting question which we leave open.

It is interesting to note that the separators we compute are not the logically strongest separators and, in fact, strongest separators do not even have to exist.

Example 12.

Consider $\varphi=\theta_{\infty}$ from before and $\varphi=\Box\bot$ For every $n\in\mathbb{N}$ , the modal formula $\Diamond^{n}\top$ separates $\varphi$ from $\varphi^{\prime}$ , and $\Diamond^{m}\top\models\Diamond^{n}\top$ whenever $m\geq n$ .

The remaining open cases are the problems of $\mathsf{ML}$ -separability (and separator construction) over $\mathbb{T}^{d}$ for $d\geq 1$ . We investigate the cases of unary ( $d=1$ ), binary ( $d=2$ ), and higher maximal outdegree ( $d\geq 3$ ) in turn. We emphasize that the outdegree $d$ is not a part of the input but rather a property of the considered class of models.

4 Unary Case

We first investigate $\mathsf{ML}$ -separability over $\mathbb{T}^{1}$ , that is, models that are essentially words. Note that satisfiability of $\mu\mathsf{ML}$ over words is PSpace-complete (an upper bound follows, e.g., via the translation to automata and the lower bound is inherited from $\mathsf{LTL}$ [30, Theorem 4.1]) which suggests that also definability and separability could be easier. Indeed, we show:

Theorem 13.

$\mathsf{ML}$ -definability and $\mathsf{ML}$ -separability of $\mu\mathsf{ML}$ -formulae is PSpace-complete over $\mathbb{T}^{1}$ .

Proof.

The lower bound is by a reduction from satisfiability, and applies to definability.

Given formulae $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ and a subset of the signature $\sigma$ , consider the set of finite words $L=\{W\in\mathcal{P}(\sigma)^{*}\ |\ \text{ $W$ is a $\sigma$-reduct of a % prefix $V$ of some model $U$ of $\varphi$}\}$ . Let $L^{\prime}$ be a similar language defined for $\varphi^{\prime}$ . Two unary models are bisimilar iff they are identical. Hence, by Equivalence ( $\mathsf{Base}$ ) the formulae $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ are not $\mathsf{ML}_{\sigma}$ -separable over $\mathbb{T}^{1}$ iff $L\cap L^{\prime}$ is infinite. It is standard to define a finite automaton $\mathcal{A}$ recognizing $L\cap L^{\prime}$ and check if its language is infinite (which is equivalent to checking if $L\cap L^{\prime}$ contains input longer than $|\mathcal{A}|$ ). To do it in polynomial space, we nondeterministically guess the long input, letter by letter, and only remember the current state and a binary counter measuring the length of the input guessed so far. $\hfill\blacktriangleleft$

We conclude this section with proving that $\mathsf{ML}_{\sigma}$ -separators can be constructed in exponential time and are thus of at most exponential size. Note that this is optimal, since over $\mathbb{T}^{1}$ , $\mu\mathsf{ML}$ is exponentially more succinct than $\mathsf{ML}$ . Indeed, it is standard to implement an exponential counter using a polynomially sized $\mu\mathsf{ML}$ -formula.

Theorem 14.

If $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ are $\mathsf{ML}_{\sigma}$ -separable over $\mathbb{T}^{1}$ , then one can compute an $\mathsf{ML}_{\sigma}$ -separator in time exponential in $|\varphi|+|\varphi^{\prime}|$ .

As argued in the previous section, it suffices to construct an $\mathsf{ML}^{n}$ -uniform consequence of the NPTA equivalent to $\varphi$ , which we do next.

Proposition 15.

Let $\mathcal{A}$ be an NPTA over $\mathbb{T}^{1}$ with $\ell$ states, $n\in\mathbb{N}$ , and $\sigma$ a signature. An $\mathsf{ML}_{\sigma}^{n}$ -uniform consequence of $\mathcal{A}$ over $\mathbb{T}^{1}$ can be constructed in time polynomial in $n$ , $\sigma$ , and $\ell$ .

Proof.

As argued in the previous section, it suffices to construct an $\mathsf{ML}^{n}$ -uniform consequence of the NPTA $\mathcal{B}$ which recognizes precisely the $\sigma$ -reducts of models of $\mathcal{A}$ . Let $\mathcal{B}$ have states $Q$ . By construction of $\mathcal{B}$ , we have $|Q|=\ell$ . As an auxiliary step, we define for every $p,q\in Q$ and $m\leq n$ a formula $\psi_{p,q}^{m}\in\mathsf{ML}_{\sigma}^{n}$ such that for every $\mathcal{M}\in\mathbb{T}^{1}$ :

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

(2)

The $\psi_{pq}^{m}$ are defined inductively with the base cases ( $m\leq 1$ ) read off from $\mathcal{B}$ , and using divide and conquer in the inductive step ( $m>1$ ), to keep the formulae small. More formally, we define $\psi_{pq}^{m}$ for $m>1$ and all $p,q\in Q$ by taking:

\displaystyle\psi^{m}_{pq}

\displaystyle=\bigvee_{q^{\prime}\in Q}\big{(}\psi^{\lfloor m/2\rfloor}_{pq^{% \prime}}\wedge\Diamond^{\lfloor m/2\rfloor}\psi^{\lceil m/2\rceil}_{q^{\prime}% q}\big{)}

It is routine to verify that $\psi^{m}_{pq}$ satisfies (2) and is of size $|\psi^{m}_{pq}|\in O(|Q|\cdot m^{2})$ . Based on the $\psi^{m}_{pq}$ , one can define a formula $\psi_{n}$ that describes all possible prefixes of length $\leq n$ of models of $\mathcal{B}$ , and thus is the sought $\mathsf{ML}_{\sigma}$ -uniform consequence of $\mathcal{B}$ . One can think of $\psi_{n}$ as the disjunction of formulae $\psi^{n}_{q_{0}q}$ for $q_{0}$ the initial state of $\mathcal{B}$ , but the full construction is slightly more involved since models accepted by $\mathcal{B}$ might be also shorter than $n$ . $\hfill\blacktriangleleft$

5 Binary Case

We next handle the binary case $\mathbb{T}^{2}$ . The key observation here is that, between full binary trees, bisimilarity entails isomorphism.

Proposition 16.

Assume full binary trees $\mathcal{M},\mathcal{M}^{\prime}\in\mathbb{T}^{2}$ . If $\mathcal{M}$ and $\mathcal{M}^{\prime}$ are $\sigma$ -bisimilar then they are $\sigma$ -isomorphic.

Proof.

By definition a $\sigma$ -bisimulation between two models is a bisimulation between their reducts to $\sigma$ , and $\sigma$ -isomorphism is such a bisimulation which is additionally bijective. It therefore suffices to show that if $\mathcal{M},\mathcal{M}^{\prime}$ are full binary trees and $Z$ is a bisimulation between them then there is a bijective bisimulation $Z^{\prime}\subseteq Z$ . We pick such $Z^{\prime}$ inductively starting with the pair of roots $(v_{I},v_{I}^{\prime})$ . The key observation is that if $v$ has children $v_{1},v_{2}$ and $w$ has children $w_{1},w_{2}$ and $v Z w$ then either (i) $v_{1}Zw_{1}$ and $v_{2}Zw_{2}$ or (ii) $v_{1}Zw_{2}$ and $v_{2}Zw_{1}$ (the cases are not exclusive). $\hfill\blacktriangleleft$ Proposition 16 can be used to prove the Craig interpolation property of $\mathsf{ML}$ over $\mathbb{T}^{2}$ and implies the following separability-variant of Lemma 6 over $\mathbb{T}^{2}$ .

Lemma 17.

For every $\varphi,\varphi^{\prime}\in\mu\mathsf{ML}$ and $n\in\mathbb{N}$ the following are equivalent:

1.

$\varphi,\varphi^{\prime}$ are joint $\leftrightarroweq_{\sigma}^{n}$ -consistent over $\mathbb{T}^{2}$ .
2.

$\varphi,\varphi^{\prime}$ are joint $\cong_{\sigma}^{n}$ -consistent over $\mathbb{T}^{2}$ .

Proof.

We show only the nontrivial implication 1 $\Rightarrow$ 2. Assume binary $\mathcal{M}\models\varphi$ , $\mathcal{M}^{\prime}\models\varphi^{\prime}$ with $\mathcal{M}\leftrightarroweq_{\sigma}^{n}\mathcal{M}^{\prime}$ . Let $\mathcal{N}\models\varphi$ and $\mathcal{N}^{\prime}\models\varphi^{\prime}$ be full binary trees obtained from $\mathcal{M}$ and $\mathcal{M}^{\prime}$ by duplicating subtrees. By Proposition 16, $\mathcal{N}\cong_{\sigma}^{n}\mathcal{N}^{\prime}$ which proves 2. $\hfill\blacktriangleleft$ Similarly to the definability case, Lemma 17 combined with Equivalence ( $\mathsf{Base}$ ) and Proposition 7 immediately give an exponential procedure for separability. Since the lower bound is inherited from definability, we get the following result.

Theorem 18.

$\mathsf{ML}$ -separability and $\mathsf{ML}$ -definability of $\mu\mathsf{ML}$ -formulae is ExpTime-complete over $\mathbb{T}^{2}$ .

With the same argument as for Theorem 11 we use Proposition 10 to conclude:

Theorem 19.

If $\varphi,\varphi^{\prime}$ are $\mathsf{ML}_{\sigma}$ -separable over $\mathbb{T}^{2}$ , then one can compute an $\mathsf{ML}_{\sigma}$ -separator in time doubly exponential in $|\varphi|+|\varphi^{\prime}|$ .

6 Ternary and Beyond

In this section we address the case of models with outdegree bounded by a number $d\geq 3$ . We illustrate that this case behaves differently as it lacks the Craig interpolation property.

Example 20.

Consider $\mathsf{ML}$ -formulae $\varphi=\Diamond(a\wedge b)\wedge\Diamond(a\wedge\neg b)$ and $\varphi^{\prime}=\Diamond(\neg a\wedge c)\wedge\Diamond(\neg a\wedge\neg c)$ . Clearly, $\varphi\models\neg\varphi^{\prime}$ over $\mathbb{T}^{3}$ . Observe that models $\mathcal{M},\mathcal{M}^{\prime}$ in Figure 1 witness that $\varphi,\varphi^{\prime}$ are joint $\leftrightarroweq_{\{a\}}$ -consistent and thus joint $\leftrightarroweq_{\{a\}}^{n}$ -consistent for every $n\in\mathbb{N}$ . By Equivalence ( $\mathsf{Base}$ ) there is no $\mathsf{ML}_{\{a\}}$ -separator, which is nothing else than a Craig interpolant. ∎

Figure 1: Witness of joint consistency: dashed lines and colors indicate the

\{a\}

-bisimulation.

Motivated by the lack of the Craig interpolation property, we study the $\mathsf{ML}$ -interpolant existence problem: given $\varphi,\varphi^{\prime}\in\mathsf{ML}$ and signature $\sigma$ , decide whether there is an $\mathsf{ML}_{\sigma}$ -separator of $\varphi,\neg\varphi^{\prime}$ , that is, $\psi\in\mathsf{ML}_{\sigma}$ with $\varphi\models\psi\models\varphi^{\prime}$ . Craig $\mathsf{ML}$ -interpolant existence is the special case in which $\sigma=\text{sig}(\varphi)\cap\text{sig}(\varphi^{\prime})$ . Observe that $\mathsf{ML}$ -interpolant existence is the special case of $\mathsf{ML}$ -separability of $\mu\mathsf{ML}$ -formulae in which the input to the separability is restricted to $\mathsf{ML}$ -formulae. We show that already $\mathsf{ML}$ -interpolant existence over $\mathbb{T}^{3}$ is harder than $\mathsf{ML}$ -separability of $\mu\mathsf{ML}$ -formulae over arbitrary models.

Theorem 21.

For $d\geq 3$ , $\mathsf{ML}$ -interpolant existence over $\mathbb{T}^{d}$ is coNExpTime-complete. Hardness already applies to Craig $\mathsf{ML}$ -interpolant existence over $\mathbb{T}^{d}$ .

Proof.

The upper bound is easy to establish based on the observation that $\varphi,\neg\varphi^{\prime}$ of modal depth at most $m$ do not admit an $\mathsf{ML}_{\sigma}$ -separator over $\mathbb{T}^{d}$ iff they are joint $\leftrightarroweq_{\sigma}^{m}$ -consistent over $\mathbb{T}^{d}$ . The witness $\mathcal{M},\mathcal{M}^{\prime}$ of joint $\leftrightarroweq_{\sigma}^{m}$ -consistency of $\varphi,\neg\varphi^{\prime}$ can assumed to be of depth $m$ . Such models are of exponential size (they have at most $d^{m}$ points) and can thus be guessed by a non-deterministic exponential time bounded Turing machine.

The lower bound is more intriguing and relies on an extension of Example 20. Reconsidering the example it is important to note that in every witness $\mathcal{M},\mathcal{M}^{\prime}$ of joint $\leftrightarroweq_{\{a\}}^{n}$ -consistency of $\varphi,\varphi^{\prime}$ , there are two successors of $v_{I}$ that are bisimilar to the same successor of $v_{I}^{\prime}$ . We extend the idea and enforce exponentially many bisimilar points. More precisely, consider families $(\psi_{i})_{i\in\mathbb{N}}$ , $(\psi_{i}^{\prime})_{i\in\mathbb{N}}$ of modal formulae inductively defined as follows:

	$\displaystyle\psi_{0}$	$\displaystyle=\psi_{0}^{\prime}=\top$
	$\displaystyle\psi_{i+1}$	$\displaystyle=\Diamond(a\wedge b_{i})\wedge\Diamond(a\wedge\neg b_{i})\wedge% \Box\big{(}a\to(\psi_{i}\wedge(b_{i}\to\textstyle\bigwedge_{j<i}\Box^{j}b_{i})% \wedge(\neg b_{i}\to\textstyle\bigwedge_{j<i}\Box^{j}\neg b_{i}))\big{)}$
	$\displaystyle\psi_{i+1}^{\prime}$	$\displaystyle=\Diamond(\neg a\wedge c)\wedge\Diamond(\neg a\wedge\neg c)\wedge% \Diamond(a\wedge\psi_{i}^{\prime})$

Clearly, the size of $\psi_{i},\psi^{\prime}_{i}$ is polynomial in $i$ . Moreover, by induction on $i$ , it is readily verified that for every $i\in\mathbb{N}$ , for every $\mathcal{M},\mathcal{M}^{\prime}\in\mathbb{T}^{3}$ with $\mathcal{M}\models\psi_{i}$ , $\mathcal{M}\models\psi_{i}^{\prime}$ , and every $(\{a\},i)$ -bisimulation $S$ witnessing $\mathcal{M}\leftrightarroweq^{i}_{\{a\}}\mathcal{M}^{\prime}$ , there are points $w_{0},\ldots,w_{2^{i}-1}$ in depth $i$ in $\mathcal{M}$ and a point $\widehat{w}$ in depth $i$ in $\mathcal{M}^{\prime}$ such that $(w_{j},\widehat{w})\in S$ for all $j$ and such that distinct $w_{j},w_{k}$ can be distinguished by some proposition in $b_{0},\ldots,b_{i-1}$ . Intuitively, this means that $\psi_{i},\psi_{i}^{\prime}$ enforce in joint $\leftrightarroweq_{\{a\}}^{i}$ -consistent models $\mathcal{M},\mathcal{M}^{\prime}$ that $\mathcal{M}$ contains $2^{i}$ points $w_{0},\ldots,w_{2^{i}-1}$ which are all linked to the same point $\widehat{w}$ in $\mathcal{M}^{\prime}$ . We exploit this link to synchronize information between the $w_{j}$ , following a strategy that has recently been used to show coNExpTime-hardness for interpolant existence in some description logics [1].

We reduce a NExpTime-complete tiling problem [14]: Given a set $\Delta$ of tile types and horizontal and vertical compatibility relations $H,V\subseteq\Delta\times\Delta$ , and some $n\in\mathbb{N}$ in unary, decide whether one can tile the $2^{n}\times 2^{n}$ torus with tiles from $\Delta$ complying with $H, V$ . Given $\Delta,H,V,n$ , we define formulae $\varphi_{n}=\psi_{2n}\wedge\Box^{2n}\chi_{n}$ , $\varphi_{n}^{\prime}=\psi_{2n}^{\prime}\wedge\Box^{2n}\chi_{n}^{\prime}$ of modal depth $m$ and with common signature $\sigma=\text{sig}(\varphi_{n})\cap\text{sig}(\varphi^{\prime}_{n})$ such that

\Delta,H,V,n

has a solution

\Leftrightarrow

\varphi_{n},\varphi_{n}^{\prime}

are joint

\leftrightarroweq_{\sigma}^{m}

-consistent.

To explain the idea, let $\mathcal{M},\mathcal{M}^{\prime}$ witness joint $\leftrightarroweq_{\sigma}^{m}$ -consistency of $\varphi_{n},\varphi_{n}^{\prime}$ . The gadget formulae $\psi_{2n},\psi_{2n}^{\prime}$ enforce $2^{2n}$ points $w_{0},\ldots,w_{2^{2n}-1}$ in depth $2n$ in $\mathcal{M}$ which are all linked via the bisimulation to a single point $\widehat{w}$ in $\mathcal{M}^{\prime}$ . These $2^{2n}$ points shall represent the $2^{n}\times 2^{n}$ cells of the torus. The intended solution of the tiling problem is represented via propositions $p_{d}\in\sigma$ , for each $d\in\Delta$ . To synchronize them we proceed as follows. Using the $2n$ propositions $b_{0},\ldots,b_{2n-1}$ (which are not in $\sigma$ ), we can associate coordinates $(x_{i},y_{i})\in\{0,\ldots,2^{n}-1\}\times\{0,\ldots,2^{n}-1\}$ to each point $w_{i}$ in the torus. To understand the purpose of $\chi_{n},\chi_{n}^{\prime}$ , suppose for a moment that the outdegree of the points $\widehat{w}$ and the $w_{i}$ is at most $2^{2n}$ (instead of 3). Then we could proceed by enforcing (via $\chi_{n}$ ) below each $w_{i}$ with coordinates $(x_{i},y_{i})$ three successors $v_{i}^{1},v_{i}^{2},v_{i}^{3}$ such that

$\blacksquare$

$v_{i}^{1}$ , $v_{i}^{2}$ , $v_{i}^{3}$ have coordinates $(x_{i},y_{i})$ , $(x_{i},y_{i}+1)$ , and $(x_{i}+1,y_{i})$ , respectively;
$\blacksquare$

the coordinates of the $v_{i}^{j}$ are made visible using propositions in $\sigma$ ;
$\blacksquare$

$v_{i}^{1},v_{i}^{2},v_{i}^{3}$ satisfy $p_{d_{1}},p_{d_{2}},p_{d_{3}}$ for $d_{1},d_{2},d_{3}\in\Delta$ such that $(d_{1},d_{2})\in V$ and $(d_{1},d_{3})\in H$ .

These three successors stipulate bisimilar successors of $\widehat{w}$ . Since each point in the torus is stipulated three times as successor of some $w_{i}$ and since the outdegree of $\widehat{w}$ is restricted to $2^{2n}$ , the three copies of the same point satisfy the same proposition $p_{d}$ . By the last item above, the selected propositions comply with $V, H$ and thus represent a solution to the tiling problem. Now, since the outdegree below $\widehat{w}$ is at most 3 (and not $2^{2n}$ as assumed), the $\chi_{n},\chi_{n}^{\prime}$ have to be a bit more complicated, but the idea remains the same. $\hfill\blacktriangleleft$

We show next that the situation for the full separability problem is even worse.

Theorem 22.

For every $d\geq 3$ , $\mathsf{ML}$ -separability of $\mu\mathsf{ML}$ -formulae over $\mathbb{T}^{d}$ is 2-ExpTime-complete.

Thus, over $\mathbb{T}^{d}$ for $d\geq 3$ , $\mathsf{ML}$ -separability is provably harder than $\mathsf{ML}$ -definability, c.f. Theorem 5. Both the upper and the lower bound of Theorem 22 are non-trivial; we provide proof sketches in the following two subsections. Before doing that let us conclude this part with separator construction.

Theorem 23.

If $\varphi,\varphi^{\prime}$ are $\mathsf{ML}_{\sigma}$ -separable over $\mathbb{T}^{d}$ , $d\geq 3$ , then one can compute an $\mathsf{ML}_{\sigma}$ -separator in time triply exponential in $|\varphi|+|\varphi^{\prime}|$ .

Proof.

(Sketch) It follows from the upper bound proof of Theorem 22 that, if $\varphi,\varphi^{\prime}$ admit an $\mathsf{ML}_{\sigma}$ -separator, then they admit one of modal depth bounded doubly exponentially in $|\varphi|+|\varphi^{\prime}|$ . Observe that over the signature of $\varphi$ and $\varphi^{\prime}$ there are only triple exponentially many trees of fixed outdegree $d$ and double exponential depth, and that each such tree is characterized by a modal formula of triply exponential size. The sought separator is then the disjunction of all such formulae consistent with $\varphi$ . $\hfill\blacktriangleleft$

6.1 Lower Bound for Theorem 22

We reduce the word problem of exponentially space bounded alternating Turing machines (ATMs), which is known to be 2-ExpTime-complete [8]. Informally, the states of such ATMs are partitioned into universal states $Q_{\forall}$ and existential states $Q_{\exists}$ . Configurations of ATMs are defined as usual, but computations are not sequences of configurations but trees of configurations such that an existential configuration has exactly one successor labeled with a universal configuration and a universal configuration has exactly two successors labeled with existential configurations. A computation tree for an input $w$ is a tree whose root is labeled with the initial configuration and such that successor nodes contain successor configurations. $w$ is accepted if there is a computation tree in which each path is infinite (this acceptance condition is slightly non-standard, but eases the proof).

The reduction relies on the same gadget formulae $(\psi_{i})_{i\in\mathbb{N}},(\psi^{\prime}_{i})_{i\in\mathbb{N}}$ as used in the proof of Theorem 21 and additionally uses ideas for showing 2-ExpTime-hardness for recently studied interpolant existence problems for description logics [1]. For a given ATM $\mathfrak{A}$ and input $w$ of length $n$ , we construct formulae $\varphi_{n}=\psi_{n}\wedge\Box^{n}\chi,\varphi^{\prime}_{n}=\psi_{n}^{\prime}% \wedge\chi^{\prime}$ such that

\varphi_{n},\varphi^{\prime}_{n}

are joint

\leftrightarroweq^{m}_{\sigma}

-consistent for every

m\in\mathbb{N}

iff

\mathfrak{A}

accepts

w

.

This suffices by Equivalence ( $\mathsf{Base}$ ). The signature $\sigma$ will consist of $a$ , $z$ , and propositions $c_{\alpha}$ for every possible cell content $\alpha$ of $\mathfrak{A}$ , that is, $\alpha\in\Gamma\cup(Q\times\Gamma)$ . Additionally, $\varphi_{n}$ and $\varphi^{\prime}_{n}$ will use auxiliary propositions, e.g., to encode counters. The only purpose of $\chi^{\prime}$ is to mention the propositions in $\sigma$ ; the main work is done by $\psi_{n},\psi_{n}^{\prime},\chi$ .

Figure 2: Computation tree of

\mathfrak{A}

below some

w_{i}

(drawn horizontally for space constraints).

To explain the idea, let us consider witnesses $\mathcal{M},\mathcal{M}^{\prime}$ for joint $\leftrightarroweq^{m}_{\sigma}$ -consistency of $\varphi_{n},\varphi_{n}^{\prime}$ for sufficiently large $m$ . By the properties of $\psi_{n},\psi_{n}^{\prime}$ , we find $2^{n}$ points $w_{0},\ldots,w_{2^{n}-1}$ in depth $n$ in $\mathcal{M}$ which are bisimilar to a single point $\widehat{w}$ in depth $n$ in $\mathcal{M}^{\prime}$ . Recall that in every $w_{i}$ , we have access to its index $i$ via a counter using propositions $b_{0},\ldots,b_{n}$ . Now, $\chi$ is a $\mu\mathsf{ML}$ -formula with the following properties, see also Figure 2 for illustration.

$\blacksquare$

$\chi$ enforces the “skeleton” of a computation tree for $\mathfrak{A}$ , in which each configuration is modeled by a path of length $2^{n}$ (using an exponential counter), and in which universal and existential configurations alternate.
$\blacksquare$

$\chi$ also enforces that each point of the skeleton is labeled with some cell content via $\sigma$ -propositions $c_{\alpha}$ , but without any synchronization except the initial configuration.
$\blacksquare$

$\chi$ makes sure that below $w_{i}$ the positions $2^{n}-i$ of successor configurations are coordinated.

The key point is that this enforces (due to bisimilarity) a computation tree below $\widehat{w}$ in which, due to the last item above, all positions of configurations are coordinated.

We remark that the hardness also holds when $\sigma$ is not part of the input: one can reduce separability of $\varphi,\varphi^{\prime}$ by $\mathsf{ML}_{\sigma}$ -formulae to separability of $\varphi,\varphi^{\prime}$ by (arbitrary) $\mathsf{ML}$ -formulae.

6.2 Upper Bound for Theorem 22

We show that over models of outdegree at most $d$ , $\mathsf{ML}$ -separability of fixpoint formulae can be solved in doubly exponential time. Let us start with establishing a technical but useful fact. For every language of $d$ -ary trees $L\subseteq\mathbb{T}^{d}$ denote the language:

\mathsf{bisQuot}(L)=\{\mathcal{M}\in\mathbb{T}^{d}\ |\ \text{there is $% \mathcal{N}\in L$ and a functional bisimulation $Z:\mathcal{N}\stackrel{{% \scriptstyle\mathsf{bis}}}{{\to}}{}\mathcal{M}$}\}

of bisimulation quotients of trees from $L$ .

Proposition 24.

For every NPTA $\mathcal{A}$ , an NPTA $\mathcal{B}$ recognizing $\mathsf{bisQuot}(\mathcal{L}(\mathcal{A}))$ can be computed in time exponential in the size of $\mathcal{A}$ .

Proof.

Fix an NPTA $\mathcal{A}=(Q,\Sigma,q_{I},\delta,\mathsf{rank})$ . For every $\mathcal{M}\in\mathbb{T}^{d}$ , we characterize existence of $d$ -ary $\mathcal{N}\models\mathcal{A}$ with $\mathcal{N}\stackrel{{\scriptstyle\mathsf{bis}}}{{\to}}{}\mathcal{M}$ with the following parity game $\mathcal{G}_{\mathsf{bisQuot}}(\mathcal{M},\mathcal{A})$ . The game has the set $M\times Q$ as positions. The pair $(v_{I},q_{I})$ consisting of the root $v_{I}$ of $\mathcal{M}$ and $q_{I}$ is the initial position. From a position $(v,q)$ first $\exists\text{ve}$ chooses $S\in\delta(q,\mathsf{val}(c))$ and a surjective map $h:S\to\{v_{1},...,v_{k}\}$ where $\{v_{1},...,v_{k}\}$ is the set of children of $v$ . Then $\forall\text{dam}$ responds with a choice of $p\in S$ and the next round starts in position $(h(p),p)$ . The game is a parity game: the ranks are inherited from $\mathcal{A}$ in the sense that the rank of $(v,q)$ equals $\mathsf{rank}(q)$ . It is easy to show that:

\displaystyle\text{$\exists\text{ve}$ wins $\mathcal{G}_{\mathsf{bisQuot}}(% \mathcal{M},\mathcal{A})$}\iff\mathcal{M}\in\mathsf{bisQuot}(\mathcal{L}(% \mathcal{A}))

(3)

for every $\mathcal{M}\in\mathbb{T}^{d}$ . Using (3) we prove Proposition 24. It suffices to construct an automaton $\mathcal{B}$ which accepts $\mathcal{M}$ iff $\exists\text{ve}$ wins $\mathcal{G}_{\mathsf{bisQuot}}(\mathcal{M},\mathcal{A})$ . To that end, using standard techniques we encode $\exists\text{ve}$ ’s positional strategies for $\mathcal{G}_{\mathsf{bisQuot}}(\mathcal{M},\mathcal{A})$ as colorings of $\mathcal{M}$ with $\mathcal{P}(Q\times Q)$ and construct, in time exponential in $|Q|$ , an automaton $\mathcal{B}^{+}$ recognizing models labelled with such winning positional strategies. We then obtain $\mathcal{B}$ recognizing $\mathsf{bisQuot}(\mathcal{L}(\mathcal{A}))$ by projecting out the additional colors $\mathcal{P}(Q\times Q)$ from $\mathcal{B}^{+}$ . $\hfill\blacktriangleleft$

With the help of Proposition 24 we prove Theorem 22. Fix $d$ , $\mu\mathsf{ML}$ -formulae $\varphi$ and $\varphi^{\prime}$ and signature $\sigma$ . By Equivalence ( $\mathsf{Base}$ ), it suffices to check if $\varphi$ and $\varphi^{\prime}$ are jointly $\leftrightarroweq_{\sigma}^{n}$ -consistent over $\mathbb{T}^{d}$ for every $n$ . However, unlike with definability or in the binary case, we cannot conclude joint $\cong_{\sigma}^{n}$ -consistency from joint $\leftrightarroweq_{\sigma}^{n}$ -consistency. Instead, we use Proposition 24 to directly decide joint $\leftrightarroweq_{\sigma}^{n}$ -consistency for all $n$ . For a language $L\subseteq\mathbb{T}^{d}$ , define the language:

\mathsf{QPL}(L)=\{\mathcal{N}\in\mathbb{T}^{d}\ |\ \text{there is $\mathcal{M}% \in L$, finite prefix $\mathcal{M}_{0}$ of $\mathcal{M}$ and $Z:\mathcal{M}_{0% }\stackrel{{\scriptstyle\mathsf{bis}}}{{\to}}\mathcal{N}$}\}

of finite $d$ -ary trees which are bisimulation quotients of finite prefixes of models from $L$ . By Proposition 24 and the closure properties of parity automata, for every $\mathcal{A}$ one can construct in exponential time an automaton $\mathcal{B}$ recognizing $\mathsf{QPL}(\mathcal{L}(\mathcal{A}))$ .

We prove the upper bound from Theorem 22. Using Theorem 2 compute automata $\mathcal{A},\mathcal{A}^{\prime}$ accepting $\sigma$ -reducts of models of $\varphi,\varphi^{\prime}$ . Compute $\mathcal{B},\mathcal{B}^{\prime}$ recognizing $\mathsf{QPL}(\mathcal{L}(\mathcal{A}))$ and $\mathsf{QPL}(\mathcal{L}(\mathcal{A}^{\prime}))$ . Recall that any two trees are bisimilar iff they have isomorphic bisimulation quotients. It follows that $\varphi,\varphi^{\prime}$ admit a $\mathsf{ML}_{\sigma}^{n}$ -separator over $\mathbb{T}^{d}$ iff $\mathcal{A},\mathcal{A}^{\prime}$ are joint $\leftrightarroweq^{n}$ -consistent iff $\mathcal{B},\mathcal{B}^{\prime}$ are joint $\cong^{n}$ consistent. By Proposition 7, the latter condition holds for all $n\in\mathbb{N}$ iff it holds for $n=|\mathcal{B}|+|\mathcal{B}^{\prime}|+1$ and this can be tested in time polynomial in $|\mathcal{B}|+|\mathcal{B}^{\prime}|$ . Since $\mathcal{A},\mathcal{A}^{\prime}$ are exponential, and $\mathcal{B},\mathcal{B}^{\prime}$ are doubly exponential in the size of $\varphi,\varphi^{\prime}$ , this gives the upper bound from Theorem 22.

7 Case Study: Graded Modalities

In this section we apply our techniques and results to the case with graded modal operators. Formally, we extend $\mu\mathsf{ML}$ with formulae of the shape $\Diamond_{\sim g}\psi$ and $\Box_{\sim g}\psi$ , where ${\sim}\in\{\leq,\geq\}$ and the grade $g\in\mathbb{N}$ is a natural number. Intuitively, $\Diamond_{\geq g}\psi$ is true in a point $w$ if $w$ has at least $g$ successors satisfying $\psi$ and dually, $\Box_{\leq g}\psi$ is true in $w$ if all but at most $g$ successors satisfy $\psi$ [11, 25]. We denote with $\mathsf{grML}$ and $\mathsf{gr}\mu\mathsf{ML}$ the extension of $\mathsf{ML}$ and $\mu\mathsf{ML}$ , respectively, with such graded modalities. Clearly, for any $d\in\mathbb{N}$ , $\mathbb{T}^{d}$ is $\mathsf{gr}\mu\mathsf{ML}$ -definable by the formula $\theta_{d}=\nu x.(\Diamond_{\leq d}\top\wedge\Box x)$ , which is an additional motivation to study $\mathsf{grML}$ and $\mathsf{gr}\mu\mathsf{ML}$ .

Indeed, using the results and techniques from the previous section one can easily prove that $\mathsf{ML}$ -separability of $\mathsf{gr}\mu\mathsf{ML}$ -formulae (defined as expected) is 2-ExpTime-complete.

Theorem 25.

$\mathsf{ML}$ -separability of $\mathsf{gr}\mu\mathsf{ML}$ -formulae is 2-ExpTime-complete.

Proof.

For the lower bound, we reduce $\mathsf{ML}$ -separability of $\mu\mathsf{ML}$ -formulae over $\mathbb{T}^{3}$ in spirit similar to Lemma 4. Since the former problem is 2-ExpTime-hard by Theorem 22, the latter is as well. Recall the formula $\theta_{3}$ defining $\mathbb{T}^{3}$ . Then, for any $\mu\mathsf{ML}$ -formulae $\varphi,\varphi^{\prime}$ and $\psi\in\mathsf{ML}$ , we have that $\psi$ is an $\mathsf{ML}_{\sigma}$ -separator of $\varphi,\varphi^{\prime}$ over $\mathbb{T}^{3}$ iff $\psi$ is an $\mathsf{ML}_{\sigma}$ -separator of $\varphi\wedge\theta_{d},\varphi^{\prime}\wedge\theta_{d}$ .

Towards the upper bound, suppose $\varphi,\varphi^{\prime}\in\mathsf{gr}\mu\mathsf{ML}$ . Using standard arguments, one can show that $\varphi,\varphi^{\prime}$ are $\mathsf{ML}$ -separable over all models iff they are $\mathsf{ML}$ -separable over $\mathbb{T}^{d}$ , where $d=g\times(|\varphi|+|\varphi^{\prime}|)$ and $g$ is the greatest grade occurring in $\varphi,\varphi^{\prime}$ . We then construct NPTA $\mathcal{A},\mathcal{A}^{\prime}$ equivalent to $\varphi,\varphi^{\prime}$ over $d$ -ary trees via (an analogue for $\mathsf{gr}\mu\mathsf{ML}$ of) Theorem 2 and proceed with $\mathcal{A},\mathcal{A}^{\prime}$ as described in the upper bound proof of Theorem 22. $\hfill\blacktriangleleft$

Interestingly, the problem becomes easier if we allow grades in the separating formula.

Theorem 26.

$\mathsf{grML}$ -separability of $\mathsf{gr}\mu\mathsf{ML}$ -formulae is ExpTime-complete.

The lower bound follows by the usual reduction from satisfiability. We thus focus on the upper bound. Similarly to the non-graded case, we establish first a model-theoretic characterization, based on the appropriate notion of bisimilarity that characterizes the expressive power of $\mathsf{grML}$ [10]. A relation $Z$ between models is a graded bisimulation if it satisfies ( $\mathsf{atom}$ ) and graded variants of the ( $\mathsf{back}$ ) and ( $\mathsf{forth}$ ) conditions of bisimulations. The graded ( $\mathsf{forth}$ ) condition says that if $v Z w$ then for every $k\in\mathbb{N}$ and pairwise different children $v_{1},...,v_{k}$ of $v$ , there are pairwise different children $w_{1},...,w_{k}$ of $w$ satisfying $v_{i}Zw_{i}$ for all $i\leq k$ . The graded ( $\mathsf{back}$ ) condition is symmetric. It is a $g$ -graded bisimulation if the graded ( $\mathsf{forth}$ ) and ( $\mathsf{back}$ ) conditions need to be satisfied only for $k\leq g$ . We denote with $\mathcal{M}\leftrightarroweq_{\mathbf{grd}}\mathcal{M}^{\prime}$ (resp., $\mathcal{M}\leftrightarroweq_{g}\mathcal{M}^{\prime}$ ) the fact that there is a graded bisimulation (resp., a $g$ -graded bisimulation) between $\mathcal{M}$ and $\mathcal{M}^{\prime}$ that relates their roots. Variants with bounded depth $n$ and/or given signature $\sigma$ are defined and denoted as expected.

Lemma 27.

For every $\varphi,\varphi^{\prime}\in\mathsf{gr}\mu\mathsf{ML}$ with maximal grade $g_{\text{max}}$ , signature $\sigma$ , and $n\in\mathbb{N}$ , the following are equivalent:

1.

$\varphi,\varphi^{\prime}$ are not $\mathsf{grML}^{n}_{\sigma}$ -separable (over all models).
2.

$\varphi,\varphi^{\prime}$ are joint $\leftrightarroweq^{n}_{\mathbf{grd},\sigma}$ -consistent (over all models).
3.

$\varphi,\varphi^{\prime}$ are joint $\cong^{n}_{\sigma}$ -consistent (over all models).
4.

$\varphi,\varphi^{\prime}$ are joint $\cong^{n}_{\sigma}$ -consistent over $\mathbb{T}^{d}$ for $d=g_{\text{max}}\times(|\varphi|+|\varphi^{\prime}|)$ .

Using Lemma 27, one can solve $\mathsf{grML}$ -separability of $\mathsf{gr}\mu\mathsf{ML}$ formulae in exponential time, following the approach described in Section 3. More precisely, given $\varphi,\varphi^{\prime}$ , we construct NPTA $\mathcal{A},\mathcal{A}^{\prime}$ equivalent to $\varphi,\varphi^{\prime}$ over $d$ -ary trees, $d$ as in Lemma 27, and decide whether $\mathcal{A},\mathcal{A}^{\prime}$ are joint $\cong_{\sigma}^{n}$ -consistent over $\mathbb{T}^{d}$ for all $n$ via Proposition 7.

Let us provide some details on the proof of the central Lemma 27.

Proof.

We show the implications $1\Rightarrow 2\Rightarrow 3\Rightarrow 4\Rightarrow 1$ in turn. The implication $4\Rightarrow 1$ is immediate.

For $1\Rightarrow 2$ , suppose $\varphi,\varphi^{\prime}$ are not $\mathsf{grML}^{n}_{\sigma}$ -separable. Hence, for every $g\in\mathbb{N}$ there is a pair of models $\mathcal{M}_{g}\models\varphi$ and $\mathcal{M}_{g}^{\prime}\models\varphi^{\prime}$ with $\mathcal{M}_{g}\leftrightarroweq_{g,\sigma}^{n}\mathcal{M}_{g}^{\prime}$ . One can encode with an $\mathsf{FO}$ -sentence $\theta$ that two models $\mathcal{M}$ and $\mathcal{M}^{\prime}$ are depth- $n$ trees, $\mathcal{M}$ is a prefix of some $\mathcal{M}_{+}\models\varphi$ and $\mathcal{M}^{\prime}$ of some $\mathcal{M}_{+}^{\prime}\models\varphi^{\prime}$ . If $Z$ is a fresh binary symbol, then it is also possible to encode with an (infinite) set $T$ of $\mathsf{FO}$ -sentences that $Z$ is a graded bisimulation between $\mathcal{M}$ and $\mathcal{M}^{\prime}$ . Every finite fragment of $\{\theta\}\cup T$ only mentions finitely many grades and hence by assumption is satisfiable. Thus, by compactness of $\mathsf{FO}$ , the entire $\{\theta\}\cup T$ is satisfiable. This gives us $\mathcal{M}\leftrightarroweq_{\mathbf{grd},\sigma}^{n}\mathcal{M}^{\prime}$ with extensions $\mathcal{M}_{+}\models\varphi$ and $\mathcal{M}_{+}^{\prime}\models\varphi^{\prime}$ .

For $2\Rightarrow 3$ , fix witnesses $\mathcal{M},\mathcal{M}^{\prime}$ of joint $\leftrightarroweq_{\mathbf{grd},\sigma}^{n}$ -consistency, that is, $\mathcal{M}\leftrightarroweq_{\mathbf{grd},\sigma}^{n}\mathcal{M}^{\prime}$ and there are extensions $\mathcal{M}_{+},\mathcal{M}_{+}^{\prime}$ of $\mathcal{M},\mathcal{M}^{\prime}$ with $\mathcal{M}_{+}\models\varphi$ and $\mathcal{M}_{+}^{\prime}\models\varphi^{\prime}$ . By the Löwenheim-Skolem property of $\mathsf{FO}$ we may assume that both models are at most countable. It remains to apply the known fact that countable trees $\mathcal{N}$ and $\mathcal{N}^{\prime}$ satisfy $\mathcal{N}\leftrightarroweq_{\mathbf{grd}}\mathcal{N}^{\prime}$ iff $\mathcal{N}$ and $\mathcal{N}^{\prime}$ are isomorphic. For the sake of completeness, we add a brief justification of this latter statement. Assume $w\in\mathcal{N}$ and $w^{\prime}\in\mathcal{N}$ with respective children $w_{1},w_{2},...=\overline{w}$ and $w_{1}^{\prime},w_{2}^{\prime},...=\overline{w^{\prime}}$ such that $w\leftrightarroweq_{\mathbf{grd}}w^{\prime}$ . For every $\leftrightarroweq_{\mathbf{grd}}$ -equivalence class $X$ of $\overline{w}$ the corresponding equivalence class $\{w_{i}^{\prime}\ |\ \exists_{j\leq k}.\ w_{j}\leftrightarroweq_{\mathbf{grd}}% w_{i}^{\prime}\}=X^{\prime}$ has the same cardinality as $X$ . This is immediate for finite $X$ , and for infinite $X$ it follows because in countable models every two infinite subsets have the same cardinality. This allows us to inductively pick a bijective subrelation $Z$ of $\leftrightarroweq_{\mathbf{grd}}$ between $\mathcal{N}$ and $\mathcal{N}^{\prime}$ which is still a graded bisimulation.

For $3\Rightarrow 4$ , fix witnesses $\mathcal{M},\mathcal{M}^{\prime}$ of joint $\cong_{\sigma}^{n}$ -consistency, that is, $\mathcal{M}\cong_{\sigma}^{n}\mathcal{M}^{\prime}$ and there are extensions $\mathcal{M}_{+},\mathcal{M}_{+}^{\prime}$ of $\mathcal{M},\mathcal{M}^{\prime}$ with $\mathcal{M}_{+}\models\varphi$ and $\mathcal{M}_{+}^{\prime}\models\varphi^{\prime}$ . We trim $\mathcal{M}_{+}$ and $\mathcal{M}_{+}^{\prime}$ so that the outdegree becomes at most $d$ . Without loosing generality we assume that the prefixes of $\mathcal{M}_{+}$ and $\mathcal{M}_{+}^{\prime}$ are not only isomorphic but identical. The semantics of every $\psi\in\mu\mathsf{ML}$ in a model $\mathcal{N}$ is captured by a parity game whose positions are $N\times\mathsf{SubFor}(\psi)$ . We extend the definition of the game to $\mu\mathsf{ML}_{\mathbf{grd}}$ . The set of positions $N\times\mathsf{SubFor}(\psi)$ and the winning condition are defined as in the classical case, and so are the moves for all the positions with topmost connective other than the graded modalities. In the classical game, from $(v,\Diamond\theta)$ $\exists\text{ve}$ chooses a child $v^{\prime}$ of $v$ and the next position is $(v^{\prime},\theta)$ . In $(v,\Diamond_{\geq k}\theta)$ , first $\exists\text{ve}$ chooses a subset $v_{1},...,v_{k}$ of size $k$ of children of $v$ , then $\forall\text{dam}$ chooses one of these children $v_{i}$ and the next round starts at $(v_{i},\theta)$ . Dually, in $(v,\Box_{\leq k}\theta)$ first $\exists\text{ve}$ picks a subset $v_{1},...,v_{k}$ of at most $k$ $v$ ’s children, then $\forall\text{dam}$ responds with a choice of some $v^{\prime}$ not in $v_{1},...,v_{k}$ and the next position is $(v^{\prime},\theta)$ . It is tedious but straightforward to check that $\exists\text{ve}$ wins the game from $v,\psi$ iff $\psi$ is true at $v$ , as in the classical case. Note that if we take a submodel $\mathcal{N}_{0}$ of $\mathcal{N}$ which contains at least the root and all $\Diamond$ -witnesses (that is, points chosen by a winning strategy $\zeta$ in for positions of shape $(v,\Diamond_{\geq k}\theta)$ ) then (the restriction of) $\zeta$ to $\mathcal{N}_{0}$ is a winning strategy for $\mathcal{G}(\mathcal{N}_{0},\psi)$ .

Let $\zeta$ and $\zeta^{\prime}$ be positional winning strategies for $\exists\text{ve}$ in the semantic games $\mathcal{G}(\mathcal{M}_{+},\varphi)$ and $\mathcal{G}(\mathcal{M}_{+}^{\prime},\varphi^{\prime})$ . We take submodel $\mathcal{M}_{0}\models\varphi$ of $\mathcal{M}_{+}$ as follows. In the $n$ -prefix we take the root and all $\Diamond$ -witnesses for both $\zeta$ and $\zeta^{\prime}$ . In the rest of the model we only take $\Diamond$ -witnesses for $\zeta$ . A submodel $\mathcal{M}_{0}^{\prime}$ of $\mathcal{M}_{+}^{\prime}$ is defined symmetrically. It follows that $\mathcal{M}_{0}\models\varphi$ and $\mathcal{M}_{0}^{\prime}\models\varphi^{\prime}$ .

Recall that $g$ is the maximal grade appearing in $\varphi$ and $\varphi^{\prime}$ . Since the respective sets of positions of $\mathcal{G}(\mathcal{M}_{+},\varphi)$ and $\mathcal{G}(\mathcal{M}_{+}^{\prime},\varphi^{\prime})$ are $M_{+}\times\mathsf{SubFor}(\varphi)$ and $M_{+}^{\prime}\times\mathsf{SubFor}(\varphi^{\prime})$ , for every point $v$ there are at most $g\times|\varphi|$ $\Diamond$ -witnesses chosen by $\zeta$ from a position which has $v$ on the first coordinate. Consequently, the outdegree of $\mathcal{M}_{0}$ and $\mathcal{M}_{0}^{\prime}$ is not greater than $d=g\times(|\varphi|+|\varphi^{\prime}|)$ . This proves Lemma 27. $\hfill\blacktriangleleft$

8 Conclusion

We have presented an in-depth study of modal separation of $\mu\mathsf{ML}$ -formulae over different classes of structures. For us, the most interesting results are the differences that are obtained over classes of bounded outdegree for different bounds $d=1$ , $d=2$ , $d\geq 3$ . Without much effort our results on trees of bounded outdegrees can be transferred to infinite words and to ranked trees, via reductions similar to Lemma 4.

Throughout the paper we used the simplest possible measure of formula size: the length of a formula written as a string. Alternative more succinct measures, such as the number of non-isomorphic subformulae (DAG-size), are also interesting. Thus, a natural question is to what extent our results depend on the choice of size measure. In principle, using a more succinct measure makes the problems of definability and separability harder. However, all our decision procedures, with an exception of Theorem 21, are automata-based. Consequently, these procedures carry over with unchanged complexity to any size measure for which the translation from logic to nondeterministic automata has the same complexity as in Theorem 2. In the remaining case of Theorem 21 a weaker assumption suffices: the modal depth of a formula is at most polynomial in its size. Both the mentioned assumptions are arguably modest.

A place where the choice of size measure matters a little more is the construction of modal definitions and separators. In the cases of unrestricted, unary ( $\mathbb{T}^{1}$ ), and high outdegree models ( $\mathbb{T}^{d}$ for $d\geq 3$ ) the constructed formulae have DAG-size essentially the same as size: doubly, singly, and triply exponential, respectively. Interestingly, however, in the binary case $\mathbb{T}^{2}$ our formulae have only singly exponential DAG-size, which is easily seen to be optimal and contrasts with their doubly exponential size. This demonstrates that the lower bounds for size of modal definitions over $\mathbb{T}^{2}$ cannot work for DAG-size. The same lower bound construction fails for DAG-size over unrestricted models, although there the exact DAG-size complexity of optimal separators remains unknown.

We mention some interesting open problems. First, the relative succinctness of $\mu\mathsf{ML}$ over $\mathsf{ML}$ is to the best of our knowledge open in the setting with only one accessibility relation. Second, as we have mentioned in Section 3, the separators we compute are not necessarily the logically strongest ones. The logically strongest separators of $\varphi,\varphi^{\prime}$ are precisely the $\mathsf{ML}$ -uniform consequences of $\varphi$ (if they exist) and are a natural object of study. Clearly, modal definability of $\varphi$ is a sufficient condition, but not a necessary one. Let $\varphi=\psi\wedge\neg\theta_{\infty}$ and $\varphi^{\prime}=\psi$ for some $\psi\in\mathsf{ML}$ . Then $\varphi$ is not equivalent to a modal formula, but $\psi$ is a strongest separator. In the context of $\mathsf{gr}\mu\mathsf{ML}$ , open questions are $\mathsf{ML}$ -definability (and separability) and $\mu\mathsf{ML}$ -definability (and separability) of $\mathsf{gr}\mu\mathsf{ML}$ -formulae. We conjecture them to be easier than 2-ExpTime. Finally, let us mention that definability of $\mu\mathsf{ML}$ -formulae by safety formulae has been studied in [22]. It would be natural to investigate separability there as well.

References

[1] Alessandro Artale, Jean Christoph Jung, Andrea Mazzullo, Ana Ozaki, and Frank Wolter. Living without Beth and Craig: Definitions and interpolants in description and modal logics with nominals and role inclusions. ACM Trans. Comput. Log., 24(4):34:1–34:51, 2023. doi:10.1145/3597301.
[2] Franz Baader, Ian Horrocks, Carsten Lutz, and Ulrike Sattler. An Introduction to Description Logic. Cambridge University Press, 2017. URL: http://www.cambridge.org/de/academic/subjects/computer-science/knowledge-management-databases-and-data-mining/introduction-description-logic?format=PB#17zVGeWD2TZUeu6s.97.
[3] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
[4] Fabio Bellissima. On the lattice of extensions of the modal logics KAlt ${}_{\mbox{n}}$ . Arch. Math. Log., 27(2):107–114, 1988. doi:10.1007/BF01620760.
[5] Michael Benedikt, Balder ten Cate, Thomas Colcombet, and Michael Vanden Boom. The complexity of boundedness for guarded logics. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pages 293–304. IEEE Computer Society, 2015. doi:10.1109/LICS.2015.36.
[6] Achim Blumensath, Martin Otto, and Mark Weyer. Decidability results for the boundedness problem. Log. Methods Comput. Sci., 10(3), 2014. doi:10.2168/LMCS-10(3:2)2014.
[7] Mikołaj Bojańczyk and Wojciech Czerwiński. Automata Toolbox. University of Warsaw, 2018. URL: https://www.mimuw.edu.pl/~bojan/papers/toolbox.pdf.
[8] Ashok K. Chandra, Dexter Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114–133, 1981. doi:10.1145/322234.322243.
[9] Sang Cho and Dung T. Huynh. Finite-automaton aperiodicity is PSpace-complete. Theor. Comput. Sci., 88(1):99–116, 1991. doi:10.1016/0304-3975(91)90075-D.
[10] Maarten de Rijke. A note on graded modal logic. Stud Logica, 64(2):271–283, 2000. doi:10.1023/A:1005245900406.
[11] Kit Fine. In so many possible worlds. Notre Dame J. Formal Log., 13(4):516–520, 1972. doi:10.1305/NDJFL/1093890715.
[12] Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci., 18(2):194–211, 1979. doi:10.1016/0022-0000(79)90046-1.
[13] Tim French, Wiebe van der Hoek, Petar Iliev, and Barteld P. Kooi. On the succinctness of some modal logics. Artif. Intell., 197:56–85, 2013. doi:10.1016/j.artint.2013.02.003.
[14] Martin Fürer. The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems). In Logic and Machines: Decision Problems and Complexity, Proceedings of the Symposium ”Rekursive Kombinatorik”, volume 171 of Lecture Notes in Computer Science, pages 312–319. Springer, 1983. doi:10.1007/3-540-13331-3_48.
[15] Dov M. Gabbay. Craig’s interpolation theorem for modal logics. In Conference in Mathematical Logic — London ’70, pages 111–127, Berlin, Heidelberg, 1972. Springer Berlin Heidelberg.
[16] Gerd G. Hillebrand, Paris C. Kanellakis, Harry G. Mairson, and Moshe Y. Vardi. Undecidable boundedness problems for datalog programs. J. Log. Program., 25(2):163–190, 1995. doi:10.1016/0743-1066(95)00051-K.
[17] Jean Christoph Jung and Jędrzej Kołodziejski. Modal separability of fixpoint formulae. In Proceedings of the 37th International Workshop on Description Logics (DL 2024), volume 3739 of CEUR Workshop Proceedings. CEUR-WS.org, 2024. URL: https://ceur-ws.org/Vol-3739/paper-5.pdf.
[18] Jean Christoph Jung and Frank Wolter. Living without Beth and Craig: Definitions and interpolants in the guarded and two-variable fragments. In Proceedings of Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–14. IEEE, 2021. doi:10.1109/LICS52264.2021.9470585.
[19] Eryk Kopczynski. Invisible pushdown languages. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 867–872. ACM, 2016. doi:10.1145/2933575.2933579.
[20] Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333–354, 1983. doi:10.1016/0304-3975(82)90125-6.
[21] Louwe Kuijer, Tony Tan, Frank Wolter, and Michael Zakharyaschev. Separating counting from non-counting in fragments of two-variable first-order logic (extended abstract). In Proc. of DL 2024, 2024.
[22] Karoliina Lehtinen and Sandra Quickert. Deciding the first levels of the modal mu alternation hierarchy by formula construction. In Proceedings of Annual Conference on Computer Science Logic CSL, volume 41 of LIPIcs, pages 457–471. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015. doi:10.4230/LIPICS.CSL.2015.457.
[23] Christof Löding and Christopher Spinrath. Decision problems for subclasses of rational relations over finite and infinite words. Discrete Mathematics & Theoretical Computer Science, Vol. 21 no. 3, January 2019. doi:10.23638/DMTCS-21-3-4.
[24] Martin Otto. Eliminating recursion in the $\mathrm{\mu}$ -calculus. In Proceedings of 16th Annual Symposium on Theoretical Aspects of Computer Science (STACS), volume 1563 of Lecture Notes in Computer Science, pages 531–540. Springer, 1999. doi:10.1007/3-540-49116-3_50.
[25] Martin Otto. Graded modal logic and counting bisimulation. CoRR, abs/1910.00039, 2019. arXiv:1910.00039.
[26] Thomas Place and Marc Zeitoun. Separating regular languages with first-order logic. Log. Methods Comput. Sci., 12(1), 2016. doi:10.2168/LMCS-12(1:5)2016.
[27] Vaughan R. Pratt. A decidable mu-calculus: Preliminary report. In Proceedings of 22nd Annual Symposium on Foundations of Computer Science (FOCS), pages 421–427. IEEE Computer Society, 1981. doi:10.1109/SFCS.1981.4.
[28] Abraham Robinson. A result on consistency and its application to the theory of definition. Journal of Symbolic Logic, 25(2):174–174, 1960. doi:10.2307/2964240.
[29] Marcel Paul Schützenberger. On finite monoids having only trivial subgroups. Inf. Control., 8(2):190–194, 1965. doi:10.1016/S0019-9958(65)90108-7.
[30] A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733–749, 1985. doi:10.1145/3828.3837.
[31] Moshe Y. Vardi. Reasoning about the past with two-way automata. In Proceedings of International Colloquium Automata, Languages and Programming (ICALP), volume 1443 of Lecture Notes in Computer Science, pages 628–641. Springer, 1998. doi:10.1007/BFB0055090.
[32] Yde Venema. Lectures on the modal $\mu$ -calculus, 2020.

[bib.bib1] [1] Alessandro Artale, Jean Christoph Jung, Andrea Mazzullo, Ana Ozaki, and Frank Wolter. Living without Beth and Craig: Definitions and interpolants in description and modal logics with nominals and role inclusions. ACM Trans. Comput. Log., 24(4):34:1–34:51, 2023. doi:10.1145/3597301.

[bib.bib2] [2] Franz Baader, Ian Horrocks, Carsten Lutz, and Ulrike Sattler. An Introduction to Description Logic. Cambridge University Press, 2017. URL: http://www.cambridge.org/de/academic/subjects/computer-science/knowledge-management-databases-and-data-mining/introduction-description-logic?format=PB#17zVGeWD2TZUeu6s.97.

[bib.bib3] [3] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.

[bib.bib4] [4] Fabio Bellissima. On the lattice of extensions of the modal logics KAlt ${}_{\mbox{n}}$ . Arch. Math. Log., 27(2):107–114, 1988. doi:10.1007/BF01620760.

[bib.bib5] [5] Michael Benedikt, Balder ten Cate, Thomas Colcombet, and Michael Vanden Boom. The complexity of boundedness for guarded logics. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pages 293–304. IEEE Computer Society, 2015. doi:10.1109/LICS.2015.36.

[bib.bib6] [6] Achim Blumensath, Martin Otto, and Mark Weyer. Decidability results for the boundedness problem. Log. Methods Comput. Sci., 10(3), 2014. doi:10.2168/LMCS-10(3:2)2014.

[bib.bib7] [7] Mikołaj Bojańczyk and Wojciech Czerwiński. Automata Toolbox. University of Warsaw, 2018. URL: https://www.mimuw.edu.pl/~bojan/papers/toolbox.pdf.

[bib.bib8] [8] Ashok K. Chandra, Dexter Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114–133, 1981. doi:10.1145/322234.322243.

[bib.bib9] [9] Sang Cho and Dung T. Huynh. Finite-automaton aperiodicity is PSpace-complete. Theor. Comput. Sci., 88(1):99–116, 1991. doi:10.1016/0304-3975(91)90075-D.

[bib.bib10] [10] Maarten de Rijke. A note on graded modal logic. Stud Logica, 64(2):271–283, 2000. doi:10.1023/A:1005245900406.

[bib.bib11] [11] Kit Fine. In so many possible worlds. Notre Dame J. Formal Log., 13(4):516–520, 1972. doi:10.1305/NDJFL/1093890715.

[bib.bib12] [12] Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci., 18(2):194–211, 1979. doi:10.1016/0022-0000(79)90046-1.

[bib.bib13] [13] Tim French, Wiebe van der Hoek, Petar Iliev, and Barteld P. Kooi. On the succinctness of some modal logics. Artif. Intell., 197:56–85, 2013. doi:10.1016/j.artint.2013.02.003.

[bib.bib14] [14] Martin Fürer. The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems). In Logic and Machines: Decision Problems and Complexity, Proceedings of the Symposium ”Rekursive Kombinatorik”, volume 171 of Lecture Notes in Computer Science, pages 312–319. Springer, 1983. doi:10.1007/3-540-13331-3_48.

[bib.bib15] [15] Dov M. Gabbay. Craig’s interpolation theorem for modal logics. In Conference in Mathematical Logic — London ’70, pages 111–127, Berlin, Heidelberg, 1972. Springer Berlin Heidelberg.

[bib.bib16] [16] Gerd G. Hillebrand, Paris C. Kanellakis, Harry G. Mairson, and Moshe Y. Vardi. Undecidable boundedness problems for datalog programs. J. Log. Program., 25(2):163–190, 1995. doi:10.1016/0743-1066(95)00051-K.

[bib.bib17] [17] Jean Christoph Jung and Jędrzej Kołodziejski. Modal separability of fixpoint formulae. In Proceedings of the 37th International Workshop on Description Logics (DL 2024), volume 3739 of CEUR Workshop Proceedings. CEUR-WS.org, 2024. URL: https://ceur-ws.org/Vol-3739/paper-5.pdf.

[bib.bib18] [18] Jean Christoph Jung and Frank Wolter. Living without Beth and Craig: Definitions and interpolants in the guarded and two-variable fragments. In Proceedings of Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–14. IEEE, 2021. doi:10.1109/LICS52264.2021.9470585.

[bib.bib19] [19] Eryk Kopczynski. Invisible pushdown languages. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 867–872. ACM, 2016. doi:10.1145/2933575.2933579.

[bib.bib20] [20] Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333–354, 1983. doi:10.1016/0304-3975(82)90125-6.

[bib.bib21] [21] Louwe Kuijer, Tony Tan, Frank Wolter, and Michael Zakharyaschev. Separating counting from non-counting in fragments of two-variable first-order logic (extended abstract). In Proc. of DL 2024, 2024.

[bib.bib22] [22] Karoliina Lehtinen and Sandra Quickert. Deciding the first levels of the modal mu alternation hierarchy by formula construction. In Proceedings of Annual Conference on Computer Science Logic CSL, volume 41 of LIPIcs, pages 457–471. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2015. doi:10.4230/LIPICS.CSL.2015.457.

[bib.bib23] [23] Christof Löding and Christopher Spinrath. Decision problems for subclasses of rational relations over finite and infinite words. Discrete Mathematics & Theoretical Computer Science, Vol. 21 no. 3, January 2019. doi:10.23638/DMTCS-21-3-4.

[bib.bib24] [24] Martin Otto. Eliminating recursion in the $\mathrm{\mu}$ -calculus. In Proceedings of 16th Annual Symposium on Theoretical Aspects of Computer Science (STACS), volume 1563 of Lecture Notes in Computer Science, pages 531–540. Springer, 1999. doi:10.1007/3-540-49116-3_50.

[bib.bib25] [25] Martin Otto. Graded modal logic and counting bisimulation. CoRR, abs/1910.00039, 2019. arXiv:1910.00039.

[bib.bib26] [26] Thomas Place and Marc Zeitoun. Separating regular languages with first-order logic. Log. Methods Comput. Sci., 12(1), 2016. doi:10.2168/LMCS-12(1:5)2016.

[bib.bib27] [27] Vaughan R. Pratt. A decidable mu-calculus: Preliminary report. In Proceedings of 22nd Annual Symposium on Foundations of Computer Science (FOCS), pages 421–427. IEEE Computer Society, 1981. doi:10.1109/SFCS.1981.4.

[bib.bib28] [28] Abraham Robinson. A result on consistency and its application to the theory of definition. Journal of Symbolic Logic, 25(2):174–174, 1960. doi:10.2307/2964240.

[bib.bib29] [29] Marcel Paul Schützenberger. On finite monoids having only trivial subgroups. Inf. Control., 8(2):190–194, 1965. doi:10.1016/S0019-9958(65)90108-7.

[bib.bib30] [30] A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733–749, 1985. doi:10.1145/3828.3837.

[bib.bib31] [31] Moshe Y. Vardi. Reasoning about the past with two-way automata. In Proceedings of International Colloquium Automata, Languages and Programming (ICALP), volume 1443 of Lecture Notes in Computer Science, pages 628–641. Springer, 1998. doi:10.1007/BFB0055090.

[bib.bib32] [32] Yde Venema. Lectures on the modal $\mu$ -calculus, 2020.