Generic Model Checking for
Modal Fixpoint Logics in

Daniel Hausmann0000-0002-0935-86021Funded by the ERC Consolidator grant D-SynMA (No.
772459) Merlin Humml0000-0002-2251-85192Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 377333057 and 393541319/GRK2475/1-2019 Simon Prucker0009-0000-2317-55652 Lutz Schröder0000-0002-3146-59062Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 419850228 Aaron Strahlberger2

D. Hausmann, M. Humml, S. Prucker, L. Schröder, A. Strahlberger

University of Gothenburg, Sweden Friedrich-Alexander-Universität Erlangen-Nürnberg,

We report on , a model checking tool for fixpoint logics that
is parametric in the branching type of models (non-deterministic,
game-based, probabilistic etc.) and in the next-step modalities used
in formulae. The tool implements generic model checking algorithms
developed in coalgebraic logic that are easily adapted to concrete
instance logics. Apart from the standard modal $\mu$-calculus,
currently supports alternating-time, graded, probabilistic
and monotone variants of the $\mu$-calculus, but is also effortlessly
extensible with new instance logics.  The model checking process is
realized by polynomial reductions to parity game solving, or,
alternatively, by a local model checking algorithm that
directly computes the extensions of formulae in a lazy fashion,
thereby potentially avoiding the construction of the full parity game. We
evaluate on informative benchmark sets.

§ INTRODUCTION

The $\mu$-calculus [24] is one of the most expressive logics
for the temporal verification of concurrent systems. Model checking
the $\mu$-calculus is equivalent to parity game solving, and as such
enjoys diversified tool support in the shape of both well-developed
parity game solving suites such as PGSolver [11, 38] or
Oink [7] and dedicated model checking tools such as
mCRL2 [3]. While the $\mu$-calculus is standardly
interpreted over relational transition systems, a wide range of
alternative flavours have emerged whose semantics is variously based
on concurrent games as in the alternating-time
$\mu$-calculus [2]; on probabilistic transition systems as
in the (two-valued) probabilistic
$\mu$-calculus [5, 29, 4]; on
counting successors as in the graded
$\mu$-calculus [25]; or on neighbourhood structures as
in the monotone $\mu$-calculus, the ambient fixpoint logic of game
logic [31, 33, 8]. Model checking tools
for such $\mu$-calculi are essentially non-existent or limited to
fragments (see additional comments under `related work'). We present
the generic model checker , which implements generic model
checking algorithms for the coalgebraic
$\mu$-calculus [5] developed in previous
work [22]. The coalgebraic
$\mu$-calculus is based on the semantic framework of coalgebraic
logic, which treats systems generically as coalgebras for a set
functor encapsulating the system type, following the paradigm of
universal coalgebra [35], and
parametrizes the semantics of modalities using so-called
predicate liftings [32, 36]. By fairly
simple instantiation to concrete logics, thus serves as the
first available model checker for the probabilistic $\mu$-calculus,
the graded $\mu$-calculus, and the full alternating-time
$\mu$-calculus AMC (model checking tools for alternating-time temporal
logic ATL, a fragment of the AMC, do exist, as discussed further
below). Besides presenting the tool itself and discussing
implementation issues, we conduct an experimental evaluation of on benchmark series of parity games [11, 38] that we adapt to
the generalized coalgebraic setting. We thus show that scales
even on series of problems designed to be hard in the relational base

*Related Work
As mentioned above, is the only currently available model
checker for most of the logics that it supports, other than the standard
modal $\mu$-calculus (and the main point of its genericity is that
support for further logics can be added easily). We refrain from benchmarking against modal $\mu$-calculus model checkers (e.g. mCRL2 [3]) as this would essentially amount to comparing the respective backend parity game solvers. Model checking tools
for alternating-time temporal logic ATL [2] do exist, such
as MOCHA [1],
MCMAS [30], and
UMC4ATL [23], out of which MCMAS appears to be the
fastest one currently available [23]. We do compare
to MCMAS on two benchmarks, confirming that MCMAS is faster on
ATL. Note however that ATL model checking works along essentially the
same lines as for CTL, and as such is much simpler than model checking
the alternating-time $\mu$-calculus AMC (e.g., it does not require
parity conditions, and unlike AMC model checking it is known to be
in PTime [2]), so it is expected that dedicated
ATL model checkers will be faster than an AMC model checker like on ATL. Local solving has been shown to be advantagous in
model checking for the relational $\mu$-calculus [37]
and for standard parity
games [12].

uses the basic infrastructure, such as parsers and data
structures for formulae, of the Coalgebraic Ontology Logic
Solver (COOL/COOL 2) [13, 14], a
generic reasoner aimed at satisfiability checking rather than model
checking. The algorithms we use
here [22] improve on either the
theoretical complexity or the complexity analysis of previous model
checking algorithms for concrete instance logics including the
alternating-time [2], graded [10], and
monotone [16] $\mu$-calculi, as well as of a previous
generic model checking algorithm for the coalgebraic
$\mu$-calculus [18];
see [22] for details.

§ MODEL CHECKING FOR THE COALGEBRAIC $\MU$-CALCULUS

We briefly recall the syntax and semantics of the the
underlying generic logic of , the coalgebraic
$\mu$-calculus [5], and subsequently sketch two
different model checking algorithms implemented for this logic in
, a local algorithm that directly computes extensions of
formulae, and a more global algorithm that reduces instances of the
model checking problem to parity
games [22].

Formulae of the coalgebraic $\mu$-calculus are given by the
following grammar, parametrized over a choice of countable
sets $\Lambda$ and $\Vars$ of modalities and (fixpoint)
variables, respectively.

\begin{gather*}
\varphi, \psi ::= \top \mid \bot \mid \varphi \land \psi
\mid \varphi \lor \psi \mid \hearts\varphi\mid X\mid
\nu X.\,\varphi \mid     \mu X.\,\varphi
\end{gather*}

where $X\in\Vars$; we assume that $\Lambda$ contains, for each
modality $\hearts\in\Lambda$, also the dual $\overline{\hearts}$ (with
$\overline{\overline{\hearts}}=\hearts$).  The logic generalizes the
standard $\mu$-calculus by supporting arbitrary monotone modalities
$\hearts$ in place of $\Diamond$ and $\Box$, assuming that the
semantics of $\hearts$ can be defined in the framework of coalgebraic
logic, recalled below.

To ensure monotonicity, the logic
does not contain negation as an explicit operator; however, negation
of closed formulae can, as usual, be defined via negation normal

Given a formula $\varphi$, we let $|\varphi|$ denote its syntactic
size. The algorithms we use work on the (Fischer-Ladner)
closure $\mathsf{cl}(\varphi)$ of $\varphi$, a succinct graph
representation of the respective formula, intuitively obtained from
its syntax tree by identifying occurrences of fixpoint variables with
their binding fixpoint operators; we have
$|\mathsf{cl}(\varphi)|\leq |\varphi|$ [24].  The
alternation-depth $\mathsf{ad}(\varphi)$ of fixpoint formulae
$\varphi=\eta X.\,\psi$ is defined in the usual way as the number of
dependent alternations between least and greatest fixpoints
in $\varphi$; for a detailed account, see [26].

The semantics of the coalgebraic $\mu$-calculus is parametrized over
the choice of a set functor $\mathcal{F}$ that encapsulates the
branching type of systems, e.g. nondeterministic
($\mathcal{F}X=\mathcal{P}X$, the powerset of $X$) or probabilistic
($\mathcal{F}X=\mathcal{D}X$, the set of discrete probability
distributions on $X$). Formulae are then evaluated over
coalgebras $(C,\xi:C\to \mathcal{F}C)$ for $\mathcal{F}$, that
is, over generalized transition systems consisting of a set $C$ of
states and transition function $\xi$ that associates to each
state $c$ a collection $\xi(c)\in \mathcal{F}C$ of observations and
successors, structured according to $\mathcal{F}$. For the most basic
case, we can pick $\mathcal{F}=\mathcal{P}$ to be the powerset
functor, so that $\mathcal{F}$-coalgebras are standard transition
systems, with $\xi(c)\in\mathcal{P}C$ being the set of successor states
of $c$.

The semantics of modalities $\hearts\in\Lambda$ is defined in terms of
so-called predicate liftings, that is, functions
$\sem{\hearts}$ that lift predicates $D\subseteq C$ on $C$ to
predicates $\sem{\hearts}(D)\in \Pow(\mathcal{F}C)$ on
$\mathcal{F}C$. A state $c\in C$ in a coalgebra $(C,\xi)$ then
satisfies a formula $\hearts\psi$ if
$\xi(c)\in\sem{\hearts}(\sem{\psi})$ where $\sem{\psi}$ is the set of
states that satisfy $\psi$.

This concept instantiates to the standard modalities $\Diamond$ and
$\Box$ over transition systems (that is, over coalgebras
$(C,\xi:C\to\Pow C)$ for the functor $\Pow$) by taking predicate

\begin{align*}
\sem{\Diamond}(D)&=\{E\in\Pow C\mid E\cap D\neq\emptyset\} &
\sem{\Box}(D)&=\{E\in\Pow C\mid E\subseteq D\}.
\end{align*}

For another example, consider graded modalities of the shape
$\langle n \rangle $ and $[ n ] $ (for $n\in\mathbb{N}$), expressing
that more than $n$ successors or all but at most $n$ successors,
respectively, satisfy the argument formula.  We interpret such
modalities over graded transition systems, in which every
transition from one state to another is equipped with a non-negative
integer multiplicity; these are coalgebras
$(C,\xi:C\to \mathcal{G}C)$ for the multiset
functor $\mathcal{G}$ that maps a set $X$ to the set $\mathcal{G}X$
of finite multisets over $X$, represented as maps $X\to\mathbb{N}$
with finite support [6]. For $\theta:C\to\mathbb{N}$ and $D\subseteq C$,
we put $\theta(D)=\Sigma_{d\in D}\theta(d)$, and interpret
$\langle n \rangle $, $[ n ] $ as the predicate liftings

\begin{align*}
\sem{\langle n \rangle}(D)&=\{\theta\in \mathcal{G}C\mid \theta(D)>n\} &
\sem{[n]}(D)&=\{\theta\in \mathcal{G}C\mid \theta(C\setminus D)\leq n\}.
\end{align*}

Having defined the semantics of single modal steps, we now extend the
semantics to the full logic, introducing the game-based
semantics of the coalgebraic $\mu$-calculus (which is equivalent to
a recursively defined algebraic
semantics [39, 22, 21]). To
treat least and greatest fixpoints correctly, this semantics uses
parity games, which are infinite-duration games played by two
players $\exists$ and $\forall$. A
parity game \(G= (V,V_{\exists}, E,\Omega)\) consists of a set $V$ of
positions, with positions $V_{\exists}\subseteq V$ owned by $\exists$
and the others by $\forall$, a move relation
$E\subseteq V\times V$, and a priority function
\(\Omega\colon V\to \mathbb{N}\) that assigns a natural number
$\Omega(v)$ to each position $v\in V$.  A play is a path in the
directed graph $(V,E)$ that is either infinite or ends in a node
$v\in V$ with no outgoing moves. Finite plays \(v_0v_1\dots v_n\) are
won by $\exists$ if and only if \(v_n\in V_{\forall}\) (i.e. if
$\forall$ is stuck); infinite plays are won by $\exists$ if and only
if the maximal priority that is visited infinitely often is even.

A (history-free) $\exists$-strategy is a
partial function \(s\colon V_\exists\rightharpoonup V\) that assigns
moves to $\exists$-nodes.  A play follows a strategy \(s\) if
for all \(i\geq 0\) such that \(v_i\in V_{\exists}\),
\(v_{i+1}=s(v_i)\).  An $\exists$-strategy wins a node
\(v\in V\) if $\exists$ wins all plays that start at \(v\) and follow
\(s\).

For the remainder of the paper, we fix a functor $\mathcal{F}$,
an $\mathcal{F}$-coalgebra $(C,\xi)$, a set $\Lambda$ of
modalities with associated monotone predicate liftings, and
a formula $\chi$ (that uses modalities from $\Lambda$);
further we let $\mathsf{cl}=\mathsf{cl}(\chi)$ denote the
closure of $\chi$, and put $n:=|\mathsf{cl}|$ and $k:=\mathsf{ad}(\chi)$.

The model checking game $G_{(C,\xi),\chi}=(V,V_\exists,E,\Omega)$ is
the parity game defined by the following table, where game nodes
$v\in V=V_\exists\cup V_\forall$ are of the shape
$v=(c,\psi)\in C\times \mathsf{cl}$ or
$v=(D,\psi)\in \Pow(C)\times \mathsf{cl}$.

node     owner     set of allowed moves

$(c,\top)$     $\forall$     $\emptyset$

$(c,\bot)$     $\exists$     $\emptyset$

$(c,\varphi\land\psi)$     $\forall$     $\{(c,\varphi),(c,\psi)\}$

$(c,\varphi\lor\psi)$     $\exists$     $\{(c,\varphi),(c,\psi)\}$

$(c,\eta X.\,\psi)$     $\exists$     $\{(c,\psi[\eta X.\,\psi/X])\}$

$(c,\hearts\psi)$     $\exists$     $\{(D,\psi)\mid \xi(c)\in\sem{\hearts}(D)\}$

$(D,\psi)$     $\forall$     $\{(d,\psi)\mid d\in D\}$

In order to show satisfaction of $\hearts\psi$ at $c\in C$,
player $\exists$ thus has to claim satisfaction of $\psi$ at a
sufficiently large set $D\subseteq C$ of states; player $\forall$ in
turn can challenge the satisfaction of $\psi$ at any node $d\in D$.

As usual in $\mu$-calculi, the priority function $\Omega$ serves to
detect that the outermost fixpoint that is unfolded infinitely
often is a greatest fixpoint. It is thus defined ensuring that for
nodes $(c,\varphi)$, $\Omega(c,\varphi)$ is even if
$\varphi=\nu X.\,\psi$, odd if $\varphi=\mu X.\,\psi$, and
$\Omega(c,\varphi)=0$ otherwise, and moreover that larger numbers are
assigned to outer fixpoints, using the alternation depth of

The formal definition of $\Omega$ follows
the standard method, see e.g. [26].

We say that $c\in C$ satisfies $\chi$ (denoted $(C,\xi),c\models \chi$)
if and only if player $\exists$ wins the position $(c,\chi)$ in $G_{(C,\xi),\chi}$.
The model checking problem for the coalgebraic $\mu$-calculus consists in deciding, for state $c\in C$ in a coalgebra $(C,\xi)$, and formula $\chi$ of the
coalgebraic $\mu$-calculus, whether $(C,\xi),c\models\chi$.

We point out that $G_{(C,\xi),\chi}$ is a parity game with $k$ priorities
that contains up to $n\cdot 2^{|C|}$ positions of the form $(D,\psi)$ for
$D\subseteq C$. Therefore it is not feasible to perform model checking
by explicitly constructing and solving this parity game. In previous
work [22, 20], we have shown that the model
checking problem for the coalgebraic $\mu$-calculus is in
$\textsc{NP}\cap\textsc{co-NP}$ and in $\textsc{QP}$ (under mild
assumptions on the complexity of evaluating single modal steps using
the predicate liftings), providing two methods to circumvent the
explicit construction of the full game:

* Compute the winning region in $G_{(C,\xi),\chi}$ as a nested fixpoint over the set
of positions of the shape $(c,\psi)$; intuitively, this avoids the explicit construction of the intermediate positions of the shape $(D,\psi)$ by directly computing the extension of
subformulae over $C$. This solution is generic in the sense that it works for any instance of the coalgebraic $\mu$-calculus.

* Provide a polynomial-sized game-characterization of the
modalities of the concrete logic at hand, enabling a polynomial
reduction of the model checking problem to solving parity
games. This makes it possible to use
parity game solvers, but relies on the logic-specific
game characterization of the modalities.

As part of this work, we have implemented and evaluated both methods as an extension of the
reasoner COOL, as described next.

§ IMPLEMENTATION – MODEL CHECKING IN

We report on the implementation of model checking for the coalgebraic
$\mu$-calculus within the framework provided by the COalgebraic
Ontology Logic solver (COOL), a coalgebraic reasoner for modal
fixpoint logics [13], implemented in
OCaml.  The satisfiability-checking capacities of COOL have been
reported elsewhere [14]. Our tool extends this
framework with comprehensive functionality for model checking, along
the lines of <ref>.  To this end, we use existing
infrastructure and data structures of COOL for parsing and
representing (the closure of) input formulae $\chi$ for an extensible
selection of logics, induced by the choice of a set functor
$\mathcal{F}$; a newly added parser reads input models
$(C,\xi:C\to\mathcal{F}(C))$ in the form of coalgebras for the
selected functor (more details on the introduced specification
format for coalgebras can be found in the artifact [19]).
We thus obtain model checking support for

* the standard modal $\mu$-calculus (including its fragment CTL) [24],

* the monotone $\mu$-calculus (including its fragment game
logic) [31, 33, 8],

* the alternating-time $\mu$-calculus (including its fragment ATL) [2],

* the graded $\mu$-calculus [25],

* the probabilistic $\mu$-calculus [5, 29, 4].

By the relation between $\mu$-calculus model checking and the solution of games
with parity conditions, made more precise in <ref> below,
can also be seen as a generic qualitative solver for (standard, monotone, alternating-time, graded and probabilistic) parity games.

The core model checking functionality is provided by implementations
of the two approaches described in <ref>: On the one
hand, we implement the direct evaluation of formulae in the form of a
generic local model checking algorithm; on the other hand, we
also implement a polynomial reduction to standard parity games
for each of the logics currently supported. Below, we provide intuitive
explanations of the two algorithms, pointing out concrete implementational details
only where the implementation is not straight-forward.

Local Model Checking.

The local model checking algorithm follows the ideas of [22]
directly encoding the one-step evaluation of formulae $\psi\in\mathsf{cl}$
by means of functions $\mathsf{eval}_\psi:\Pow(C\times\mathsf{cl})\to \Pow(C\times\mathsf{cl})$, corresponding to all moves in the model checking game that evaluate $\psi$
at some state.
For instance, we have

\begin{align*}
\mathsf{eval}_{\varphi\lor\psi}(X)&=\{(c,\varphi\lor\psi)\mid (c,\varphi)\in X\text{ or }(c,\psi)\in X\}\\
\mathsf{eval}_{\hearts\psi}(X)&=\{(c,\hearts\psi)\mid \xi(c)\in\sem{\hearts}(\{d\mid (d,\psi)\in X\})\}
\end{align*}
$X\subseteq C\times\mathsf{cl}$, and similar functions for the remaining operators; intuitively, $\mathsf{eval}_\psi(X)$ computes the
set of positions in the model checking game that have formula component $\psi$ and are won by player $\exists$, assuming that it is already known that $\exists$ wins all positions in $X$. Crucially, the evaluation function for
modal operators skips the exploration of the
intermediate nodes $(D,\psi)$ in the model checking game by directly evaluating
the predicate lifting over the set $X$.

Then we can compute the winning regions in the model checking game as nested fixpoints
of the one-step solving function:

\begin{align*}
\mathsf{win}_\exists &= \mu X_k.\,\nu X_{k-1}.\,\ldots.\,\nu X_0. \cup_{\psi\in\mathsf{cl}}\mathsf{eval}_\psi(X_{\Omega(\psi)})\\
\mathsf{win}_\forall &= \nu X_k.\,\nu X_{k-1}.\,\ldots.\,\mu X_0. \cup_{\psi\in\mathsf{cl}}{\mathsf{eval}_{\neg\psi}}(X_{\Omega(\psi)}),
\end{align*}

assuming w.l.o.g. that $k$ is odd, and denoting by $\Omega(\psi)$ the
priority of all game nodes of the shape $(c,\psi)$;
thus the functions below the fixpoints directly
correspond to the functions $f$, $g$ from [22], Definition 5, noting that $\Omega(\psi)=0$
whenever $\psi$ is not a fixpoint formula.
We implement this game solving procedure

by a higher order function that receives the semantic function for
modalities as an argument, and then computes
the relevant fixpoints by Kleene fixpoint iteration.

The overall local model checking implementation then builds the model checking
game step by step, starting from the initial position $(c,\varphi)$ and adding nodes to
which the respective player can move; crucially, the evaluation functions for
modalities allow us to skip all nodes
of the form $(D,\psi)$ during the exploration of the game arena.
At any point during the game construction, the algorithm can attempt to solve
the partially constructed game by computing the fixpoints defined above, allowing it (in some cases) to finish early, that
is, before the whole search space has been explored; this constitutes the local nature
of the algorithm in the sense that satisfaction of a formula may be proved or refuted
without traversing the whole model.

Parity Game Model Checking.

Relying on polynomial reductions of modality evaluation
to game fragments [22], we implement
the generation of model checking parity games in by a higher
order function which traverses the input model and formula and
translates all connectives into game nodes as described in
<ref>, interpreting modal operators using a function it
receives as an argument.  The parity game thus constructed then can be
solved using any parity game solver (including an unoptimized native
solver provided by the framework); the current version of
uses PGSolver as external parity game solver
(support for Oink is planned).

The subgames that evaluate individual modalities in this construction
are specific to the logic at hand.
Due to space restrictions, we provide sketches of the reductions for two
central logics here
and refer to [22], Example 15 for full details.
For the standard $\mu$-calculus, we
have modal positions $(c,\Diamond \psi)$ (or $(c,\Box \psi)$), for
which the one-step evaluation games just consist of that single
position controlled by player $\exists$ (or $\forall$), with moves to
all positions $(d,\psi)$ such that $d\in\xi(c)$.  The evaluation games
for, e.g., graded modalities are significantly more involved: For
instance, from a position $(c,\langle n\rangle \psi)$, the game
proceeds in layers, with one layer for each $d\in C$ to which $c$ has
an edge with multiplicity at least $1$. In each layer, player
$\exists$ decides whether or not to include $d$ in the set of states
that she claims to satisfy $\psi$; all game positions also contain a
counter that keeps track of the joint multiplicities of all successors
included so far. Player $\exists$ wins the subgame as soon as this counter
exceeds $n$ but loses when the subgame exits the final layer while the
counter is still below $n$. Additionally, player $\forall$ can choose,
for any state $d$ that player $\exists$ decides to use, to either
challenge the satisfaction of $\psi$ at $d$ by continuing the model
checking game a position $(d,\psi)$, or accept the choice of $d$ and
proceed to the next layer of the local game, increasing the counter by
the multiplicity of $d$ as a successor of $c$.

§ EXPERIMENTAL EVALUATION OF THE IMPLEMENTATION

We experimentally evaluate the performance of our two generic model
checking implementations for all logics currently supported. The main
interest in lies in its genericity, which enables it to cover
a wide range of logics not supported by other tools, so comparison to
other tools is mostly omitted for lack of competitors; additional
discussion is provided below.

Generalized parity games. As we have seen above, model
checking for (coalgebraic) $\mu$-calculi reduces to solving parity
games. Conversely, parity games can also be solved by model checking:
It is well known that player $\exists$ wins a node $v\in V$ in a
parity game with $k$ priorities if and only if $v$ satisfies the

\[ \chi_k := \mu X_{k}.\,\nu X_{k-1} \dots \mu X_1.\, \nu X_0.\,
\textstyle\bigvee_{0 \le i \le k} \Omega^{-}(i)\land
((V_\exists\land\hearts X_i) \lor (V_\forall\land\overline{\hearts}
where $\Omega^{-}(i)=\{v\in V\mid\Omega(v)=i\}$,
$\hearts=\Diamond$ and $\overline{\hearts}=\Box$ and
$k$ is w.l.o.g. assumed to be odd.  We
exploit this characterization to lift benchmarking problems for
standard parity games to a coalgebraic level of generality: A parity
game is essentially a Kripke structure with propositional atoms for
priorities and player ownership, that is, a coalgebraic model based
(for transitions) on the powerset functor $\mathcal{P}$. We generalize
this situation by replacing $\mathcal{P}$ with other
functors $\mathcal{F}$, and $\Diamond,\Box$ with suitable pairs
$\hearts,\overline{\hearts}$ of dual modalities. In order to win the
resulting generalized game, player $\exists$ then requires a strategy
that picks, at each game node $v$, a set of successors that satisfies
$\hearts$ if $v\in V_\exists$ or $\overline{\hearts}$ if
$v\in V_\forall$; e.g. in the case of standard games player $\exists$
has to pick a single successor at their nodes ($\hearts=\Diamond$),
while they have to allow all successors at nodes belonging to
$\forall$ ($\overline{\hearts}=\Box$). Furthermore, all plays adhering
to such a strategy have to satisfy the parity condition. We then
systematically enrich given standard parity games to supply additional
functor-specific transition structure in a deterministic way to strike a balance between making the games much harder or much easier than the original game while still making use of the added structure; in our leading examples, we
proceed as follows:

* For the monotone $\mu$-calculus, we construct monotone
parity games; concretely, we build monotone neighbourhood
structures $N$ (e.g. [31]; these are coalgebras for
the monotone neighbourhood functor [15]), in
which two consecutive steps in the original parity game $G$ are
merged so that a single step in $N$ corresponds to the evaluation of
two-step strategies in $G$, that is, we define $\xi(v)$ to be the
set $\{D_1,\ldots,D_m\}$ of (minimal) neighbourhoods
$D_i\subseteq V$ such that the owner of $v$ has a strategy in $G$ to
ensure that starting from $v$ and playing two steps, some node from
$D_i$ is reached. Then, $\Diamond\varphi$ essentially says
that $\exists$ can enforce $\varphi$ (in two steps), while $\Box\varphi$
says that $\exists$ cannot prevent $\varphi$.

* For the graded $\mu$-calculus (<ref>), we
construct graded parity games by equipping moves in $G$ with
multiplicities summing up to at least $10$ at each
node, that is, we assign multiplicity
$(\xi(v))(u)=\lceil10 \div E(v)\rceil$ to each successor
$u\in E(v)$
of $v$ in $G$.
Then we take \(\hearts = \CLdia{5}, \overline{\hearts}=\CLbox{5}\),
so to win in the graded parity game, player $\exists$ requires a
strategy that picks more than five moves, counting multiplicities,
at $\exists$ nodes, and all but at most five moves at $\forall$

* For the two-valued probablistic $\mu$-calculus, we construct
qualitive stochastic parity games by imposing a uniform
distribution on the moves, thus obtaining probabilistic
transition systems, which are coalgebras for the
distribution functor that assigns to a set $X$ the set of
(discrete) probability distributions on $X$.  Then we take
\(\hearts = \CLdia{\frac{1}{2}},
\overline{\hearts}=\CLbox{\frac{1}{2}}\) where $\CLdia{p}$ is read
“with probability more than $p$”, so player $\exists$ wins the
resulting stochastic parity game if they have a strategy that in
each $\exists$-move stays within the winning region with probability
more than $\frac{1}{2}$, and forces $\forall$ to stay within
$\exists$'s winning region with probability at least $\frac{1}{2}$.

We apply the above constructions to various established parity game
benchmarking series, and in each case evaluate the respective variant
of the formula $\chi_k$, thereby solving the respective monotone,
graded, or probabilistic variants of the game.  Specifically, we use
series of clique games, ladder games, Jurdzinski
games, Towers of Hanoi games, and language inclusion
games generated by the parity game solver
PGSolver [11, 38].

Lazy games.
To illustrate the potential advantages of local model checking, we
also devise an experiment in which each game from a series of
generalized parity games (as detailed above) is prepended with a node
owned by player $\exists$ which has one move that leads to the
original game, but also a move to an additional self-looping node with
priority \(0\).  The resulting games all have very small solutions
that can be found by the local solver, while global solving becomes
more and more expensive as the parameters of the game grow.

Modulo game.
To evaluate the alternating-time $\mu$-calculus [2]
instance of the model checking implementation in , we devise a
series of games, parameterized by a number of agents and a number $m$ of
moves per agent, but with a fixed number of positions $p_0,\dots,p_9$
marked by propositional atoms of the same name. At $p_j$, the agents
concurrently each pick a number from the set $\{1,\ldots,m\}$, causing
the game to proceed to position $p_{(h+j)\!\!\mod 10}$ where $h$ is the
sum of the numbers played.  Given a set $C$ of agents, we evaluate the
$\varphi_1=\textstyle\bigwedge_{0 \le i < 10}\mu X.\, p_i \vee \CLbox{C}X$
$\varphi_2=\nu X.\, \mu Y.\,(X \wedge (p_0 \vee \CLbox{C}Y) \wedge (p_{5} \vee \CLbox{C}Y))$
over the modulo game. Formula $\varphi_1$ says that the
coalition \(C\) has a joint strategy to reach any given state
eventually, while $\varphi_2$ expresses the Büchi property that \(C\)
can enforce that both $p_0$ and $p_5$ are visited infinitely often.

Evaluation setup.
Our main aim in the evaluation is to show that scales even on the
benchmark series we use, which are designed to be hard. In the
process, we compare the local model checking method with the reduction
to parity games (<ref>). To solve the parity games
obtained, we use PGSolver's [11, 38] implementation of
Zielonka's recursive algorithm; we expect that practical performance
can be further improved by instead using Oink [7]
as a back-end parity game solver, but leave this issue as future work.

For the standard and monotone $\mu$-calculi, the
reduction to parity games is straightforward, blurring the difference
between model checking and parity game solving. For these logics, we
thus refrain from a comparison between and other existing model
checking tools [3, 28], which would essentially
boil down to a comparison of the respective backend parity game
solvers. On the alternating-time $\mu$-calculus (AMC), we do conduct a
brief comparison with the model checker
MCMAS [30]
(further comparison between COOL-MC
and MCMAS can be found in the appendix).
We emphasize that the
meaningfulness of such a comparison is limited, as on the one hand,
MCMAS represents models symbolically while uses an
explicit-state representation, and on the other hand, MCMAS only
supports alternating-time temporal logic ATL (for which
parity-game-based model checking is overkill) while supports the
full AMC. For graded and probabilistic $\mu$-calculi, appears to
be the only existing model checker, so for these logics we evaluate
only the two variants of model checking in ; we note that the
Probabilistic Symbolic Model Checker (PRISM) [27]
uses a specification language based largely on
PCTL [17], which is incomparable to the two-valued
probabilistic $\mu$-calculus [4].

Below, we refer to the different
instantiations of by indexing a logic name with
either $l$ (for local model checking) or $g$ (for model checking by
game reduction); for instance “graded$_g$” refers to the variant of
that reduces model checking for the graded
$\mu$-calculus to parity game solving.

We measure runtimes as well as the sizes of the graph
structures and games constructed, averaging the values measured in our
experiments over at least five executions, with a timeout of 60 seconds.
All experiments have been executed on a machine with an AMD Ryzen 7 2700 CPU and
32GB of RAM. An artifact containing the source code, evaluation scripts, and
benchmarking sets for all experiments described above is available online [19].

Results and interpretation.

The runtime results on the generalized parity games experiment are
shown in <ref>. The trends
for the different logics and variants of generalized games are
For readability, we show the measurements for just three
logics in each case; additional results can be found in the appendix
and in the artifact.

minor tick num=1,
xtick distance = 10,
every axis y label/.style=
at=(ticklabel cs:0.5),rotate=90,anchor=center,
every axis x label/.style=
at=(ticklabel cs:0.5),anchor=center,
transpose legend,
legend columns=2,
legend style=at=(0.5,-0.2),anchor=north,
log ticks with fixed point,
xlabel=game size parameter,
ylabel=runtime (s),
legend entries=standard$_l$, standard$_g$,

probabilistic$_l$, probabilistic$_g$, graded$_l$, graded$_g$]

[color=blue,mark size=1.7pt,mark=x] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/laddergame-K-COOL.csv;
[color=black,mark size=1.7pt,mark=x] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/laddergame-K-PG.csv;

[color=blue,dotted,mark=triangle*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/laddergame-PML-COOL.csv;
[color=black,dotted,mark=triangle*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/laddergame-PML-PG.csv;

[color=blue,mark size=1.2pt,mark=*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/laddergame-GML-COOL.csv;
[color=black,mark size=1.2pt,mark=*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/laddergame-GML-PG.csv;

Ladder games runtimes

xtick distance = 1,
every axis y label/.style=
at=(ticklabel cs:0.5),rotate=90,anchor=center,
every axis x label/.style=
at=(ticklabel cs:0.5),anchor=center,
transpose legend,
legend columns=2,
legend style=at=(0.5,-0.2),anchor=north,
log ticks with fixed point,
xlabel=game size parameter,
ylabel=runtime (s),
legend entries=standard$_l$, standard$_g$, monotone$_l$, monotone$_g$,

graded$_l$, graded$_g$]

[color=blue,mark size=1.7pt,mark=x] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/langincl-K-COOL.csv;
[color=black,mark size=1.7pt,mark=x] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/langincl-K-PG.csv;

[color=blue,dotted,mark=triangle*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/langincl-Monotone-COOL.csv;
[color=black,dotted,mark=triangle*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/langincl-Monotone-PG.csv;

[color=blue,mark size=1.2pt,mark=*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/langincl-GML-COOL.csv;
[color=black,mark size=1.2pt,mark=*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/langincl-GML-PG.csv;

Language inclusion game runtime

It appears that the concrete choice of the logic does not
strongly effect the runtimes of the local solvers (the blue plots in
<ref>).  For game-based
solving (the black plots), we observe a considerable impact of the
choice of logic on the runtimes, in particular solving the graded
and probabilistic parity games through PGSolver takes much longer
than for the standard variants.  This is in line with expectations:
As mentioned in the end of <ref>, the game
characterization of the standard (or monotone)
modalities $\Diamond,\Box$ is straightforward, but the encoding of
graded and probabilistic modalities leads to quadratic blow-up in
the resulting games.  The local solver however, directly evaluates
modalities and thereby avoids this blow-up so that
the performance of the local solver is hardly affected by the concrete
choice of modalities.

On the other hand, game-based solving  typically is faster than local
solving. We note that the
native fixpoint computation that uses for local solving is
completely unoptimized and performs naive Kleene fixpoint iteration,
while PGSolver is an optimized tool, and in particular its recursive
algorithm shows good performance in practice.

scale only axis, axis y line*=left,

xtick distance = 1,
every axis y label/.style=
at=(ticklabel cs:0.5),rotate=90,anchor=center,
every axis x label/.style=
at=(ticklabel cs:0.5),anchor=center,
transpose legend,
legend columns=2,
legend style=at=(0.23,-0.28),anchor=north,
log ticks with fixed point,
xlabel=game size parameter,
ylabel=runtime (s),
legend entries=standard$_g$, prob$_g$, standard$_l$,

[color=black,mark size=1.7pt,mark=x] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/towersofhanoi-K-PG.csv;
[color=black,mark=triangle*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/towersofhanoi-PML-PG.csv;
[color=blue,mark size=1.7pt,mark=x] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/towersofhanoi-K-COOL.csv;

[color=blue,mark=triangle*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/towersofhanoi-PML-COOL.csv;

scale only axis, axis y line*=right, axis x line=none,

ytick distance = 0.2,

transpose legend,
legend columns=2,
legend style=at=(0.9,-0.28),anchor=north,

ylabel=exploration quotient,
legend entries=eq standard$_l$,

eq prob$_l$,

[color=red,mark size=1.7pt,mark=x]
coordinates (1,1)(2,1)(3,1)(4,1);
[color=red,dotted,mark=triangle*] coordinates (1,1)(2,0.417989417989)(3,0.227513227513)(4,0.121693121693)

Towers of Hanoi runtimes

scale only axis, axis y line*=left,

xtick distance = 1,
every axis y label/.style=
at=(ticklabel cs:0.5),rotate=90,anchor=center,
every axis x label/.style=
at=(ticklabel cs:0.5),anchor=center,
transpose legend,
legend columns=3,
legend style=at=(0.23,-0.2),anchor=north,
log ticks with fixed point,
xlabel=game size parameter,
ylabel=runtime (s),
legend entries=standard$_g$, prob$_g$, graded$_g$,

standard$_l$, prob$_l$, graded$_l$]

[color=black,mark size=1.7pt,mark=x] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/easy-hanoi-K-PG.csv;
[color=black,dotted,mark=triangle*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/easy-hanoi-PML-PG.csv;
[color=black,mark size=1.2pt,mark=*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/easy-hanoi-GML-PG.csv;

[color=blue,mark size=1.7pt,mark=x] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/easy-hanoi-K-COOL.csv;

[color=blue,dotted,mark=triangle*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/easy-hanoi-PML-COOL.csv;

[color=blue,mark size=1.2pt,mark=*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/easy-hanoi-GML-COOL.csv;

scale only axis, axis y line*=right, axis x line=none,

ytick distance = 0.2,

transpose legend,
legend columns=1,
legend style=at=(0.88,-0.2),anchor=north,

ylabel=exploration quotient,
legend entries=eq standard$_l$,

eq prob$_l$,
eq graded$_l$
[color=red,mark size=1.7pt,mark=x]
coordinates (1,0.553398058252)(2,0.248908296943)(3,0.0939044481054)(4,0.0327398047099)
[color=red,dotted,mark=triangle*] coordinates (1,1)(2,0.502183406114)(3,0.27018121911)(4,0.132682366456)
[color=red,mark size=1.2pt,mark=*] coordinates (1,0.990291262136)(2,0.445414847162)(3,0.168039538715)(4,0.0585870189546)

Lazy Towers of Hanoi runtimes

Also, the generalized
games used in the benchmarks are constructed from parity games
designed to be hard to solve; in particular, we observe that with
the notable exceptions of the language inclusion games
(<ref>) and the probabilistic variant of the
Towers of Hanoi games (<ref>), these games
typically do not have small solutions so that the local solver
cannot play out the strength of on-the-fly model checking.

Experiment series     parameter     worlds     full graph     lazy graph     game size

Language incl., monotone     $1$     $3$     $93$     $59$     $126$

$7$     $313$     $9,703$     $937$     $13,146$

$30$     $\dagger$     $\dagger$     $\dagger$     $1,099,896$

Lazy Hanoi, standard     $1$     $5$     $103$     $57$     $133$

$5$     $245$     $5,143$     $57$     $6,613$

$9$     $19,685$     $413,383$     $53$     $531,493$

$10$     $59,051$     $1,240,069$     $53$     $\dagger$

Lazy Hanoi, graded     $1$     $5$     $103$     $102$     $523$

$2$     $11$     $229$     $102$     $2,345$

$4$     $83$     $1,741$     $102$     $126,222$

$10$     $59,051$     $1,240,069$     $102$     $\dagger$

Sizes of (full and lazy) graphs and constructed parity games

This line of argumentation is substantiated by the lazy games
experiment conducted on games built from the Towers of Hanoi series,
shown in <ref> (the sizes of the constructed
graphs and games are listed in <ref>).
These results are representative
for the lazy modifications of the other parity game series as
well. Here, the local solver significantly outperforms the algorithm
that first constructs the full game.  It appears that the local solver
does indeed manage to detect the existence of small winning strategies
in these games, thereby avoiding the full exploration of the search
space.  In each case, the extent to which the local solver explores
the full game is shown in <ref> with a red plot that depicts the
exploration quotient, i.e. the percentage of the total number
of nodes that are actually explored.  This effect is observed for all
logics currently supported, including the graded and probabilistic

minor tick num=1,
xtick distance = 1,
every axis y label/.style=
at=(ticklabel cs:0.5),rotate=90,anchor=center,
every axis x label/.style=
at=(ticklabel cs:0.5),anchor=center,
transpose legend,
legend columns=2,
legend style=at=(0.5,-0.2),anchor=north,
log ticks with fixed point,
xlabel=number of moves,
ylabel=runtime (s),
legend entries=MCMAS$^2$,MCMAS$^4$, CL$^2_g$, CL$^4_g$, CL$^2_l$, CL$^4_l$]

[color=red,mark size=1.7pt,mark=x]  table [col sep=comma, x=parameter_moves, y=mean] benchmarks/modulos/results/modulosMCMAS-2.csv;
[color=red,mark size=1.7pt,mark=o]  table [col sep=comma, x=parameter_moves, y=mean] benchmarks/modulos/results/modulosMCMAS-4.csv;

[color=black,mark size=1.7pt,mark=x] table [col sep=comma, x=parameter_moves, y=mean] benchmarks/modulos/results/modulos-2-CL-PG.csv;
[color=black,mark size=1.7pt,mark=o] table [col sep=comma, x=parameter_moves, y=mean] benchmarks/modulos/results/modulos-4-CL-PG.csv;

[color=blue,mark size=1.7pt,mark=x] table [col sep=comma, x=parameter_moves, y=mean] benchmarks/modulos/results/modulos-2-CL-COOL.csv;
[color=blue,mark size=1.7pt,mark=o] table [col sep=comma, x=parameter_moves, y=mean] benchmarks/modulos/results/modulos-4-CL-COOL.csv;

Modulo game runtimes ($\varphi_1$)

minor tick num=1,
xtick distance = 1,
every axis y label/.style=
at=(ticklabel cs:0.5),rotate=90,anchor=center,
every axis x label/.style=
at=(ticklabel cs:0.5),anchor=center,
transpose legend,
legend columns=2,
legend style=at=(0.5,-0.2),anchor=north,
log ticks with fixed point,
xlabel=number of moves,
ylabel=runtime (s),
legend entries=CL$^2_g$, CL$^4_g$, CL$^2_l$,  CL$^4_l$]

[color=black,mark size=1.7pt,mark=x] table [col sep=comma, x=parameter_moves, y=mean] benchmarks/modulos/results/modulos-2-CL-PG-mu.csv;
[color=black,mark size=1.7pt,mark=o] table [col sep=comma, x=parameter_moves, y=mean] benchmarks/modulos/results/modulos-4-CL-PG-mu.csv;

[color=blue,mark size=1.7pt,mark=x]  table [col sep=comma, x=parameter_moves, y=mean] benchmarks/modulos/results/modulos-2-CL-COOL-mu.csv;
[color=blue,mark size=1.7pt,mark=o]  table [col sep=comma, x=parameter_moves, y=mean] benchmarks/modulos/results/modulos-4-CL-COOL-mu.csv;

Modulo game runtimes ($\varphi_2$)

<Ref> show the runtimes for
$\varphi_1$ and $\varphi_2$ on the modulo game with 2 and 4 agents,
respectively.  We include runtime plots for MCMAS on $\varphi_1$,
which is expressible in ATL, while $\phi_2$ is goes beyond ATL and is
thus not handled by . As expected, MCMAS is faster on the
fragment that it supports; presumably, this is due partly to the fact
that ATL allows for dedicated model checking algorithms that avoid
parity games and in fact run in polynomial time [2].

§ CONCLUSIONS AND FUTURE WORK

We have presented and evaluated the generic model checker
, which implements generic model checking algorithms for the
coalgebraic $\mu$-calculus [22], and
has been instantiated to a range of instance logics. In particular,
thus constitutes the first available model checker for the
two-valued probabilistic
$\mu$-calculus [5, 29, 4], the
graded $\mu$-calculus [25], and the full
alternating-time $\mu$-calculus [2] (model checkers for
alternating-time temporal logic
exist [1, 30, 23]).
The benchmarking results suggest the
direct evaluation of modalities in combination with lazy solving
as a setup for coalgebraic model checking that scales well in practice. An
important issue for future work is to develop and implement symbolic
model checking algorithms for the coalgebraic $\mu$-calculus.

§ DATA-AVAILABILITY STATEMENT

All data to reproduce the findings in this paper are available online.
The COOL-MC source code used to compile the artifact is available at tag  of the COOL git repository [9].
Pre-compiled Linux executables as well as a docker container to reproduce the measurements displayed in the figures and tables of this paper are available online [19].

[1]
Alur, R., de Alfaro, L., Grosu, R., Henzinger, T.A., Kang, M., Kirsch, C.M.,
Majumdar, R., Mang, F.Y.C., Wang, B.: JMOCHA: A model checking tool that
exploits design structure. In: International Conference on Software
Engineering, ICSE 2001. pp. 835–836. IEEE Computer Society (2001).

[2]
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J.  ACM  49,  672–713 (2002). 10.1145/585265.585270

[3]
Atif, M., Groote, J.F.: Understanding Behaviour of Distributed Systems Using
mCRL2. Springer (2023). 10.1007/978-3-031-23008-0

[4]
Chakraborty, S., Katoen, J.: On the satisfiability of some simple probabilistic
logics. In: Logic in Computer Science, LICS 2016. pp. 56–65. ACM (2016).

[5]
Cîrstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the
coalgebraic mu-calculus. Log. Methods Comput. Sci.  7(3) (2011).

[6]
D'Agostino, G., Visser, A.: Finality regained: A coalgebraic study of
Scott-sets and multisets. Arch. Math. Logic  41,  267–298
(2002). 10.1007/S001530100110

[7]
van Dijk, T.: Oink: An implementation and evaluation of modern parity game
solvers. In: Tools and Algorithms for the Construction and, TACAS 2018.
LNCS, vol. 10805, pp. 291–308. Springer (2018).

[8]
Enqvist, S., Hansen, H.H., Kupke, C., Marti, J., Venema, Y.: Completeness for
game logic. In: Logic in Computer Science, LICS 2019. pp. 1–13. IEEE
(2019). 10.1109/LICS.2019.8785676

[9]
fauprojects: COOL - The Coalgebraic Ontology Logic Reasoner (git repository).

[10]
Ferrante, A., Murano, A., Parente, M.: Enriched \({\mu}\)-calculi module
checking. Log. Methods Comput. Sci.  4(3) (2008).

[11]
Friedmann, O., Lange, M.: The PGSolver collection of parity game solvers.
Tech. rep., University of Munich (2009)

[12]
Friedmann, O., Lange, M.: Local strategy improvement for parity game solving.
In: Proceedings First Symposium on Games, Automata, Logic, and Formal
Verification, GANDALF 2010. EPTCS, vol. 25, pp. 118–131 (2010).

[13]
Gorín, D., Pattinson, D., Schröder, L., Widmann, F., Wißmann,
T.: COOL - A generic reasoner for coalgebraic hybrid logics (system
description). In: International Joint Conference on Automated Reasoning,
IJCAR 2014. LNCS, vol. 8562, pp. 396–402. Springer (2014).

[14]
Görlitz, O., Hausmann, D., Humml, M., Pattinson, D., Prucker, S.,
Schröder, L.: COOL 2 – a generic reasoner for modal fixpoint logics
(system description). In: Automated Deduction, CADE 2023. LNAI, vol. 14132,
p. 234–247. Springer (2023). 10.1007/978-3-031-38499-8_14

[15]
Hansen, H.H., Kupke, C.: A coalgebraic perspective on monotone modal logic. In:
Coalgebraic Methods in Computer Science, CMCS 2004. ENTCS, vol. 106, pp.
121–143. Elsevier (2004). 10.1016/j.entcs.2004.02.028

[16]
Hansen, H.H., Kupke, C., Marti, J., Venema, Y.: Parity games and automata for
game logic. In: Dynamic Logic. New Trends and Applications, DALI 2017.
LNCS, vol. 10669, pp. 115–132. Springer (2018).

[17]
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability.
Formal Aspects Comput.  6(5),  512–535 (1994).

[18]
Hasuo, I., Shimizu, S., Cîrstea, C.: Lattice-theoretic progress measures
and coalgebraic model checking. In: Principles of Programming Languages, POPL
2016. pp. 718–732. ACM (2016). 10.1145/2837614.2837673

[19]
Hausmann, D., Humml, M., Prucker, S., Schröder, L., Strahlberger, A.: Generic
model checking for modal fixpoint logics in COOL-MC (artifact). Zenodo
(2023). 10.5281/zenodo.8332511

[20]
Hausmann, D., Schröder, L.: Quasipolynomial computation of nested
fixpoints. In: Tools and Algorithms for the Construction and Analysis of
Systems, TACAS 2021. LNCS, vol. 12651, pp. 38–56. Springer (2021).

[21]
Hausmann, D., Schröder, L.: Coalgebraic satisfiability checking for
arithmetic \(\mu\)-calculi. CoRR  abs/2212.11055 (2022).

[22]
Hausmann, D., Schröder, L.: Game-based local model checking for the
coalgebraic mu-calculus. In: 30th International Conference on Concurrency
Theory, CONCUR 2019. LIPIcs, vol. 140, pp. 35:1–35:16. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik (8 2019). 10.4230/LIPIcs.CONCUR.2019.35

[23]
Kański, M., Niewiadomski, A., Kacprzak, M., Penczek, W., Nabiałek, W.:
Unbounded model checking for ATL. Studia Informatica  25(1–2)
(2021). 10.34739/si.2021.25.01

[24]
Kozen, D.: Results on the propositional $\mu$-calculus. Theor. Comput. Sci.
27,  333–354 (1983). 10.1016/0304-3975(82)90125-6

[25]
Kupferman, O., Sattler, U., Vardi, M.Y.: The complexity of the graded
\(\mathrm{\mu}\)-calculus. In: Automated Deduction, CADE-18. LNCS,
vol. 2392, pp. 423–437. Springer (2002). 10.1007/3-540-45620-1_34

[26]
Kupke, C., Marti, J., Venema, Y.: Size measures and alphabetic equivalence in
the \(\mu\)-calculus. In: Logic in Computer Science, LICS 2022. pp.
18:1–18:13. ACM (2022), <https://doi.org/10.1145/3531130.3533339>

[27]
Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of
probabilistic real-time systems. In: Computer Aided Verification, CAV 2011.
LNCS, vol. 6806, pp. 585–591. Springer (2011).

[28]
Landsaat, E.: A model checker for game logic via parity games (2022),
<https://fse.studenttheses.ub.rug.nl/28126/>, BSc thesis, University of

[29]
Liu, W., Song, L., Wang, J., Zhang, L.: A simple probabilistic extension of
modal mu-calculus. In: International Joint Conference on Artificial
Intelligence, IJCAI 2015. pp. 882–888. AAAI Press (2015),

[30]
Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for
the verification of multi-agent systems. Int. J. Softw. Tools Technol.  Transf.  19(1),  9–30 (2017). 10.1007/s10009-015-0378-x

[31]
Parikh, R.: The logic of games and its applications. Ann. Discr. Math.
24,  111–140 (1985). 10.1016/S0304-0208(08)73078-0

[32]
Pattinson, D.: Expressive logics for coalgebras via terminal sequence
induction. Notre Dame J. Formal Log.  45(1),  19–33 (2004).

[33]
Pauly, M.: Logic for Social Software. Ph.D. thesis, Universiteit van Amsterdam

[34]
Pilecki, J., Bednarczyk, M.A., Jamroga, W.: SMC: synthesis of uniform
strategies and verification of strategic ability for multi-agent systems. J.  Log. Comput.  27(7),  1871–1895 (2017).

[35]
Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theor. Comput.  Sci.  249(1),  3–80 (2000). 10.1016/S0304-3975(00)00056-6

[36]
Schröder, L.: Expressivity of coalgebraic modal logic: The limits and
beyond. Theor. Comput. Sci.  390(2-3),  230–247 (2008).

[37]
Stevens, P., Stirling, C.: Practical model-checking using games. In: Tools and
Algorithms for Construction and Analysis of Systems, TACAS '98. LNCS,
vol. 1384, pp. 85–101. Springer (1998). 10.1007/BFb0054166

[38]
tcsprojects: PGSolver (git repository).

[39]
Venema, Y.: Automata and fixed point logic: A coalgebraic perspective. Inf.  Comput.  204(4),  637–678 (2006). 10.1016/j.ic.2005.06.003

§ APPENDIX

<Ref> below show the runtimes
for additional experiments on clique games and Jurdzinski games; the results
in these experiments show the same trends as the results shown and commented on in the main paper.

xtick distance = 1,
every axis y label/.style=
at=(ticklabel cs:0.5),rotate=90,anchor=center,
every axis x label/.style=
at=(ticklabel cs:0.5),anchor=center,
transpose legend,
legend columns=2,
legend style=at=(0.5,-0.2),anchor=north,
log ticks with fixed point,
xlabel=game size parameter,
ylabel=runtime (s),
legend entries=standard$_l$, standard$_g$, monotone$_l$, monotone$_g$,

graded$_l$, graded$_g$, PML$_l$, PML$_g$]

[color=blue,mark size=1.7pt,mark=x] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/cliquegame-K-COOL.csv;
[color=black, mark size=1.7pt,mark=x] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/cliquegame-K-PG.csv;

[color=blue,dotted,mark=triangle*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/cliquegame-Monotone-COOL.csv;
[color=black,dotted,mark=triangle*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/cliquegame-Monotone-PG.csv;

[color=blue,mark size=1.2pt,mark=*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/cliquegame-GML-COOL.csv;
[color=black,mark size=1.2pt,mark=*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/cliquegame-GML-PG.csv;

Clique games runtime

xtick distance = 1,
every axis y label/.style=
at=(ticklabel cs:0.5),rotate=90,anchor=center,
every axis x label/.style=
at=(ticklabel cs:0.5),anchor=center,
transpose legend,
legend columns=2,
legend style=at=(0.5,-0.2),anchor=north,
log ticks with fixed point,
xlabel=game size parameter,
ylabel=runtime (s),
legend entries=standard$_l$, standard$_g$,

probabilistic$_l$, probabilistic$_g$, graded$_l$, graded$_g$]

[color=blue,mark size=1.7pt,mark=x] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/jurdzinskigame-K-COOL.csv;
[color=black,mark size=1.7pt,mark=x] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/jurdzinskigame-K-PG.csv;

[color=blue,dotted,mark=triangle*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/jurdzinskigame-PML-COOL.csv;
[color=black,dotted,mark=triangle*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/jurdzinskigame-PML-PG.csv;

[color=blue,mark size=1.2pt,mark=*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/jurdzinskigame-GML-COOL.csv;
[color=black,mark size=1.2pt,mark=*] table [col sep=comma, x=size, y=mean] benchmarks/parity-mod/results/jurdzinskigame-GML-PG.csv;

Jurdzinski games runtime

We also present an additional benchmark comparing the performance of COOL-MC to the MCMAS model checker.
The castle game has been used for benchmarking in previous work
on ATL model
checking [34, 23].
The game is parametrized over the number of castles and the health
points all castles start with.  Each castle has a corresponding knight
that can, in each turn, either be sent out to attack another castle or
stay and defend the castle.  In each turn, all knights decide
concurrently which other castle they want to attack or if they want to
stay at their castle and defend.  A knight who has attacked in one
turn needs to stay and rest in the next turn.  A castle that has its
knight defending it or resting can block one attack.  Each unblocked
attack on a castle reduces that castle's number of health points by
one. When no health points are left, the castle has lost the game and
can no longer attack; this situation is indicated by propositional
atoms $\mathsf{lost}_{a}$, where $a$ is a knight.

For the castle game we check the following AMC formulas
(which are expressible in ATL as used for the MCMAS benchmarks) for satisfaction in the initial state. The formula

\[\nu X.\, \neg\mathsf{lost}_\agent \wedge \CLbox{\{\agent\}}X\]

expresses that the knight \(\agent\) has a strategy ensuring that her castle never gets destroyed.
We check this formula for each \(\agent \in \Agents\). Moreover, the formula

\[\textstyle\mu X.\, ((\bigwedge_{\agent \in C}\neg\mathsf{lost}_\agent) \wedge (\bigwedge_{\agent \in \Agents\setminus C}\mathsf{lost}_\agent)) \vee \CLbox{C}X\]

expresses that the coalition \(C\) has a joint strategy to ensure that
all other castles are eventually destroyed while none of the allied
castles (belonging to $C$) are destroyed.  We check this formula for
one coalition of each size.

The castle game has the property that almost none of the joint moves
are equivalent, i.e. almost all joint moves lead to a different
outcome.  Additionally, the castle game can be specified in MCMAS
using separated local states of the agents.  We chose a
straightforward encoding where each agent has a boolean variable
|ready| capturing whether the agent is ready to attack and
an integer variable |hp| holds the current number of health
points of the agent.  The atoms \(\mathsf{lost}_\agent\) are evaluated
to true exactly when the |hp| variable of \(\agent\) is
\(0\).  The main difficulty of this encoding lies in the specification
of the |Evolution|, which encodes the transition function of
agents, as shown in <ref>: The rules of the game
require counting the number of attackers, but MCMAS provides no direct
way to count; hence one case has to be generated for each possible
number of attackers.  Additionally, all the cases have to be disjoint
as MCMAS will pick otherwise some matching case non-deterministically.
So each of these cases has to list all possible combinations of
attackers and non-attackers in a disjunction.

Agent ag1
Lobsvars =   ;
Vars: ready : boolean; hp : 0 .. 2; end Vars
Actions =  defend, rest, dead, attack_2 ;
((hp) >= (1) and ready = true) :  defend, attack_2 ;
((hp) >= (1) and ready = false) :  rest ;
Other :  dead ;  end Protocol
hp = (hp) - (1) and ready = false if (Action = attack_2 and
((ag2.Action = attack_1 and (hp) >= (1)) or (hp = 1 and
ag2.Action = attack_1)));
hp = (hp) - (0) and ready = true if (!(Action = attack_2) and
((ag2.Action = attack_1 and (hp) >= (0)) or (hp = 0 and
ag2.Action = attack_1)));
ready = false if ((hp) >= (1) and (!(ag2.Action = attack_1) and
Action = attack_2));
ready = true if ((hp) >= (1) and (!(ag2.Action = attack_1) and
!(Action = attack_2))); end Evolution
end Agent

MCMAS encoding of an agent in the two-castle two-health-point game

The encoding of the castle game with \(n\) castles and \(h\) health points
in COOL uses \((2 \times H)^n\) as state space where \(2 = \{t, f\}\) and \(H = \{x \mid 0 \le x \le h\}\).
In <ref> we see that COOL-MC again can not match the performance of MCMAS due to the same reasons as mentioned in the paper already.

minor tick num=1,
xtick distance = 1,
every axis y label/.style=
at=(ticklabel cs:0.5),rotate=90,anchor=center,
every axis x label/.style=
at=(ticklabel cs:0.5),anchor=center,
transpose legend,
legend columns=2,
legend style=at=(0.5,-0.2),anchor=north,
log ticks with fixed point,
xlabel=number of HP,
ylabel=runtime (s),
legend entries=MCMAS$^2$,MCMAS$^3$, MCMAS$^4$, CL$^2_g$, CL$^3_g$, CL$^4_g$, CL$^2_l$, CL$^3_l$, CL$^4_l$]

[color=red,mark size=1.7pt,mark=x]  table [col sep=comma, x=parameter_hp, y=mean] benchmarks/castles/results/castles-2-MCMAS.csv;
[color=red,mark size=1.7pt,mark=*]  table [col sep=comma, x=parameter_hp, y=mean] benchmarks/castles/results/castles-3-MCMAS.csv;
[color=red,mark size=1.7pt,mark=o]  table [col sep=comma, x=parameter_hp, y=mean] benchmarks/castles/results/castles-4-MCMAS.csv;

[color=black,mark size=1.7pt,mark=x] table [col sep=comma, x=parameter_hp, y=mean] benchmarks/castles/results/castles-2-CL-PG.csv;
[color=black,mark size=1.7pt,mark=*] table [col sep=comma, x=parameter_hp, y=mean] benchmarks/castles/results/castles-3-CL-PG.csv;
[color=black,mark size=1.7pt,mark=o] table [col sep=comma, x=parameter_hp, y=mean] benchmarks/castles/results/castles-4-CL-PG.csv;

[color=blue,mark size=1.7pt,mark=x] table [col sep=comma, x=parameter_hp, y=mean] benchmarks/castles/results/castles-2-CL-COOL.csv;
[color=blue,mark size=1.7pt,mark=*] table [col sep=comma, x=parameter_hp, y=mean] benchmarks/castles/results/castles-3-CL-COOL.csv;
[color=blue,mark size=1.7pt,mark=o] table [col sep=comma, x=parameter_hp, y=mean] benchmarks/castles/results/castles-4-CL-COOL.csv;

Castles game runtimes on the ATL formula series


Time-Limited Waveforms with Minimum Time Broadening for the Nonlinear Schrödinger Channel

Youssef Jaffal,  Alex Alvarado, Senior Member, IEEE

This work has  received  funding  from  the  European  Research  Council (ERC) under the European Union’s Horizon 2020 research and innovation programme under Grant 757791. (Corresponding author: Youssef Jaffal.)

The authors are with the Department of Electrical
Engineering, Eindhoven University of Technology, 5600 MB Eindhoven,
The Netherlands (e-mail<EMAIL_ADDRESS>a.alvarado@tue.nl).

Simple fiber optic communication systems can be implemented using energy modulation of isolated time-limited pulses. Fundamental solitons are one possible solution for such pulses which offer a fundamental advantage: their shape is not affected by fiber disperison and nonlinearity. Furthermore, a simple energy detector can be used at the receiver to detect the transmitted information. However, systems based on energy modulation of solitons are not competitive in terms of data rates. This is partly due to
the fact that the effective time duration of a soliton depends on its chosen amplitude. In this paper, we propose to replace fundamental solitons by new time-limited waveforms that can be detected using an energy detector, and that are immune to fiber distortions. Our proposed solution relies on the prolate spheroidal wave functions and a numerical optimization routine. Time-limited waveforms that undergo minimum time broadening along an optical fiber are obtained and shown to outperform fundamental solitons. In the case of binary transmission and a single span of fiber, we report rate increases of $33.8$% and $12$% over lossy and lossless fibers, respectively. Furthermore, we show that the transmission rate of the proposed system increases as the number of used energy levels increases, which is not the case for fundamental solitons due to their effective time-amplitude constraint. For example,  rate increases of $164$%  and $70$% over lossy and lossless fibers respectively are reported when using four energy levels.

Nonlinear Schr$\ddot{\text{o}}$dinger equation, energy modulation, optical fibers,  time broadening, solitons.

§ INTRODUCTION

The propagation of signals through a single-mode optical fiber is governed by the nonlinear Schr$\ddot{\text{o}}$dinger (NLS) equation <cit.>. Communication systems for the NLS channel can be divided into two main categories. The first one uses linear modulation techniques combined with either linear or nonlinear (e.g., digital backpropagation) receivers. Such communication systems (with linear receivers) are currently implemented in most commercial systems. The second category includes systems with nonlinear transmitters and receivers, e.g., those based on the nonlinear Fourier transform (NFT). Such systems are tailored to the NLS equation [2] and are currently still at a research stage. The simplest NFT-based transceiver uses energy modulation (EM) of isolated fundamental solitons, where the inverse NFT is not required at the receiver and a simple energy detector can be used. Such systems date in fact back to 1973, where the idea of using solitons for transmission was first proposed by Hasegawa [3].

The transmission rates of EM of isolated fundamental solitons are lower than the ones achieved by other sophisticated techniques (such as current coherent systems or modulation techniques that need the NFT or its inverse). Systems based on EM of isolated solitons suffer from several weaknesses.
First, EM systems have limited transmission rates as they limit the number of useful signals. For example, the energy detector cannot differentiate between two different signals that have the same energy but different phases.

Second, fundamental solitons are not time-limited, and hence consecutive fundamental solitons are not perfectly isolated. Generating a time-limited signal from a fundamental soliton can be done by simple truncation or by more sophisticated methods such as the soliton shortening methods recently introduced in [4]. Increasing the time window of the truncated or shortened soliton reduces the distortion and provides better isolation between the consecutive pulses along the NLS channel. Such time increase  decreases the bit error rate, but it also decreases the transmission rates. Third, fundamental solitons have a high time-bandwidth product [5], which results in a low spectral efficiency.
Fourth,  low energy solitons need relatively high time duration since the energy and the effective duration of solitons are inversely proportional. Consequently, conventional pulse amplitude modulation (PAM) systems with more than two amplitude levels have lower performance compared to an on-off keying (OOK) system as reported in <cit.>.

Fundamental solitons are not the only candidate pulses to be used in EM of isolated pulses; as the transmitted information is embedded in the energy of the transmitted pulses, preserving the shape of the transmitted pulses along the NLS channel is in fact not required. The desirable property of the used pulses is to have low time  broadening: large time broadening would require a large guard time to guarantee that consecutive pulses remain isolated along the channel, which would decrease the transmission rates of the system. Compared to a fundamental soliton (that preserves its effective duration), a shorter pulse with the same energy is more desirable if the effective duration of the broadened received pulse remains lower than the effective duration of the received soliton.

Energy modulation of isolated pulses, where consecutive pulses carry the information bits in their energies. $T$ should be greater or equal to the duration of each transmitted pulse ($T_{p_m}$), and greater or equal to the duration that contains $100(1-\epsilon)\%$ of the energy of each received pulse  ($T_{\tilde{p}_m}$).

In this paper we propose replacing fundamental solitons by time-limited waveforms that undergo  minimum time broadening (MTB) in EM of isolated pulses.

We make use of the set of prolate spheroidal wave functions (PSWFs) to search for the MTB waveforms. The PSWFs form a complete orthonormal set for time-limited functions and they were used in [7], [8], and [9] to design optimal time-limited pulses. We consider both lossless and lossy fibers
and we show that the obtained MTB waveforms have lower time duration and lower time-bandwidth product compared to fundamental solitons. Consequently, MTB waveforms outperform the truncated solitons in conventional EM of isolated pulses. More importantly, we show that MTB waveforms have the ability to increase the transmission rates and the spectral efficiency when additional low energy pulses are used, which as previously mentioned, is not the case for solitons. The main contribution of this paper is introducing MTB waveforms that improve the performance of EM of isolated pulses in fiber optic channels.

The paper is organized as follows: in Sec. <ref> we present the considered system model. In Sec. <ref> we present the numerical results  of using fundamental solitons in EM of isolated pulses. In Sec. <ref> we propose the use of MTB waveforms and show their advantage over fundamental solitons. We  conclude the paper in Sec. <ref>.

§ SYSTEM MODEL: ENERGY MODULATION OF ISOLATED PULSES

We consider the EM system illustrated in Fig. <ref>. The transmitted messages $\{m_k\}_{k\in\mathbb{Z}}$ are chosen from the set $\mathcal{M}=\{1,2, \dots, M\}$ where we restrict $M$ to be a power of two. For each message $m\in \mathcal{M}$, the energy modulator generates a corresponding pulse $p_m(t)$ that has an energy

\begin{equation}
E_{m} = \left(\frac{m-1 }{M-1}\right)^2E_{M},
\label{Eq:EnergiesEM}
\end{equation}

where $E_{M}$ is the highest used energy level. Note that if the chosen pulses $p_m(t)$ are scaled versions of the same pulse, i.e.,  $p_m(t)=\frac{m-1}{M-1}p_{M}(t)$ $\forall m\in\mathcal{M}$, then the considered EM system is equivalent to conventional PAM with equispaced amplitudes, where the transmitted information bits are embedded in the amplitude of the same pulse.

We consider the use of strictly time-limited pulses. We define the duration $T_{p_m}$ of $p_m(t)$ by the minimum time window that satisfies

\begin{equation}
p_m(t)=0 \text{ if } t \notin \left[-\frac{T_{p_m}}{2}, \frac{T_{p_m}}{2} \right].
\label{eq:pulsePtl}
\end{equation}

Note that $T_{p_1}=0$ since $p_1(t)$ is the zero-energy signal (see (<ref>)).
The energy modulator transmits the signal

\begin{equation}
\label{eq:TxSignal}
\end{equation}

where $T$ is the modulation interval.
To guarantee strict isolation between the consecutive transmitted pulses, we restrict $T$ to be greater or equal to the duration of the pulses, i.e.,

\begin{equation}
T\geq T_{p_m}   \text{ for } m\in\{2,3,\dots, M\}.
\label{eq:TxIsolation}
\end{equation}

Because of the time limitation in (<ref>), $\left\{p_{m}(t)\right\}_{m=2}^{M}$ cannot be strictly band-limited.  We define their effective bandwidth by the values of $W_{p_m}$ that satisfy

\begin{equation}
\int_{-W_{p_m}}^{W_{p_m}} \left|P_m(f)\right|^2df = (1-\epsilon)E_m  \text{ for } m\in\{2,3,\dots, M\},
\label{eq:Banddef}
\end{equation}

where $P_m(f)=\int_{-\infty}^{\infty}p_m(t)e^{-j2\pi ft}dt$ is the Fourier transform of $p_m(t)$, and $\epsilon E_m$ is the corresponding out-of-band energy where $0<\epsilon<1$. Note that $W_{p_1}=0$ since $p_1(t)$ is the zero signal. We consider a maximum allowable bandwidth $W_{max}$ where the bandwidths of the transmitted pulses should satisfy

\begin{equation}
W_{p_m}\leq W_{max} \text{ for } m\in\{2,3,\dots, M\}.
\label{eq:BandConstr}
\end{equation}

The considered channel is a single-mode optical fiber of length $L$, where the evolution of the propagated signal $q(t,z)$ is governed by the NLS equation <cit.>

\begin{equation}
\frac{\partial q(t,z)}{\partial z} = -\frac{\alpha}{2}q(t,z) -\frac{i\beta_2}{2}\frac{\partial^2 q(t,z)}{\partial^2 t} + i\gamma|q(t,z)|^2q(t,z),
\label{NLSEq}
\end{equation}

where $t$ represents retarded time, $z$ is the propagation distance, $\alpha$ represents the fiber losses, $\beta_2$ is the group-velocity dispersion parameter, and $\gamma$ is the nonlinear parameter.
The NLS equation is used to describe two main models for fiber optical channels. The first model is when using ideal distributed amplification where we assume that the fiber losses are ideally compensated, hence $\alpha=0$. We refer to this model as “lossless fiber”.
The second one is the “lossy fiber” model where an erbium-doped fiber amplifier (EDFA) is used at the end of the optical fiber, so $\alpha$ is non zero along the fiber.
Both amplification schemes add noise to the system, but in this work we ignore the noise and we focus on the deterministic pulse propagation in  optical fibers.

The receiver can obtain the squared magnitude of the propagated signal $|q(t,L)|^2$ using a photodiode detector for example.

\begin{equation}
\left\{\Tilde{p}_{m}(t)\right\}_{m\in \mathcal{M}}
\label{eq:RxPulses}
\end{equation}

to be the magnitude of the propagated $\left\{p_{m}(t)\right\}_{m\in \mathcal{M}}$, i.e.,   $\forall m\in\mathcal{M}$

\begin{equation*}
\Tilde{p}_{m}(t) = |q(t,L)|    \text{ if }q(t,0) = p_{m}(t).
\label{}
\end{equation*}

We assume that the energy of a received pulse is equal to the energy of the corresponding transmitted one, which can be achieved by using amplifiers. Hence, $E_m$ is the energy of $\Tilde{p}_m(t)$ $\forall m\in \mathcal{M}$. The time support of the propagated pulses may change along the NLS channel, and we refer to this effect as “time broadening”. Note that $\Tilde{p}_1(t)$ is the zero signal and has zero duration and zero bandwidth.
We define the effective duration of $\Tilde{p}_m(t)$ with $m\in\{2,3, \dots, M\}$ by the time window  $T_{\Tilde{p}_m}$ that satisfies

\begin{equation}
\int_{-T_{\Tilde{p}_m}/2}^{T_{\Tilde{p}_m}/2} \left|\Tilde{p}_m(t)\right|^2dt = (1-\epsilon)E_m.
\label{eq:Teff}
\end{equation}

To control the interaction between consecutive received pulses, we impose the following constraint on the modulation interval:

\begin{equation}
T\geq T_{\tilde{p}_m}  \text{ for } m\in\{2,3,\dots, M\}.
\label{eq:RxIsolation}
\end{equation}

Decreasing $\epsilon$ improves the isolation between propagated consecutive pulses, hence, consecutive pulses are said to be isolated at level $1-\epsilon$ at the receiver. Note that the isolation should be also maintained along the channel and not only at the receiver. If the effective duration of the propagated pulses along the channel does not exceed the effective duration at the receiver, then the constraint in (<ref>) is sufficient. Otherwise, as in the case of multi-solitons [5], the constraint in (<ref>) should be extended to take into account the effective duration along the channel.

By choosing a sufficiently small value for $\epsilon$ in (<ref>), the interaction between the possibly broadened consecutive pulses can be kept negligible when transmitting the signal in (<ref>) through (<ref>). Then, the received signal $|q(t,L)|$ is well approximated by

\begin{equation}\label{aaaaa}
|q(t,L)|\approx\sum_{k\in\mathbb{Z}} \Tilde{p}_{m_k}(t-kT).
\end{equation}

In this case, the energy detector can generate the estimate $\{\Tilde{m}_k\}$ of $\{m_k\}$ by computing the energy over the time window $[kT-T/2, \, kT+T/2]$.

The transmission rate of this system is

\begin{equation}
\label{eq:rates}
\end{equation}

We consider the use of the modulation interval

\begin{equation}
T = \max\left\{T_{p_2}, T_{\Tilde{p}_2},T_{p_3}, T_{\Tilde{p}_3},\dots, T_{p_{M}}, T_{\Tilde{p}_{M}}\right\}.
\label{eq:Tmax}
\end{equation}

To satisfy the constraints in (<ref>) and (<ref>), the modulation interval should be greater or equal to the right hand side of (<ref>). Hence, the considered modulation interval in (<ref>) is the one that maximizes (<ref>) while satisfying  (<ref>) and (<ref>).
We use the bandwidth definition in (<ref>) for the pulses $p_m(t)$ and $\Tilde{p}_m(t)$, and we define the spectral efficiency by

\begin{equation}
\text{SE} \triangleq \frac{R}{W}=\frac{\log_2M}{WT} \text{~bit/s/Hz},
\label{eq:SE}
\end{equation}

\begin{equation}
W=\max\left\{W_{p_2}, W_{\Tilde{p}_2},W_{p_3}, W_{\Tilde{p}_3},\dots, W_{p_{M}}, W_{\Tilde{p}_{M}}\right\}.
\label{eq:WeqMax}
\end{equation}

If the effective bandwidths along the channel do not exceed the ones at the transmitter and the receiver, then (<ref>) and (<ref>) are valid definitions. Otherwise, the effective bandwidth along the channel should be also considered as done in [5] for multi-solitons.
We define the time-bandwidth product by

\begin{equation}
c\triangleq WT,
\label{eq:TimBandProd}
\end{equation}

which is inversely proportional to the spectral efficiency: the lower the $c$, the higher the spectral efficiency.

In the following section we consider the truncated solitons as a baseline for our system model, and in Sec. <ref> we propose the MTB waveforms and present their numerical results. In what follows we use the following simulation parameters: $L=80$ Km, $\epsilon=10^{-4}$, $W_{max}=50$ GHz, $\beta_2=-21.7$ $\text{ps}^2$/Km, $\gamma=1.2$ $\text{W}^{-1}\text{Km}^{-1}$, $\alpha=0$ dB/Km for the lossless fiber, and $\alpha=0.2$ dB/Km for the lossy fiber.

§ ENERGY MODULATION OF TRUNCATED SOLITONS

In this section, we first present the definition and some properties of fundamental solitons, then we present their use in our system model.
In this paper, we use the following equation for fundamental solitons <cit.>:

\begin{equation}
s(t)=A \, \text{sech}\left(A\sqrt{\frac{\gamma}{|\beta_2|}} t \right),
\label{eq:soliton}
\end{equation}

which is a solution for (<ref>) when $\alpha=0$, i.e., if $q(t,0)=s(t)$ is used in (<ref>), then $\tilde{s}(t)=|q(t,z)|=s(t)$ $\forall z\in \mathbb{R}$.
The energy of $s(t)$ is

\begin{equation}
E_{s}= 2A\sqrt{\frac{|\beta_2|}{\gamma}},
\label{ESoliton}
\end{equation}

and its effective duration is given by

\begin{equation}
T_{s} = \frac{\sqrt{|\beta_2|}}{A\sqrt{\gamma}}\ln{\frac{2-\epsilon}{\epsilon}},
\label{TeffSoliton}
\end{equation}

which is obtained by solving (<ref>) for $\tilde{p}_m(t)=s(t)$ (similarly to (9) in [6] which was derived in the case of normalized NLS equation).

The Fourier transform of $s(t)$ is <cit.>

\begin{equation*}
S(f)= \pi\sqrt{\frac{|\beta_2|}{\gamma}} \, \text{sech}\left(\frac{\pi^2}{A}\sqrt{\frac{|\beta_2|}{\gamma}} f \right).
\end{equation*}

Its effective bandwidth is obtained by solving (<ref>) for $P_m(f)=S(f)$ and it is given by

\begin{equation}
W_{s}= \frac{A\sqrt{\gamma}}{\pi^2\sqrt{|\beta_2|}}\ln{\frac{2-\epsilon}{\epsilon}}.
\label{WeffSoliton}
\end{equation}

By (<ref>) and (<ref>), the time-bandwidth product of fundamental solitons is given by

\begin{equation}
c_{s}= T_s W_s = \frac{1}{\pi^2}\ln^2{\frac{2-\epsilon}{\epsilon}}.
\label{cSoliton}
\end{equation}

By (<ref>) and (<ref>),  the energy of the soliton is directly proportional to its effective bandwidth. Hence using a maximum constraint on the used bandwidth $W_{max}=50$ GHz yields a maximum possible energy for fundamental solitons of approximately $1.8$ pJ (for the considered values of $\epsilon$, $\beta_2$, and $\gamma$).

We consider truncated solitons as a baseline of our system, where a soliton is truncated to its effective duration $T_{s}$ (see (<ref>)). Given an energy level $E$, we generate the soliton over its effective duration using (<ref>), (<ref>), and (<ref>). We obtain the received truncated soliton using the split-step Fourier method (SSFM) <cit.>, and we estimate numerically its effective duration $T_{\tilde{s}}$. In Fig. <ref> we show the transmitted duration (solid) and the estimated received duration (dashed) for both lossless and lossy fibers as a function of the energy $E$. Note that $T_s$ and $E$ are inversely proportional (by (<ref>) and (<ref>)), where the minimum $T_s$ is obtained at the maximum energy $E=1.8$ pJ, and where $T_{s}\to \infty$ as $E\to 0$. For energies that are lower than $0.9$ pJ, $T_{\tilde{s}}$ is almost the same for lossy and lossless fibers (no broadening). $T_{\tilde{s}}$ is slightly lower than $T_{s}$, then $\max\{T_s, T_{\tilde{s}}\}=T_{s}$. For energies higher than $0.9$ pJ, $T_{\tilde{s}}$ is larger than $T_{s}$, and hence $\max\{T_s, T_{\tilde{s}}\}=T_{\tilde{s}}$ for both lossy and lossless fibers.  We verified that the effective duration of the truncated solitons along the fibers does not exceed their effective duration at the receiver, hence the constraint in (<ref>) is sufficient to guarantee isolation along both the channel and the receiver.

Duration of transmitted ($T_s$) and received ($T_{\tilde{s}}$) truncated solitons for $L=80$ Km and $\epsilon=10^{-4}$.

The transmission rate $R$ in (<ref>) of EM of truncated solitons can be computed based on the results of Fig. <ref>. The transmission rate of an OOK system is maximized when the pulse with minimum $T=\max\{T_s, T_{\tilde{s}}\}$ is used. As shown in Fig. <ref>, the minimum $T$ for OOK is $338$ ps for lossy fibers (at $E=1.2$ pJ), and $239$ ps for lossless fibers (at $E=1.8$ pJ). We compute the corresponding transmission rates and we include them in the first column of Table <ref>. Note that using the truncated soliton with $E=1.8$ pJ over lossy fiber decreases the transmission rate by $12.5$% compared to using the one with $E=1.2$ pJ, since $T_{\tilde{s}}=386$ ps at $E=1.8$ pJ.

Consider now the case with $M=4$ energies. The energy levels that satisfy (<ref>) and yield the minimum possible $T$ (defined in (<ref>)) are $\{0, 0.2, 0.8, 1.8\}$ pJ for both lossy and lossless fibers (as shown in Fig. <ref>).
In Fig. <ref> we show the truncated solitons for the different energy levels, where the duration of a soliton increases as the energy decreases. The modulation interval in this case is $T=1789$ ps which is the same for lossy and lossless fibers. The corresponding transmission rates are computed and included in the first column of Table <ref>. Note that the transmission rates for $4$-EM is lower than the ones achieved by OOK (similarly to the results in <cit.>). In the following theorem we derive an upper bound for the transmission rate, which decays to zero as $M\to\infty$.

Given a maximum allowable bandwidth $W_{max}$, the transmission rate of $M$-EM of isolated solitons is upper-bounded by

\begin{equation*}
R \leq \frac{\pi^2W_{max}\log_2 M}{(M-1)^2 \ln^2{\frac{2-\epsilon}{\epsilon}}} \text{ bit/s.}
\end{equation*}

In the considered system model, $T_{p_2}$ and $T_{p_M}$ are the effective duration of the solitons with energies $E_2$ and $E_M$, respectively. $E_2=\frac{E_{M}}{(M-1)^2}$ by (<ref>), and since the effective duration and the energy of solitons are inversely proportional (by (<ref>) and (<ref>)), $T_{p_2}=(M-1)^2T_{p_M}$. By (<ref>),

\begin{equation}
T_{p_2}=(M-1)^2T_{p_M}\geq \frac{(M-1)^2 \ln^2{\frac{2-\epsilon}{\epsilon}}}{\pi^2W_{max}}.
\label{eq:ThProofTp2}
\end{equation}

By (<ref>),

\begin{equation*}T\geq T_{p_2}\geq \frac{(M-1)^2 \ln^2{\frac{2-\epsilon}{\epsilon}}}{\pi^2W_{max}}.
\end{equation*}

Finally, using (<ref>) and the obtained lower bound on $T$ concludes the proof.

Used pulses in $4$-EM of truncated solitons ($E_1=0$ pJ not shown).

Based on (<ref>) and Fig. <ref>, $T=T_{p_2}$ for $M\geq4$ since $E_2$ falls in the region with no broadening. Using $E_M=1.8$ pJ (i.e. $p_M(t)$ is the truncated soliton with bandwidth $W_{max}$) maximizes the transmission rate for $M\geq4$ where the resulting $T=T_{p_2}$ is equal to the right hand side of (<ref>). Hence, the transmission rates achieve the upper bound of Theorem <ref> with equality $R=5\frac{\log_2M}{(M-1)^2}$ Gbit/s for $M \geq 4$ (for the considered simulation parameters). The main weakness of solitons shows up here: OOK outperforms $M$-EM systems with $M\geq4$ and the rates decrease if $M$ increases.  It is possible to look for the optimal energy levels (instead of the ones in (<ref>)) to improve the rates as done in  [6], where the optimal achievable rate depends on the noise model. In this paper we do not search for the optimal energy levels since we consider noiseless fibers and because our main goal is to introduce the MTB waveforms.

Transmission rates (Gbit/s) for fiber length $L=80$Km and at an isolation level $(1-10^{-4})$. We show the percentage increase with respect to OOK of truncated solitons.

Truncated solitons      MTB pulses

OOK, lossless fibers     $4.18$       $4.68$ ($12\%$ increase)

OOK, lossy fibers      $2.96$      $3.96$ ($33.8\%$ increase)

$4$-EM, lossless fibers    $1.12$     $7.12$ ($70\%$ increase)

$4$-EM, lossy  fibers    $1.12$       $7.09$ (164$\%$ increase)

$M$-EM, $M \geq 4$
Lossless & lossy fibers      $ 5\frac{\log_2M}{(M-1)^2}$     $\approx 3.5\log_2M$

For sample values of the energy level $E$, we compute  the time-bandwidth product of truncated solitons (based on   (<ref>), (<ref>), and (<ref>)) as

\begin{equation*}
c=\max\{T_s, T_{\tilde{s}}\}\cdot \max\{W_s, W_{\tilde{s}}\}.
\end{equation*}

The obtained numerical results are shown in Fig. <ref>.
Note that for $E\leq 0.9$ pJ, the time-bandwidth product for truncated solitons is almost equal to the one of nontruncated solitons ($c_s=9.94$ computed using (<ref>)), since the truncated solitons do not broaden for this range of $E$ (as shown in Fig. <ref>).
Using the results of Fig. <ref>, we compute the SE in (<ref>) for OOK (shown in Fig. <ref>).  The obtained SEs are shown in Table <ref>. Note that the spectral efficiency increases as $\epsilon$ increases, where $0.33$ bit/s/Hz was reported in [2] for OOK of solitons when using $\epsilon=10^{-2}$. The used $\epsilon=10^{-4}$ here is considered “practically reasonable” in [5], where the approximated time-bandwidth product of fundamental solitons in [5] is similar to the one obtained here by (<ref>) and yields a similar spectral efficiency around $0.1$ bit/s/Hz for OOK of solitons.

For $M$-EM of isolated pulses, the time-bandwidth product depends on $T$  and $W$ that are defined in (<ref>) and (<ref>). For the $4$-EM of solitons shown in Fig. <ref>, $W=50$ GHz which occurs at $E=1.8$ pJ, and  $T=1789$ ps which is the duration of the soliton at $0.2$ pJ, then the resulting time-bandwidth product is $\approx89.5$ and the corresponding spectral efficiency is $\log_2(4)/89.5\approx 0.022$ bit/s/Hz. The spectral efficiency for $M\geq4$ can be obtained form Table <ref> by dividing the transmission rate by $50$ GHz (the bandwidth at $1.8$ pJ). Similarly to the transmission rates of truncated solitons, the spectral efficiency decreases when $M$ increases.

Time-bandwidth product of MTB pulses and solitons for $L=80$ Km and $\epsilon=10^{-4}$.

Spectral efficiency (bit/s/Hz) for fiber length $L=80$ Km and at an isolation level $(1-10^{-4})$.

Truncated solitons      MTB pulses

OOK, lossless fibers     $0.084$       $0.094$

OOK, lossy fibers      $0.089$      $0.111$

Lossless & lossy fibers    $0.022$       $0.14$

$M$-EM, $M \geq 4$
Lossless & lossy fibers      $ 0.1\frac{\log_2M}{(M-1)^2}$     $\approx 0.07\log_2M$

§ ENERGY MODULATION OF WAVEFORMS WITH MINIMUM TIME BROADENING

We consider maximizing the transmission rate in (<ref>) by finding the optimal pulses $\left\{p_m(t)\right\}_{m\in\mathcal{M}}$ that allows to use the minimum possible $T$ (defined in (<ref>)). Minimizing the right hand side of (<ref>) can be done by independently finding the optimal pulses that minimize the maximum of each pair $\{T_{p_m}, T_{\Tilde{p}_m}\}_{m=2}^{M}$.

We consider the general problem of finding the optimal pulse $p(t)$ that has an energy $E$ and achieves the minimum possible value of $\max\{T_p, T_{\Tilde{p}}\}$. To solve this problem, we first consider the problem of finding the pulse $p(t)$ that achieves the minimum $T_{\Tilde{p}}$ for a given value of $T_p$:

\begin{equation}
\begin{aligned}
p^*(t) &=  \,\,\,\, \underset{p(t)}{\text{argmin}} && T_{\Tilde{p}}\\
& \text{subject to} && p(t)=0 \text{ for } t\notin [-T_p/2, \, T_p/2] \\
& && \int_{-T_{p}/2}^{T_{p}/2} |p(t)|^2dt = E\\
& && \int_{-W_{max}}^{W_{max}} \left|P(f)\right|^2df \geq (1-\epsilon)E%\\
%& && W_{q,L}  \leq W_{max}
\end{aligned},
\label{eq:OptProb}
\end{equation}

where the third constraint is used to satisfy (<ref>).
To find the optimal solution of (<ref>), we use a numerical method that is similar to the one proposed in [9]; we write $p(t)$ as a linear combination of normalized truncated PSWFs (see (9) in [9] and the appendix therein) and we find the optimal  combinations of normalized truncated PSWFs that minimize the objective function in (<ref>). We use the software in [11] to generate the PSWFs, and we use the MATLAB function `fmincon' to find the optimal solution of (<ref>).

For chosen sample values of $T_{p}$, we search for the corresponding optimal pulses $p^*(t)$ that yield $T_{\Tilde{p}^*}$ at the receiver.
Using higher values of $T_p$ implies a more relaxed constraint on the time-limitation of $p(t)$, and hence, the corresponding $T_{\Tilde{p}^*}$ does not increase as we increase $T_p$. Therefore the minimum value of $\max\{T_p, T_{\Tilde{p}}\}$ is achieved when $T_{\Tilde{p}^*}=T_p$. We refer to the corresponding optimal pulse as the MTB pulse since it achieves the minimum time broadening.

In the following, we present the numerical results for three models of the channel: dispersion-only channel, lossless channel, and lossy channel. Although the lossless and lossy channels are more practically relevant, we present the results for the dispersion-only channel too since it approximates well the fiber model in the low power regime.

§.§ Dispersion-only channel

We consider the following values of the parameters in (<ref>): $\beta_2=-21.7$ $\text{ps}^2$/Km, $\gamma=0$ $\text{W}^{-1}\text{Km}^{-1}$, and $\alpha=0$ dB/Km. As the dispersion-only channel is linear, the time broadening of a pulse is not affected by its energy. Consequently, the solutions of (<ref>) for different $E$ are scaled versions of each other and they yield the same $T_{\tilde{p}^*}$. In this section we present the results of (<ref>) for $E=1$ pJ.

Obtained $T_{\tilde{p}^*}$ for sample values of $T_p$, dispersion-only channel for $E=1$ pJ, $L=80$ Km, and $\epsilon=10^{-4}$.

We found the optimal solution $p^*(t)$ of (<ref>) for $T_p\in\{200, 240, 280, 320, 360, 400 \}$ ps and in Fig. <ref> we show the obtained $T_{\tilde{p}^*}$. The straight line in Fig. <ref> creates two regions, in the left one $\max\{T_p, T_{\Tilde{p}^*}\}=T_{\Tilde{p}^*}$ and in the right one $\max\{T_p, T_{\Tilde{p}^*}\}=T_{p}$.
At the intersection, the minimum value of $\max\{T_p, T_{\Tilde{p}^*}\}$ is achieved where $T_{\Tilde{p}^*}=T_p$, hence the modulation interval (defined in (<ref>)) is $T\approx285.5$ ps and the transmission rate $R$ in (<ref>) is $3.5\log_2M$ Gbit/s.
In Fig. <ref> we show the propagation of the obtained pulse $p^*(t)$ that achieves the minimum time broadening for $T_p=285.5$ ps. We refer to this pulse as the MTB pulse.
Using the bandwidth definition in (<ref>), we found that the effective bandwidth of $p^*(t)$ is equal to $29.3$ GHz, which is also equal to the effective bandwidth of $\tilde{p}^*(t)$ since the dispersion-only channel models an all-pass filter. Then the spectral efficiency defined in (<ref>) is equal to $0.12\log_2M$ bit/s/Hz for the dispersion only channel.

The obtained transmission rate depends mainly on the length of the fiber and the chosen isolation level. Therefore, higher transmission rates can be obtained for lower distances or for a lower level of isolation (i.e., higher $\epsilon$). For example, the MTB pulse for $L=40$ Km is found to have $T_{p^*}=T_{\tilde{p}^*}=202$ ps which yields a transmission rate of $5\log_2{M}$ Gbit/s, i.e., an increase of $66.7$%. However the improvement in the spectral efficiency is lower (an increase of $2.8$%) since the effective bandwidth of the MTB pulse is $40.3$ GHz (compared to $29.3$ GHz for $L=80$ Km).

Propagation of the MTB pulse, dispersion-only channel for $E=1$ pJ and $L=80$ Km.

Since the dispersion-only channel is a linear channel, the received signal is $|q(t,L)| = \sum_{k\in\mathbb{Z}} \Tilde{p}_{m_k}(t-kT)$ when $q(t,0) = \sum_{k\in\mathbb{Z}} p_{m_k}(t-kT)$ is transmitted even if the consecutive pulses are not isolated, i.e., if $T$ does not satisfy (<ref>) and (<ref>). In this case, decreasing $T$ requires an equalizer at the receiver to suppress the resulting intersymbol interference. The complexity of the equalizer depends on the number of interfering symbols. For example, the complexity of the Viterbi equalizer increases exponentially with the number of interfering symbols [9].  In this context, the MTB pulses are desirable as they result in a low number of interfering symbols.

§.§ Lossless and Lossy Channels

In this section we use the simulation parameters that we used in Sec. <ref> ($L=80$ Km, $\epsilon=10^{-4}$, $W_{max}=50$ GHz, $\beta_2=-21.7$ $\text{ps}^2$/Km, $\gamma=1.2$ $\text{W}^{-1}\text{Km}^{-1}$, $\alpha=0$ dB/Km for the lossless fiber, and $\alpha=0.2$ dB/Km for the lossy fiber).
We obtained the MTB pulses for sample values of the energy level $E$ that are allowed by solitons, i.e., for $E\leq 1.8$ pJ (for the considered simulation parameters).
For a given energy level $E$, we numerically solve (<ref>) for sample values of $T_p$ and we find the MTB pulse that minimizes $\max\{T_p, T_{\Tilde{p}}\}$ (as done in Sec. <ref> and Fig. <ref>).
We show the obtained duration of MTB pulses in Fig. <ref>, where the results for the dispersion-only channel do not change with $E$ since the dispersion-only channel is linear. The results for lossless and lossy fibers converge to the one of the dispersion-only fibers as $E\to 0$. This is expected since the Kerr effect has lower impact in lower power regimes, where the NLS equation can be approximated by neglecting the nonlinear term (i.e., using $\gamma=0$). For the lossless fibers, the duration of the MTB pulses decreases as $E$ increases, where the minimum duration is $213.9$ ps (achieved at $E=1.8$ pJ). For lossy fibers, the duration of the MTB pulses increases as $E$ increases for $E\leq1.5$ pJ, reaches a minimum of $252.7$ ps at $E=1.5$ pJ, and then increases as $E$ increases beyond $1.5$ pJ.

The transmission rates for OOK are computed based on the minimum duration (as we did for truncated solitons in Sec. <ref>), and we include the corresponding transmission rates in the second column of Table <ref>. The obtained results show improvements (compared to truncated solitons) of $33.8$% and $12$% for OOK over lossy and lossless fibers respectively. For $4$-EM, we show in Fig. <ref> the energy levels that maximize the transmission rates given by (<ref>) while satisfying (<ref>) and (<ref>), where the values of $T$ are $282$ ps and $281$ ps for lossy and lossless fibers respectively. The transmission rates are then computed and shown in Table <ref>. Note that we compute the percentage increase with respect to OOK of truncated  solitons since OOK is the best option when using truncated solitons. We also derive an approximation for the transmission rates of $M$-EM of MTB pulses for $M\geq4$; The modulation interval $T$ can be approximated by the duration of the MTB pulse of the dispersion-only fiber $T\approx285.5$ ps, and hence the transmission rates are approximated by $3.5\log_2{M}$ Gbit/s. Therefore, increasing $M$ increases the transmission rates of EM of isolated MTB pulses, which is the main advantage of MTB pulses over the truncated solitons. Comparing Fig. <ref> and Fig. <ref>, we notice that the obtained MTB pulses achieve lower values of the minimum of $\max\{T_p, T_{\Tilde{p}}\}$ compared to truncated solitons, and hence they outperform truncated solitons in the considered EM system. In Fig. <ref> and  Fig. <ref> we show the transmitted and received MTB pulses in the  $4$-EM system over lossless fiber, which shows that it is possible to use low energy pulses at the cost of a slight increase in $T$.

Achieved duration of MTB pulses for $L=80$ Km and $\epsilon=10^{-4}$.

We compute the time-bandwidth product of the MTB pulses using

\begin{equation*}
c= \max\{T_{p^*}, T_{\tilde{p}^*}\}\cdot \max\{W_{p^*}, W_{\tilde{p}^*}\},
\end{equation*}

and we include them in Fig. <ref>. The obtained results show that the MTB pulses have lower time-bandwidth product compared to truncated solitons. Similarly to Sec. <ref>, we compute the spectral efficiency of OOK and $4$-EM of MTB pulses and we include them in Table <ref>. The approximation of the spectral efficiency for $M\geq4$ is obtained by dividing the approximation of the transmission rates (in Table <ref>) by the maximum allowable bandwidth ($50$ GHz). As shown in Tables <ref> and <ref>, the proposed MTB waveforms outperform the truncated solitons in EM of isolated pulses in terms of transmission rate and spectral efficiency. Moreover, the transmission rate and spectral efficiency of MTB pulses increase as $M$ increases, which is not the case for fundamental solitons.

Transmitted $4$-EM MTB pulses over $80$ Km lossless fiber.

Magnitude of received $4$-EM MTB pulses over $80$ Km lossless fiber.

§ CONCLUSIONS

We introduced waveforms that undergo the minimum time broadening along optical fibers. These waveforms maximize the transmission rates of communication systems that use energy modulation of isolated pulses, and they open the door to finding the maximum achievable rate of such systems. We regard the problem of finding the maximum information theoretic rates as a future research, since solving it requires finding the optimal energy levels and their probabilities based on a given noise model. Another future research is to study the use of these waveforms in intensity modulation direct detection over dispersion-only channels:  pulses with minimum time broadening do not require dispersion compensation and they generate a low number of interfering symbols. We therefore believe that these waveforms could play an important role in complexity-constrained systems. Lastly, the effects of amplifier noise on the designed system are also to be explored.

[1]
G. P. Agrawal, Nonlinear Fiber Optics.
Academic Press, 6th ed., 2019.

[2]
M. I. Yousefi and F. R. Kschischang, “Information Transmission Using the
Nonlinear Fourier Transform, Part III: Spectrum Modulation,” IEEE
Transactions on Information Theory, vol. 60, no. 7, pp. 4346–4369, Apr.

[3]
A. Hasegawa and F. Tappert, “Transmission of stationary nonlinear optical
pulses in dispersive dielectric fibers. I. Anomalous dispersion,” Applied Physics Letters, vol. 23, no. 3, pp. 142–144, Oct. 1973.

[4]
S. Wahls, “Shortening solitons for fiber-optic transmission,” in 2021
17th International Symposium on Wireless Communication Systems (ISWCS),
Berlin , Germany, Jul. 2021.

[5]
A. Span, V. Aref, H. Bülow, and S. ten Brink, “Time-Bandwidth Product
Perspective for Nonlinear Fourier Transform-Based Multi-Eigenvalue Soliton
Transmission,” IEEE Transactions on Communications, vol. 67, no. 8,
pp. 5544–5557, Apr. 2019.

[6]
Y. Chen, I. Tavakkolnia, A. Alvarado, and M. Safari, “On the Capacity of
Amplitude Modulated Soliton Communication over Long Haul Fibers,” Entropy, vol. 22, Aug. 2020.

[7]
P. Halpern, “Optimum finite duration Nyquist signals,” IEEE
Transactions on Communications, vol. 27, no. 6, pp. 884–888, Jun. 1979.

[8]
Y. Jaffal and I. Abou-Faycal, “Achievable rates using PAM time-limited pulses
over band-limited channels: From Nyquist to FTN,” in 2019 IEEE
Wireless Communications and Networking Conference (WCNC), Marrakesh,
Morocco, Apr. 2019.

[9]
Y. Jaffal and A. Alvarado, “Pulses with Minimum Residual Intersymbol
Interference for Faster than Nyquist Signaling,” arXiv preprint
arXiv:2203.07156, Mar. 2022.

[10]
G. Lamb Jr, Introductory Applications of Partial Differential Equations:
With Emphasis on Wave Propagation and Diffusion.
John Wiley & Sons, 1995.

[11]
R. Adelman, N. A. Gumerov, and R. Duraiswami, “Software for Computing the
Spheroidal Wave Functions Using Arbitrary Precision Arithmetic,” arXiv
preprint arXiv:1408.0074, Aug. 2014.