# Modal Separability of Fixpoint Formulae

Jean Christoph Jung  Jędrzej Kołodziejski

(TU Dortmund University)

###### Abstract

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

##  1 Introduction

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

######  Example 1.

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

  * $P$:

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

  * $P^{\prime}$:

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

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

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

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

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

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

Missing proofs can be found in the appendix.

#### Related Work.

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

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

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

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

##  2 Preliminaries

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

#### Syntax.

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

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

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

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

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

#### Semantics.

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

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

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

#### Size of formulae.

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

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

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

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

#### Automata.

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

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

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

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

######  Theorem 1.

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

##  3 Foundations of Separability

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

######  Definition 1.

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

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

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

######  Theorem 2.

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

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

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

######  Example 2.

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

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

######  Lemma 1.

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

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

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

######  Proposition 1.

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

  1. (i)

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

  2. (ii)

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

  3. (iii)

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

  4. (iv)

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

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

######  Theorem 3.

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

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

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

######  Theorem 4.

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

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

######  Proposition 2.

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

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

######  Definition 2.

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

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

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

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

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

##  4 Optimal Separators: Arbitrary Models

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

###  4.1 Construction

######  Theorem 5.

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

The above is a consequence of the following lemma.

######  Lemma 2.

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

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

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

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

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

###### Proof.

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

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

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

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

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

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

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

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

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

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

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

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

###  4.2 Lower bounds

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

######  Proposition 3.

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

###### Proof.

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

  * $B_{n}$:

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

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

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

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

  * $P_{n}$:

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

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

##  5 Optimal Separators: Word Case

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

######  Theorem 6.

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

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

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

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

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

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

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

######  Lemma 3.

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

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

###### Proof.

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

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

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

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

######  Proposition 4.

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

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

##  6 Conclusion and Open Problems

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

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

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

## 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.
  * [2] Christel Baier and Joost-Pieter Katoen.  Principles of model checking.  MIT Press, 2008.
  * [3] Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors.  Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning.  North-Holland, 2007.
  * [4] Mikołaj Bojańczyk and Wojciech Czerwiński.  Automata Toolbox.  Univrsity of Warsaw, 2018.
  * [5] Giovanna D’Agostino and Marco Hollenberg.  Uniform interpolation, automata and the modal $\mu$-calculus.  In Marcus Kracht, Maarten de Rijke, Heinrich Wansing, and Michael Zakharyaschev, editors, Advances in Modal Logic 1, papers from the first workshop on "Advances in Modal logic," held in Berlin, Germany, 8-10 October 1996, pages 73–84. CSLI Publications, 1996.
  * [6] Michael J. Fischer and Richard E. Ladner.  Propositional dynamic logic of regular programs.  J. Comput. Syst. Sci., 18(2):194–211, 1979.
  * [7] 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.
  * [8] David Janin and Igor Walukiewicz.  On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic.  In Ugo Montanari and Vladimiro Sassone, editors, CONCUR ’96: Concurrency Theory, pages 263–277, 1996.
  * [9] Jean Christoph Jung, Carsten Lutz, Hadrien Pulcini, and Frank Wolter.  Logical separability of labeled data examples under ontologies.  Artif. Intell., 313:103785, 2022.
  * [10] Jean Christoph Jung and Frank Wolter.  Living without beth and craig: Definitions and interpolants in the guarded and two-variable fragments.  In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–14. IEEE, 2021.
  * [11] Dexter Kozen.  Results on the propositional mu-calculus.  Theor. Comput. Sci., 27:333–354, 1983.
  * [12] 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.
  * [13] Karoliina Lehtinen and Sandra Quickert.  Deciding the first levels of the modal mu alternation hierarchy by formula construction.  In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 457–471. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.
  * [14] Denis Mayr Lima Martins.  Reverse engineering database queries from examples: State-of-the-art, challenges, and research opportunities.  Inf. Syst., 83:89–100, 2019.
  * [15] Maarten Marx.  Interpolation in modal logic.  In International Conference on Algebraic Methodology and Software Technology, 1999.
  * [16] Martin Otto.  Eliminating recursion in the $\mathrm{\mu}$-calculus.  In Christoph Meinel and Sophie Tison, editors, STACS 99, 16th Annual Symposium on Theoretical Aspects of Computer Science, Trier, Germany, March 4-6, 1999, Proceedings, volume 1563 of Lecture Notes in Computer Science, pages 531–540. Springer, 1999.
  * [17] Thomas Place and Marc Zeitoun.  Separating regular languages with first-order logic.  Log. Methods Comput. Sci., 12(1), 2016.
  * [18] Andreas Potthoff.  First-order logic on finite trees.  In Theory and Practice of Software Development, 1995.
  * [19] Vaughan R. Pratt.  A decidable mu-calculus: Preliminary report.  In 22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28-30 October 1981, pages 421–427. IEEE Computer Society, 1981.
  * [20] A. Prasad Sistla and Edmund M. Clarke.  The complexity of propositional linear temporal logics.  J. ACM, 32(3):733–749, 1985.
  * [21] Moshe Y. Vardi.  Reasoning about the past with two-way automata.  In Kim Guldstrand Larsen, Sven Skyum, and Glynn Winskel, editors, Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings, volume 1443 of Lecture Notes in Computer Science, pages 628–641. Springer, 1998.
  * [22] Yde Venema.  Lectures on the modal $\mu$-calculus, 2020.
  * [23] Albert Visser.  Uniform interpolation and layered bisimulation.  In Petr Hájek, editor, Gödel ’96: Logical Foundations of Mathematics, Computer Science and Physics - Kurt Gödel’s Legacy, Lecture Notes in Logic, page 139–164. Springer, 1996.

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

##  Appendix A Separability Coincides with Craig Separability

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

###### Proof.

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

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

##  Appendix B Model-theoretic Characterization

We prove Proposition 1.

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

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

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

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

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

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

$M_{Z}=M\cup Z$

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

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

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

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

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

##  Appendix C Separability over All Models is in ExpTime

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

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

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

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

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

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

$\displaystyle R\in\delta_{0}^{\mathcal{B}}(q,q^{\prime})$ $\displaystyle\iff$
There is $c\in\Sigma$, such that the left projection of $R$
$\displaystyle\text{belongs to $\delta(q,c)$ and the right one to
$\delta^{\prime}(q^{\prime},c)$}.$

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

$\displaystyle R\in\delta^{\mathcal{B}}(q,q^{\prime})$ $\displaystyle\iff$ $R$
can be obtained from some
$R^{\prime}\in\delta_{0}^{\mathcal{B}}(q,q^{\prime})$ by removing some
consistent pairs.

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

To finish the proof let us first prove Proposition 2.

###### Proof.

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

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

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

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

##  Appendix D Separability over Words is in PSpace

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

##  Appendix E Lower Bounds over All Models

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

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

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

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

  * •

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

  * •

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

  * •

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

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

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

##  Appendix F Optimal Separators over Words

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

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

  * $(\ast)$

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

The definition is by induction on $m$:

$\displaystyle\psi^{0}_{pq}$ $\displaystyle=\text{ if $p\neq q$ then $\bot$
else $\top$}$ $\displaystyle\psi^{1}_{pq}$ $\displaystyle=\bigvee\\{c\ \mid\
c\in\Sigma,\\{q\\}\in\delta(p,c)\\}$ $\displaystyle\psi^{m}_{pq}$
$\displaystyle=\bigvee_{q^{\prime}\in Q}\psi^{\lfloor
m/2\rfloor}_{pq^{\prime}}\wedge\psi^{\lceil m/2\rceil}_{q^{\prime}q}$

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

We finish the construction by setting:

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

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

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

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

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


# Dual-Mode Chirp Spread Spectrum Modulation

Ali Waqar Azim, Ahmad Bazzi, Raed Shubair, Marwa Chafii Ali Waqar Azim is with
Department of Telecommunication Engineering, University of Engineering and
Technology, Taxila, Pakistan (email: aliwaqarazim@gmail.com).Ahmad Bazzi and
Raed Shubair is with with Engineering Division, New York University (NYU) Abu
Dhabi, 129188, UAE (email: {ahmad.bazzi,raed.shubair}@nyu.edu).Marwa Chafii is
with Engineering Division, New York University (NYU) Abu Dhabi, 129188, UAE
and NYU WIRELESS, NYU Tandon School of Engineering, Brooklyn, 11201, NY, USA
(email: marwa.chafii@nyu.edu).

###### Abstract

In this letter, we propose dual-mode chirp spread spectrum (DM-CSS) modulation
for low-power wide-area networks. DM-CSS is capable of achieving a higher
spectral efficiency (SE) relative to its counterparts, such as Long Range
(LoRa) modulation. Considering the same symbol period, the SE in DM-CSS are
augmented by: (i) simultaneously multiplexing even and odd chirp signals; (ii)
using phase shifts of $0$ and $\pi$ radians for both even and odd chirp
signals; and (iii) using either up-chirp or down-chirp signal. The SE
increases by up to $116.66\%$ for the same bandwidth and spreading factor
relative to LoRa. We present a complete transceiver architecture along with
non-coherent detection process. Simulation results reveal that DM-CSS is not
only more spectral efficient but also more energy efficient than most
classical counterparts. It is also demonstrated that DM-CSS is robust to phase
and frequency offsets.

###### Index Terms:

LoRa, Low power wide area networks, chirp spread spectrum, IoT.

##  I Introduction

Long Range (LoRa) is a frequency-shift chirp spread spectrum (CSS) modulation
[1], in which, the number of bits transmitted per symbol is equal to the
spreading factor, $\lambda$, that results in $N=2^{\lambda}$ chirp symbols,
where $N$ is the number of cyclic time-shifts of the chirp signal. Despite the
fact that LoRa offers a wide range of throughputs, and can target a multitude
of applications, one of the limiting factors is the low achievable bit
rate/spectral efficiency (SE). In this letter, we define SE as the achievable
bit rate in a given bandwidth, and energy efficiency (EE) as the required
signal-to-noise ratio (SNR) for correct bit detection at a given bit-error
rate (BER).

Several studies have proposed energy and/or spectral efficient variants of
LoRa. Some alternatives are [2, 3, 4, 5, 6, 7, 8]. In [2], the authors propose
phase-shift keying-LoRa (PSK-LoRa), that encodes additional bits in the phase
shifts (PSs) of the chirp signal, where quaternary PSs result in the optimal
performance in terms of EE. In addition, $\lambda+2$ bits per symbol are
transmitted. The performance of PSK-LoRa can be further improved with enhanced
PSK-LoRa (ePSK-LoRa) [3]. The optimal variant of ePSK-LoRa transmits
$\lambda+3$ bits per symbol. Nonetheless, both PSK-LoRa and ePSK-LoRa require
coherent detection to determine the information embedded in the PSs, and are
capable of transmitting only $2$ or $3$ additional bits relative to LoRa,
respectively. Another approach that transmits $\lambda+1$ bits per symbol by
extending the signal space using negative frequency change slope is slope-
shift keying-LoRa (SSK-LoRa) [4]. In interleaved chirp spreading LoRa (ICS-
LoRa) [5], the use of interleaved LoRa symbols provide an additional dimension
to transmit $\lambda+1$ bits per symbol. Both SSK-LoRa and ICS-LoRa only
marginally increase the SE relative to LoRa because only $1$ additional bit is
transmitted per symbol in these approaches compared to LoRa. SSK-ICS-LoRa [6]
amalgamates SSK-LoRa and ICS-LoRa and uses up chirps, down chirps (for signal
spreading), and interleaved versions of both, enabling it to transmit
$\lambda+2$ bits per symbol. Though SSK-ICS-LoRa outperforms LoRa, SSK-LoRa
and ICS-LoRa in terms of the EE and SE, it only increases the number of
transmitted bits per symbol by $2$ relative to LoRa: that is unsubstantial.
Recently, group-based CSS (GCSS) has been proposed in [7], that is
configurable via so-called group number, $\mathrm{G}$, which provides a trade-
off between EE and SE. By increasing $\mathrm{G}$, the EE decreases, but the
SE increases and vice versa. The number of transmitted bits per symbol for
GCSS using $\mathrm{G}=2$ is $2\lambda-2$. Note that while all the variants of
GCSS are more spectral efficient than LoRa, only a few are energy efficient
because increasing $\mathrm{G}$ reduces the EE. The scheme in [8], i.e.,
discrete chirp-rate keying (DCRK)-CSS, transmits additional bits in the
discrete chirp rate. Considering $M_{\mathrm{c}}$ chirp rates, the number of
transmitted bits per symbol is $\lambda+\log_{2}(M_{\mathrm{c}})$. DCRK-CSS
improves both the EE and SE relative to LoRa, however, an increase in
$M_{\mathrm{c}}$ considerably increases the complexity of DCRK-CSS receiver,
and the increase in the number of bits is limited by a factor of
$\log_{2}(M_{\mathrm{c}})$.

In this letter, we propose dual-mode CSS (DM-CSS) modulation as an alternative
to the classical schemes as it circumvents most of their limitations. Unlike
PSK-LoRa and ePSK-LoRa, both coherent and non-coherent detection is possible
for DM-CSS. Moreover, contrary to the remainder of previously discussed
schemes, DM-CSS almost doubles the number of transmitted bits per symbol
relative to LoRa. In DM-CSS, which is an improved variant of the scheme in
[9], $N$ frequencies of an un-chirped symbol are divided into
$\nicefrac{{N}}{{2}}$ even and $\nicefrac{{N}}{{2}}$ odd frequencies. Next,
binary PSs are added to both the activated even and odd frequencies. Lastly,
the un-chirped symbol is chirped using either the up-chirp or the down-chirp.
It is highlighted that the term dual-mode refers to the use of both the even
and the odd frequencies. It shall become evident in the sequel that the
proposed DM-CSS has the following concrete advantages of the classical
counterparts: (i) higher achievable SE, i.e., it is capable of transmitting
higher number of bits per symbol for the same symbol duration and bandwidth;
(ii) it is more energy efficient, in a sense that for the same throughput,
less SNR/bit is needed; and (iii) both coherent and non-coherent detection is
applicable.

We can summarize the contributions of this work as follows:

  1. 1.

A novel DM-CSS modulation is proposed that achieves higher SE and better EE
than other alternatives.

  2. 2.

A complete transceiver architecture for DM-CSS employing non-coherent
detection is provided.

  3. 3.

A framework for evaluating the orthogonality of DM-CSS symbols is provided.

  4. 4.

The performance of DM-CSS in terms of BER considering additive white Gaussian
noise (AWGN) channel, fading channel, and in the presence of phase and
frequency offsets is evaluated.

The rest of the article is organized as follows. Section II provides the
transceiver architecture and evaluates the orthogonality of the DM-CSS
symbols. Section III provides simulation results and Section IV renders
conclusions.

##  II Dual-Mode Chirp Spread Spectrum (DM-CSS)

In this section, we introduce DM-CSS modulation. Table I provides a summary of
different LoRa variant time-domain signal structures, achievable SE in
bits/s/Hz, and relative increase in SE over LoRa in bits/s/Hz.

From Table I, it can be observed that the information bearing element in LoRa
is cyclic time-shift of the chirp signal, i.e., $k$. In DM-CSS, besides the
information being transmitted in use of either up-chirp or down-chirp, it is
also transmitted via the activated even and odd activated frequencies and
their corresponding PSs, i.e.,
$k_{\mathrm{e}},k_{\mathrm{o}},\alpha_{\mathrm{e}}$ and $\alpha_{\mathrm{o}}$.
ePSK-LoRa transmits information in the PSs of $l$ sub-blocks, i.e., $p_{l}$,
where $l=\llbracket 1,N_{\mathrm{b}}\rrbracket$, and the fundamental
frequency, $k$ [3]. SSK-ICS-LoRa uses up chirps, down chirps, interleaved up-
chirp and interleaved down-chirp. In GCSS, SE depends on $\mathrm{G}$, where
an increase in $\mathrm{G}$ results in higher achievable SE. DCRK-CSS uses
different $M_{\mathrm{c}}$ to increase the number of bits transmitted per
symbol.

TABLE I: Characteristics of Different LoRa variants. Here,
$\lambda=log_{2}(N)$, $N_{\mathrm{b}}$ and $M_{\phi}$ are the number of sub-
blocks and the number of PSs used in ePSK-LoRa, $\Pi[\cdot]$ refers to
interleaved version of a chirp symbol.

Modulation | Transmit Symbol | SE | SE increase w.r.t. LoRa
---|---|---|---
LoRa | $\exp\left\\{j\frac{2\pi}{N}n(k+n)\right\\}$ | $\frac{\lambda}{N}$ | $-$
DM-CSS | $\alpha_{\mathrm{e}}\exp\left\\{j\frac{2\pi}{N}n\left(k_{\mathrm{e}}\pm n\right)\right\\}+\alpha_{\mathrm{o}}\exp\left\\{j\frac{2\pi}{N}n\left(k_{\mathrm{o}}\pm n\right)\right\\}$ | $\frac{2\lambda+1}{N}$ | $\frac{\lambda+1}{N}$
ePSK-LoRa | $\sum_{l=1}^{N_{\mathrm{b}}}\exp\left\\{j2\pi\left(\frac{kn}{N}+\frac{ln}{N_{\mathrm{b}}}+\frac{p_{l}}{2^{\eta_{\mathrm{PS}}}}+\frac{n^{2}}{N}\right)\right\\}$ | $\frac{\log_{2}(\nicefrac{{N}}{{N_{\mathrm{b}}}})+N_{\mathrm{b}}\log_{2}(M_{\phi})}{N}$ |  $\frac{3}{N}$ (for $\\{N_{\mathrm{b}},M_{\phi}\\}=\\{2,4\\}$)
SSK-ICS-LoRa |  $\exp\left\\{j\frac{2\pi}{N}n(k\pm n)\right\\}$, $\Pi\left[\exp\left\\{j\frac{2\pi}{N}n(k\pm n)\right\\}\right]$ | $\frac{\lambda+2}{M}$ | $\frac{2}{N}$
GCSS |  $\sum_{i=1}^{\mathrm{G}}\exp\left\\{j\frac{2\pi}{N}n(k_{i}+n)\right\\}$, $k_{i}=\llbracket(i-1)\frac{N}{\mathrm{G}},i\left(\frac{N}{\mathrm{G}}-1\right)\rrbracket$ | $\frac{\mathrm{G}\log_{2}(\nicefrac{{N}}{{\mathrm{G}}})}{N}$ | $\frac{\mathrm{G}\log_{2}(\nicefrac{{N}}{{G}})-1}{N}$
DCRK-CSS | $\exp\left\\{j\frac{\pi}{N}n(2k+M_{\mathrm{c}}n)\right\\}$ | $\frac{\lambda+\log_{2}(M_{\mathrm{c}})}{N}$ | $\frac{\log_{2}(M_{\mathrm{c}})}{N}$

###  II-A Transmission

Consider that $N$ frequencies are available in bandwidth
$B=\nicefrac{{N}}{{T_{\mathrm{s}}}}$, where $T_{\mathrm{s}}$ is the symbol
period. Among these $N$ frequencies, there are $\nicefrac{{N}}{{2}}$ even and
$\nicefrac{{N}}{{2}}$ odd frequencies. The even frequencies and odd
frequencies are denoted by indexes $2\tilde{k}_{\mathrm{e}}$ and
$2\tilde{k}_{\mathrm{o}}+1$ for
$\tilde{k}_{\mathrm{e}}=\tilde{k}_{\mathrm{o}}=\llbracket
0,\nicefrac{{N}}{{2}}-1\rrbracket$, respectively. One even, $k_{\mathrm{e}}$,
and one odd frequency, $k_{\mathrm{o}}$ is activated among the possible
$\nicefrac{{N}}{{2}}$ even and $\nicefrac{{N}}{{2}}$ odd frequencies. The
activated frequencies (even and odd) have a PS of either $0$ or $\pi$ radians:
which is denoted by $\alpha$. If the PS is $0$ radians, then $\alpha=1$, on
the contrary, if the PS is $\pi$ radians, then $\alpha=-1$. The discrete
representation of the un-chirped symbol is given as:

$f(n)=\alpha_{\mathrm{e}}\exp\left\\{j\frac{2\pi}{N}k_{\mathrm{e}}n\right\\}+\alpha_{\mathrm{o}}\exp\left\\{j\frac{2\pi}{N}k_{\mathrm{o}}n\right\\},$
(1)

for $n=\llbracket 0,N-1\rrbracket$, where $j=\sqrt{-1}$. $\alpha_{\mathrm{e}}$
and $\alpha_{\mathrm{o}}$ represents the PSs for even and odd frequencies,
respectively. $f(n)$ is then chirped using either an up-chirp,
$c_{\mathrm{u}}(n)=\exp\left\\{j\frac{2\pi}{N}n^{2}\right\\}$, or a down-
chirp, $c_{\mathrm{d}}(n)=\exp\left\\{-j\frac{2\pi}{N}n^{2}\right\\}$. The
chirped signal, $s(n)=f(n)c_{\mathrm{u/d}}(n)$ is given as:

$s(n)=\alpha_{\mathrm{e}}\exp\left\\{j\frac{2\pi}{N}n\left(k_{\mathrm{e}}\pm
n\right)\right\\}+\alpha_{\mathrm{o}}\exp\left\\{j\frac{2\pi}{N}n\left(k_{\mathrm{o}}\pm
n\right)\right\\},$ (2)

where $c_{\mathrm{u/d}}(n)$ refers to either an up-chirp or a down-chirp.

DM-CSS can be extended to $p-$mode type encoding, however, the resulting
design may not be energy efficient and it will come at a cost of higher
complexity.The symbol energy of $s(n)$ is
$E_{\mathrm{s}}=\nicefrac{{1}}{{N}}\sum_{n=0}^{N-1}|s(n)|^{2}=2$.

The breakdown of the number of bits encoded in the DM-CSS symbol is as
follows: (i) $\lambda_{\mathrm{e}}=\log_{2}(\nicefrac{{N}}{{2}})$ and
$\lambda_{\mathrm{o}}=\log_{2}(\nicefrac{{N}}{{2}})$ bits are encoded in
$k_{\mathrm{e}}$ and $k_{\mathrm{o}}$, respectively; (ii)
$\lambda_{\mathrm{PS}}=2\log_{2}(2)=2$ bits are encoded in
$\alpha_{\mathrm{e}}$ and $\alpha_{\mathrm{o}}$; and (iii)
$\lambda_{\mathrm{c}}=\log_{2}(2)=1$ bit is encoded in the use of either up-
chirp or the down-chirp. Thus, the total number of bits that can be
transmitted per DM-CSS symbol of duration $T_{\mathrm{s}}$ is

$\lambda_{\mathrm{DM-
CSS}}=\lambda_{\mathrm{e}}+\lambda_{\mathrm{o}}+\lambda_{\mathrm{PS}}+\lambda_{\mathrm{c}}=2\lambda+1.$
(3)

Given that the bit rate for DM-CSS is $R=\nicefrac{{\lambda_{\mathrm{DM-
CSS}}}}{{T_{\mathrm{s}}}}$, and $B=\nicefrac{{M}}{{T_{\mathrm{s}}}}$, the SE
for DM-CSS, $\eta_{\mathrm{DM-CSS}}$ is given as:

$\eta_{\mathrm{DM-CSS}}=\frac{R}{B}=\frac{2\lambda+1}{N}.$ (4)

From (4), it is evident that the relative SE increase for DM-CSS over LoRa is
$\nicefrac{{(\lambda+1)}}{{N}}$, which yields a SE increase of $116.66\%$ and
$108.33\%$ over LoRa for $\lambda=6$ and $\lambda=12$, respectively.

###  II-B Detection

Here we only provide the non-coherent detection process which does not require
any a priori knowledge of the channel because of its practicality as the
coherent detector is generally very complex. However, to counterbalance any
phase rotation of the channel (if it is $\geq\nicefrac{{\pi}}{{2}}$), a
coherent detector that has a priori knowledge of the channel is mandatory.

Firstly, the received symbol, $r(n)$ is multiplied with both an up-chirp and a
down-chirp yielding $r_{1}(n)=r(n)c_{\mathrm{d}}(n)$ and
$r_{2}(n)=r(n)c_{\mathrm{u}}(n)$. Next, $R_{1}(k)$ and $R_{2}(k)$ are obtained
by evaluating the discrete Fourier transform (DFT) for $r_{1}(n)$ and
$r_{2}(n)$, respectively. By using
$\kappa_{1}=\max\left\\{|R_{1}(k)|\right\\}$, and
$\kappa_{2}=\max\left\\{|R_{2}(k)|\right\\}$ for $k=\llbracket
0,N-1\rrbracket$, the following criterion:

$\kappa_{1}\lessgtr\kappa_{2}.$ (5)

determines whether an up-chirp was used or a down-chirp was used for chirping
at the transmitter. If $\kappa_{1}>\kappa_{2}$, then an up-chirp was used,
conversely if $\kappa_{2}>\kappa_{1}$, a down-chirp was used.

Using non-coherent detection process, the activated even and odd frequencies
are estimated as:

$\hat{k}_{\mathrm{e}}=\mathrm{arg}\max_{k\in
2\tilde{k}_{\mathrm{e}}}~{}\left|R(k)\right|,~{}~{}\text{and}~{}~{}\hat{k}_{\mathrm{o}}=\mathrm{arg}\max_{k\in
2\tilde{k}_{\mathrm{o}}+1}~{}\left|R(k)\right|,$ (6)

respectively, where

$R(k)=\left\\{\begin{array}[]{ c l }R_{1}(k)&\quad\kappa_{1}>\kappa_{2}\\\
R_{2}(k)&\quad\kappa_{1}<\kappa_{2}\end{array}\right..$ (7)

The PSs of even and odd frequencies are respectively evaluated by determining
the polarity of $R(\hat{k}_{\mathrm{e}})$ and $R(\hat{k}_{\mathrm{o}})$ as:

$\hat{\alpha}_{\mathrm{e}}=\mathrm{polarity}\left\\{R(\hat{k}_{\mathrm{e}})\right\\},~{}~{}\text{and}~{}~{}\hat{\alpha}_{\mathrm{o}}=\mathrm{polarity}\left\\{R(\hat{k}_{\mathrm{o}})\right\\},$
(8)

where $\mathrm{polarity}\\{\cdot\\}$ is the maximum likelihood criteria to
determine the polarity of the input frequency index. If the output of
$\mathrm{polarity}\\{\cdot\\}>0$, then
$\hat{\alpha}_{\mathrm{e}}/\hat{\alpha}_{\mathrm{o}}=1$, conversely,
$\hat{\alpha}_{\mathrm{e}}/\hat{\alpha}_{\mathrm{o}}=-1$. It is accentuated
that if the channel’s phase rotation is $\geq\nicefrac{{\pi}}{{2}}$, then,
only coherent detection would be viable because the
$\mathrm{polarity}\\{\cdot\\}$ function will no longer be applicable.

###  II-C Orthogonality of DM-CSS Symbols

To establish the orthogonality of DM-CSS symbol, we evaluate the inner product
of two distinct symbols as $\langle
s(n),\tilde{s}(n)\rangle=\sum_{n=0}^{N-1}s(n)\overline{\tilde{s}}(n)$. Note
that the activated even and odd frequencies and PSs in $s(n)$ are
$k_{\mathrm{e}}$, $k_{\mathrm{o}}$, $\alpha_{\mathrm{e}}$, and
$\alpha_{\mathrm{o}}$, whereas the activated even and odd frequencies and PS
in $\tilde{s}(n)$ are $\tilde{k}_{\mathrm{e}}$, $\tilde{k}_{\mathrm{o}}$,
$\tilde{\alpha}_{\mathrm{e}}$, and $\tilde{\alpha}_{\mathrm{o}}$. Note that
the following conditions must hold to evaluate the orthogonality: (i)
$k_{\mathrm{e}}\neq\tilde{k}_{\mathrm{e}}$; and (ii)
$k_{\mathrm{o}}\neq\tilde{k}_{\mathrm{o}}$. Moreover, it shall become evident
that the PSs and chirps do not impact the orthogonality of the symbols,
therefore, it does not matter if they are same or different. Additionally,
there are four distinct cases for which the orthogonality should be evaluated.
The cases are: (i) when both $s(n)$ and $\tilde{s}(n)$ are attained using an
up-chirp, i.e., $s(n)=f(n)c_{\mathrm{u}}(n)$ and
$\tilde{s}(n)=\tilde{f}(n)c_{\mathrm{u}}(n)$; (ii) when both $s(n)$ and
$\tilde{s}(n)$ are attained using a down-chirp, i.e.,
$s(n)=f(n)c_{\mathrm{d}}(n)$ and $\tilde{s}(n)=\tilde{f}(n)c_{\mathrm{d}}(n)$;
(iii) when $s(n)$ is attained using an up-chirp and $\tilde{s}(n)$ is attained
using a down-chirp, i.e., $s(n)=f(n)c_{\mathrm{u}}(n)$ and
$\tilde{s}(n)=\tilde{f}(n)c_{\mathrm{d}}(n)$; and (iv) when $s(n)$ is attained
using a down-chirp and $\tilde{s}(n)$ is attained using an up-chirp, i.e.,
$s(n)=f(n)c_{\mathrm{d}}(n)$ and $\tilde{s}(n)=\tilde{f}(n)c_{\mathrm{u}}(n)$.
In the sequel, we consider these cases separately.

#### Case I: $s(n)=f(n)c_{\mathrm{u}}(n)$ and
$\tilde{s}(n)=\tilde{f}(n)c_{\mathrm{u}}(n)$

In this case, $\langle s(n),\tilde{s}(n)\rangle$ evaluates to

$\begin{split}\langle
s(n),\tilde{s}(n)\rangle&=\alpha_{\mathrm{e}}\tilde{\alpha}_{\mathrm{e}}\underbrace{\sum_{n=0}^{N-1}\exp\left\\{j\frac{2\pi}{N}n\left(k_{\mathrm{e}}-\tilde{k}_{\mathrm{e}}\right)\right\\}}_{:=\tau_{1}}\\\
&+\alpha_{\mathrm{e}}\tilde{\alpha}_{\mathrm{o}}\underbrace{\sum_{n=0}^{N-1}\exp\left\\{j\frac{2\pi}{N}n\left(k_{\mathrm{e}}-\tilde{k}_{\mathrm{o}}\right)\right\\}}_{:=\tau_{2}}\\\
&+\alpha_{\mathrm{o}}\tilde{\alpha}_{\mathrm{e}}\underbrace{\sum_{n=0}^{N-1}\exp\left\\{j\frac{2\pi}{N}n\left(k_{\mathrm{o}}-\tilde{k}_{\mathrm{e}}\right)\right\\}}_{:=\tau_{3}}\\\
&+\alpha_{\mathrm{o}}\tilde{\alpha}_{\mathrm{o}}\underbrace{\sum_{n=0}^{N-1}\exp\left\\{j\frac{2\pi}{N}n\left(k_{\mathrm{o}}-\tilde{k}_{\mathrm{o}}\right)\right\\}}_{:=\tau_{4}}.\end{split}$
(9)

For $k_{\mathrm{e}}\neq\tilde{k}_{\mathrm{e}}$

$\begin{split}\tau_{1}=\frac{1-\exp\left\\{j2\pi(k_{\mathrm{e}}-\tilde{k}_{\mathrm{e}})\right\\}}{1-\exp\left\\{j\frac{2\pi}{N}(k_{\mathrm{e}}-\tilde{k}_{\mathrm{e}})\right\\}}=0.\end{split}$
(10)

$\tau_{2}=\tau_{3}=\tau_{4}=0$, no matter what since the odd and even
frequencies can never meet. Thus, $\langle s(n),\tilde{s}(n)\rangle=0$ when
$s(n)=f(n)c_{\mathrm{u}}(n)$ and $\tilde{s}(n)=\tilde{f}(n)c_{\mathrm{u}}(n)$.

#### Case II: $s(n)=f(n)c_{\mathrm{d}}(n)$ and
$\tilde{s}(n)=\tilde{f}(n)c_{\mathrm{d}}(n)$

In this particular case, the inner product, $\langle s(n),\tilde{s}(n)\rangle$
is equal to:

$\begin{split}\langle
s(n),\tilde{s}(n)\rangle&=\alpha_{\mathrm{e}}\tilde{\alpha}_{\mathrm{e}}\overline{\tau}_{1}+\alpha_{\mathrm{e}}\tilde{\alpha}_{\mathrm{o}}\overline{\tau}_{2}+\alpha_{\mathrm{o}}\tilde{\alpha}_{\mathrm{e}}\overline{\tau}_{3}+\alpha_{\mathrm{o}}\tilde{\alpha}_{\mathrm{o}}\overline{\tau}_{4},\end{split}$
(11)

where, $\overline{(\cdot)}$ denotes the conjugate of a complex argument.

Since, $\tau_{1}=\tau_{2}=\tau_{3}=\tau_{4}=0$, therefore,
$\overline{\tau}_{1}=\overline{\tau}_{2}=\overline{\tau}_{3}=\overline{\tau}_{4}=0$,
which leads to $\langle s(n),\tilde{s}(n)\rangle=0$.

#### Case III: $s(n)=f(n)c_{\mathrm{u}}(n)$ and
$\tilde{s}(n)=\tilde{f}(n)c_{\mathrm{d}}(n)$

In this case, we have

$\begin{split}\langle
s(n),\tilde{s}(n)\rangle&=\alpha_{\mathrm{e}}\tilde{\alpha}_{\mathrm{e}}\underbrace{\sum_{n=0}^{N-1}\exp\left\\{j\frac{2\pi}{N}n\left(\alpha_{1}-\beta_{1}\right)\right\\}}_{:=\tau_{5}}\\\
&+\alpha_{\mathrm{e}}\tilde{\alpha}_{\mathrm{o}}\underbrace{\sum_{n=0}^{N-1}\exp\left\\{j\frac{2\pi}{N}n\left(\alpha_{1}-\beta_{2}\right)\right\\}}_{:=\tau_{6}}\\\
&+\alpha_{\mathrm{o}}\tilde{\alpha}_{\mathrm{e}}\underbrace{\sum_{n=0}^{N-1}\exp\left\\{j\frac{2\pi}{N}n\left(\alpha_{2}-\beta_{1}\right)\right\\}}_{:=\tau_{7}}\\\
&+\alpha_{\mathrm{o}}\tilde{\alpha}_{\mathrm{o}}\underbrace{\sum_{n=0}^{N-1}\exp\left\\{j\frac{2\pi}{N}n\left(\alpha_{2}-\beta_{2}\right)\right\\}}_{:=\tau_{8}},\end{split}$
(12)

where $\alpha_{1}:=k_{\mathrm{e}}+n$, $\alpha_{2}:=k_{\mathrm{o}}+n$,
$\beta_{1}:=\tilde{k}_{\mathrm{e}}+n$ and
$\beta_{2}:=\tilde{k}_{\mathrm{o}}+n$. Using the same property as in (10)
leads to $\tau_{5}=\tau_{6}=\tau_{7}=\tau_{8}=0$, therefore, $\langle
s(n),\tilde{s}(n)\rangle=0$.

#### Case IV: $s(n)=f(n)c_{\mathrm{d}}(n)$ and
$\tilde{s}(n)=\tilde{f}(n)c_{\mathrm{u}}(n)$

In this case, we have

$\begin{split}\langle
s(n),\tilde{s}(n)\rangle&=\alpha_{\mathrm{e}}\tilde{\alpha}_{\mathrm{e}}\overline{\tau}_{5}+\alpha_{\mathrm{e}}\tilde{\alpha}_{\mathrm{o}}\overline{\tau}_{6}+\alpha_{\mathrm{o}}\tilde{\alpha}_{\mathrm{e}}\overline{\tau}_{7}+\alpha_{\mathrm{o}}\tilde{\alpha}_{\mathrm{o}}\overline{\tau}_{8}=0.\end{split}$
(13)

Thus, it can be concluded that the DM-CSS symbols are always orthogonal and
the PSs do not impact the orthogonality of the symbols.

##  III Comparison with Other LoRa Variants

In this section, we evaluate and compare the performance of the DM-CSS against
LoRa, ePSK-LoRa, SSK-ICS-LoRa, GCSS, and DCRK-CSS. We consider ePSK-
LoRa$(2,4)$ because of its resilience against the phase offset (PO) and
frequency offset (FO). GCSS with $\mathrm{G}=2$ is optimal in terms of EE and
resilience to FO and PO; therefore, GCSS with only two groups is considered.
Moreover, DCRK-CSS with $M_{\mathrm{c}}=8$ is considered because of complexity
issues. The performance of these schemes is evaluated in terms of (i) SE
requirement versus required SNR/bit; (ii) BER performance in AWGN channel and
fading channels; (iii) BER performance in AWGN considering PO; and (v) BER
performance in AWGN considering FO.

###  III-A Spectral Efficiency vs. Required SNR Per Bit

Fig. 1 compares the SE versus required SNR/bit performance of DM-CSS with
other alternatives considering non-coherent detection in AWGN. SE is changed
by varying $\lambda=\llbracket 6,12\rrbracket$. Moreover, the EE is
ascertained by evaluating the required
$E_{\mathrm{b}}/N_{0}=\nicefrac{{(E_{\mathrm{s}}T_{\mathrm{s}})}}{{(\eta_{\mathrm{DM-
CSS}}N_{0})}}$ needed to attain BER of $10^{-3}$ over $10^{6}$ Monte Carlo
runs. Here, $N_{0}$ is the mono-lateral noise spectral density. The spectral
efficiencies of DM-CSS and other counterparts are summarized in Table I. It is
evident that DM-CSS has the highest achievable SE which clearly demonstrates
its superiority in achieving maximum throughput.

From Fig.1, we observe that DM-CSS provides the best trade-off between the
achievable SE and required $E_{\mathrm{b}}/N_{0}$. The modulation performance
that coincides with that of DM-CSS is ePSK-LoRa($2,4$). However, it is evident
that DM-CSS provides a relative SE increase of $\nicefrac{{(\lambda-2)}}{{M}}$
bits/s/Hz $\forall~{}\lambda$ over ePSK-LoRa($2,4$). We can also observe that
the performance of other alternatives, such as GCSS and DCRK-CSS are similar
to each other and are better than SSK-ICS-LoRa.

Figure 1: SE versus required SNR per bit for different schemes considering
non-coherent detection and target BER of $10^{-3}$ in AWGN channel.

###  III-B Bit Error Rate Performance in AWGN and Fading Channels

Next, we evaluate the performance of the discussed schemes considering an
ideal linear AWGN and fading channels considering $\lambda=9$. These results
are illustrated in Fig. 2. From Fig. 2, we can observe that in AWGN channel,
the performance of DM-CSS is better than LoRa, SSK-ICS-LoRa, GCSS and DCRK-
CSS, whereas, its performance is almost similar to that of ePSK-LoRa$(2,4)$.
Thus, it is evident that one can use less energy to transmit more information
with lower bit error probability when employing DM-CSS over other
counterparts. We can observe that DM-CSS requires $1$ dB less
$E_{\mathrm{b}}/N_{0}$ compared to LoRa at BER of $10^{-3}$. On the other
hand, for the same target BER, DM-CSS offers $0.5$ dB improvement over GCSS
and SSK-ICS-LoRa, and its gain over DCRK-CSS is around $0.3$ dB.

We consider a frequency-selective $2$-tap fading channel having an impulse
response of $h(n)=\sqrt{1-\rho}\delta(nT)+\sqrt{\rho}\delta(nT-T)$, where $T$
is the sampling duration and $0\leq\rho\leq 1$. The results are also depicted
in Fig. 2, where $\rho=0.3$. It has been demonstrated that DM-CSS provides the
best performance relative to other counterparts. An important aspect to
highlight here is that the performance of ePSK-LoRa($2,4$) which is similar to
that of DM-CSS in an ideal AWGN channel, deteriorates considerably in the
fading channel.

Figure 2: BER performance for different schemes considering non-coherent
detection in AWGN channel for $\lambda=9$.

###  III-C Bit Error Performance under Phase Offset

In this section, we analyze the performance of DM-CSS considering PO, which is
expected to exist in low-cost devices. To this end, the received symbol
corrupted by PO and AWGN is given as $\exp\\{j\psi\\}s(n)+w(n)$, where $\psi$
is the PO, and $w(n)$ are the samples of AWGN. Considering non-coherent
detection, PO of $\psi=\nicefrac{{\pi}}{{8}}$ and $\lambda=9$, the BER
performance is presented in Fig. 3. We observe that the performance of DCRK-
CSS, SSK-ICS-LoRa and LoRa are most robust because they do not incorporate any
information in the PS of the transmit symbol. On the other hand, DM-CSS, ePSK-
LoRa$(2,4)$ and GCSS suffer from the PO because either multiple chirps are
simultaneously multiplexed, or the symbols carry additional information in the
PS of the transmit symbols. Nonetheless, the performance of DM-CSS is still
acceptable, bearing in mind that DM-CSS transmits maximum number of bits,
compared to other schemes. A BER penalty of $0.6$ dB is observed for DM-CSS
considering PO of $\psi=\nicefrac{{\pi}}{{8}}$ relative to when $\psi=0$.

Figure 3: BER performance for different schemes considering non-coherent
detection, $\psi=\nicefrac{{\pi}}{{8}}$, AWGN channel, and $\lambda=9$.

###  III-D Bit Error Performance under Frequency Offset

The BER performance of DM-CSS considering the influence of carrier FO is
provided in Fig. 4. The received symbol incorporating the impact of FO is
$\exp\\{\nicefrac{{j2\pi\Delta fn}}{{N}}\\}s(n)+w(n)$. Carrier FO accumulates
phase rotation sample-by-sample in the symbol. To attain Fig. 4, we use
$\Delta f=0.1$ and $\lambda=9$. We observe that the performance of DM-CSS is
marginally better than ePSK-LoRa($2,4$) and SSK-ICS-LoRa. DCRK-CSS exhibits
the best performance, whereas, the BER performance of LoRa and GCSS
considering the influence of FO is agnostic.

Figure 4: BER performance for different schemes considering non-coherent
detection, $\Delta f=0.1$, AWGN channel, and $\lambda=9$.

###  III-E Advantages and Disadvantages of DM-CSS

Some observable advantages of DM-CSS are: (i) higher achievable SE over other
alternatives; (ii) improved EE relative to state-of-the-art schemes; (iii) the
impact of FO is the lowest for DM-CSS among DM-CSS, ePSK-LoRa($2,4$) and GCSS;
and (iv) DM-CSS provides the best performance in frequency-selective $2$-tap
fading channels. Nonetheless, there are some distinctive disadvantages as well
such as: (i) the performance of DM-CSS, ePSK-LoRa($2,4$) and GCSS is
negatively impacted under the influence of PO and FO (roughly $0.6$ dB and
$0.8$ dB considering ($\psi=\nicefrac{{\pi}}{{8}}$) and ($\Delta f=0.1$),
respectively), whereas the performance of LoRa, SSK-ICS-LoRa, DCRK-CSS is
somewhat agnostic; (ii) DM-CSS does not possess the constant envelope
property, therefore, peak-to-average power ratio (PAPR) could be a concern at
some stage of system realization; and (iii) the detector involves two ML
criteria to decode $\hat{\alpha}_{\mathrm{e}}$ and
$\hat{\alpha}_{\mathrm{o}}$, that adds complexity to the receiver design.

It is highlighted that the primary reason for BER degradation of schemes under
PO and FO is either because multiple chirps are multiplexed to increase the
achievable rate or due to additional information being transmitted via the PS
of the chirped symbol. However, the schemes that transmit only one chirp, such
as LoRa, SSK-ICS-LoRa, DCRK-CSS, achieve relatively lower bit rates. Anyhow,
the superiority of DM-CSS is also evident from the fact that it is reasonably
resilient against FO and PO and attains the highest achievable SE among the
considered approaches.

##  IV Conclusions

In this letter, we proposed DM-CSS that is capable of substantially improving
the SE relative to other state-of-the-art alternatives. A non-coherent
detection process is succinctly explained. The proposed scheme was shown to
outperform LoRa, SSK-ICS-LoRa, GCSS and DCRK-CSS in terms of EE/BER over an
AWGN channel for different $\lambda$. The performance of DM-CSS was found to
be among the best in a fading channel. We also derived mathematical
formulations to prove the orthogonality of DM-CSS symbols. Furthermore, the
resilience of DM-CSS against PO and FO impairments have been demonstrated. It
is foreseen that the achievable SE of DM-CSS can be enhanced using different
chirp rates as in DCRK-CSS. Such design is left out as a possible topic for
future research.

## References

  * [1] L. Vangelista.  Frequency shift chirp modulation: The LoRa modulation.  IEEE Sig. Process. Lett., 24(12):1818–1821, 2017.
  * [2] R. Bomfin, M. Chafii, and G. Fettweis.  A novel modulation for IoT: PSK-LoRa.  In IEEE Veh. Technol. Conf., pages 1–5. IEEE, 2019.
  * [3] A. W. Azim, J. L. G. Monsalve, and M. Chafii.  Enhanced PSK-LoRa.  IEEE Wire. Commun. Lett., 11(3):612–616, 2022.
  * [4] M. Hanif and H. H. Nguyen.  Slope-Shift Keying LoRa-Based Modulation.  IEEE Internet Things J., 8(1):211–221, 2020.
  * [5] T. Elshabrawy and J. Robert.  Interleaved chirp spreading lora-based modulation.  IEEE Internet Things J., 6(2):3855–3863, 2019.
  * [6] A. Mondal, M. Hanif, and H. H. Nguyen.  SSK-ICS LoRa: A LoRa-based modulation scheme with constant envelope and enhanced data rate.  IEEE Commun. Lett., pages 1–1, 2022.
  * [7] Q. Yu, H. Wang, Z. Lu, and S. An.  Group-Based CSS Modulation: a novel enhancement to lora physical layer.  IEEE Wire. Commun. Lett., 11(3):660–664, 2022.
  * [8] I. Bizon Franco de Almeida, M. Chafii, A. Nimr, and G. Fettweis.  Alternative chirp spread spectrum techniques for lpwans.  IEEE Trans. Green Commun. Netw., 5(4):1846–1855, 2021.
  * [9] L. Vangelista and A. Cattapan.  A new LoRa-compatible modulation improving the LoRaWAN network level performance.  In IEEE Latin-American Conf. Commun., pages 1–6, 2019.