[a,b]

[a]

[c]

[d]

[a]

# Complexity results for modal logic with recursion via translations and
tableaux

Luca Aceto0000-0002-2197-3018  ,  Antonis Achilleos0000-0002-1314-333X  ,
Elli Anastasiadi0000-0001-7526-9256  ,  Adrian Francalanza0000-0003-3829-7391
and  Anna Ingólfsdóttir0000-0001-8362-3075  Dept. of Computer Science,
Reykjavik University, Reykjavik, Iceland<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>Gran Sasso Science Institute L’Aquila, Italy  Dept. of Information
Technology, Uppsala University, Uppsala, Sweden<EMAIL_ADDRESS>Dept. of Computer Science, ICT, University of Malta, Msida, Malta
<EMAIL_ADDRESS>
###### Abstract.

This paper studies the complexity of classical modal logics and of their
extension with fixed-point operators, using translations to transfer results
across logics. In particular, we show several complexity results for multi-
agent logics via translations to and from the $\mu$-calculus and modal logic,
which allow us to transfer known upper and lower bounds. We also use these
translations to introduce a terminating tableau system for the logics we
study, based on Kozen’s tableau for the $\mu$-calculus, and the one of Fitting
and Massacci for modal logic. Finally, we show how to encode the tableaux we
introduced into $\mu$-calculus formulas. This encoding provides upper bounds
for the satisfiability checking of the few logics we previously did not have
algorithms for.

This work has been funded by the projects “Open Problems in the Equational
Logic of Processes (OPEL)” (grant no. 196050), “Epistemic Logic for
Distributed Runtime Monitoring” (grant no. 184940), “Mode(l)s of Verification
and Monitorability” (MoVeMent) (grant no 217987) of the Icelandic Research
Fund, and the project “Runtime and Equational Verification of Concurrent
Programs” (ReVoCoP) (grant 222021) of the Reykjavik University Research Fund.
Part of the work reported in the paper was done while Elli Anastasiadi was at
the Department of Computer Science, Reykjavik University.

##  1\. Introduction

In this paper, we study a family of multi-modal logics with fixed-point
operators that are interpreted over restricted classes of Kripke models. One
can consider these logics as extensions of the usual multi-agent logics of
knowledge and belief [FHMV95] by adding recursion to their syntax or of the
$\mu$-calculus [Koz83] by interpreting formulas over different classes of
frames and thus giving an epistemic interpretation to the modalities. We
define _translations_ between these logics, and we demonstrate how one can
rely on these translations to prove finite-model theorems, complexity bounds,
and tableau termination for each logic in the family, in a systematic fashion.

Modal logic comes in several variations [BvBW06]. Some of these, such as
multi-modal logics of knowledge and belief [FHMV95], are of particular
interest to Epistemology and other application areas. Semantically, the
classical modal logics used in epistemic (but also other) contexts result from
imposing certain restrictions on their models. On the other hand, the modal
$\mu$-calculus [Koz83] can be seen as an extension of the smallest normal
modal logic ${\mathbf{K}}$ with greatest and least fixed-point operators, $\nu
X$ and $\mu X$ respectively.

In this article, we explore the situation where one allows both recursion
(_i.e._ fixed-point) operators in a multi-modal language and imposes
restrictions on the semantic models. In particular, we are interested in the
complexity of satisfiability for the resulting logics. Satisfiability for the
$\mu$-calculus is known to be $\mathsf{EXP}$-complete [Koz83], while for the
modal logics between ${\mathbf{K}}$ and ${\mathbf{S5}}$ the problem is
$\mathsf{PSPACE}$-complete or $\mathsf{NP}$-complete, depending on whether
they have Negative Introspection [Lad77, HR07]. In the multi-modal case,
satisfiability for those modal logics becomes $\mathsf{PSPACE}$-complete, and
is $\mathsf{EXP}$-complete with the addition of a common knowledge operator
[HM92].

Our primary method for proving complexity results is through translations to
and from the multi-modal $\mu$-calculus. We show that we can use surprisingly
simple translations from modal logics without recursion to the base modal
logic ${\mathbf{K}}_{n}$, that is, K with $n$ agent-indexed modalities,
reproving the $\mathsf{PSPACE}$ upper bound for these logics (Theorem 8 and
Corollary 10). These translations and our constructions to prove their
correctness do not generally transfer to the corresponding logics with
recursion. We present translations from specific logics to the $\mu$-calculus
and back, and we discuss the remaining open cases. We discover, through the
existence of our translations, that several restrictions induced on the frames
do not affect the complexity of the satisfiability problem. As a result, we
prove that all logics with axioms among $D$, $T$, and $4$, and the least-
fixed-point fragments of logics that also have $B$, have their satisfiability
in $\mathsf{EXP}$, and a matching lower bound for the logics with axioms from
$D,T$, and $B$ (Corollaries 16 and 17).

To address the limitations of the translation-based approach to proving
complexity results, we then present tableaux for the discussed logics, based
on the ones by Kozen for the $\mu$-calculus [Koz83], and by Fitting and
Massacci for modal logic [Fit72, Mas94]. We give tableau-termination
conditions for every logic with a finite-model property (Theorem 20). Based on
these tableaux, we give a polynomial-space decision procedure for the single-
agent logics with axioms among $D$, $T$, and $4$, thus proving that
satisfiability for these logics is $\mathsf{PSPACE}$-complete (Theorem 27).
Finally, we give a general satisfiability-preserving translation from each
logic to the $\mu$-calculus, using our tableaux. The translation describes a
tableau branch with an exponentially larger $\mu$-calculus formula,
establishing a $\mathsf{2EXP}$-upper bound for all our logics. The
decidability of the satisfiability problem for logics with $B$ or $5$ was an
open problem (see, for example, Remark 3.12, based on [DL13]).

The addition of recursive operators to modal logic increases expressiveness.
An important example is that of _common knowledge_ or _common belief_ , which
can be expressed with a greatest fixed-point thus: $\nu
X.(\varphi\land\bigwedge_{\alpha}[\alpha]X)$, where $\varphi$ describes the
property that is common knowledge, and $\alpha$ ranges over a (finite) set of
agents. However, the combination of epistemic logics and fixed-points can
potentially express more interesting epistemic concepts. For instance, in the
context of a belief interpretation, the formula $\mu
X.\bigvee_{\alpha}([\alpha]\varphi\vee[\alpha]X)$, can be viewed as claiming
that there is a rumour of $\varphi$. It would be interesting to see what other
meaningful sentences of epistemic interest one can express using recursion.
Furthermore, the family of logics we consider allows each agent to behave
according to a different logic. This flexibility allows one to mix different
interpretations of modalities, such as a temporal interpretation for one agent
and an epistemic interpretation for another. Such logics can even resemble
hyper-logics [CS10] if a set of agents represents different streams of
computation. Combinations of epistemic and temporal or hyper-logics have
recently been used to express safety and privacy properties of systems
[BMP15].

The paper is organized as follows. Section 2 gives the necessary background
and an overview of current results. Section 3 defines a class of translations
that provide us with several upper and lower bounds, and identifies conditions
under which they can be composed. In Section 4 we give tableaux systems for
our multi-modal logics with recursion. Section 5 proves a $\mathsf{PSPACE}$
upper bound for the single-agent logics with axioms among $D$, $T$, and $4$;
Section 6 presents the translation that establishes the $\mathsf{2EXP}$ upper
bounds for all the modal logics with recursion. We conclude in Section 7 with
a set of open questions and directions.

This is an extended version of [AAA+22], with complete proofs for our results.
The results from Sections 5 and 6 are also new in this version.

##  2\. Definitions and Background

This section introduces the logics that we study and the necessary background
on the complexity of modal logic and the $\mu$-calculus.

###  2.1. The Multi-Modal Logics with Recursion

We start by defining the syntax of the logics. We consider formulas
constructed from the following grammar:

$\displaystyle\varphi,\psi\in L::$ $\displaystyle=p$ $\displaystyle|~{}~{}\neg
p$ $\displaystyle|~{}~{}\mathtt{tt}$ $\displaystyle|~{}~{}\mathtt{ff}$
$\displaystyle|~{}~{}X$ $\displaystyle|~{}~{}\varphi\land\psi$
$\displaystyle|~{}~{}\varphi\lor\psi$
$\displaystyle|~{}~{}\langle\alpha\rangle\varphi$
$\displaystyle|~{}~{}[\alpha]\varphi$ $\displaystyle|~{}~{}\mu X.\varphi$
$\displaystyle|~{}~{}\nu X.\varphi,$

where $X$ comes from a countably infinite set of logical (or fixed-point)
variables, LVar, $\alpha$ from a finite set of agents, Ag, and $p$ from a
finite set of propositional variables, PVar. When $\text{\sc
Ag}=\\{\alpha\\}$, $\Box\varphi$ stands for $[\alpha]\varphi$, and
$\Diamond\varphi$ for $\langle\alpha\rangle\varphi$. We also write
$[A]\varphi$, with $A\subseteq\text{\sc Ag}$, to mean
$\displaystyle\bigwedge_{\alpha\in A}[\alpha]\varphi$ and $\langle
A\rangle\varphi$ for $\displaystyle\bigvee_{\alpha\in
A}\langle\alpha\rangle\varphi$. As usual, an empty conjunction stands for
$\mathtt{tt}$ and and empty disjunction stands for $\mathtt{ff}$.

A formula is closed when every occurrence of a variable $X$ is in the scope of
recursive operator $\nu X$ or $\mu X$. Henceforth we consider only closed
formulas, unless we specify otherwise.

Moreover, for recursion-free closed formulas we associate the notion of modal
depth, which is the nesting depth of the modal operators111The modal depth of
recursive formulas can be either zero, or infinite. However, this is will not
affect the results we present later onthe .. The modal depth of $\varphi$ is
defined inductively as:

  * •

$md(p)=md(\neg p)=md(\mathtt{tt})=md(\mathtt{ff})=0$, where $p\in\text{\sc
PVar}$,

  * •

$md(\varphi\lor\psi)=md(\varphi\land\psi)=\max(md(\varphi),md(\psi))$, and

  * •

$md([a]\varphi)=md(\langle a\rangle\varphi)=1+md(\varphi)$, where
$a\in\text{\sc Ag}$.

We assume that each recursion variable $X$ appears in a unique fixed-point
formula $\mathsf{fx}(X)$, which is either of the form $\mu X.\varphi$ or $\nu
X.\varphi$. If $\mathsf{fx}(X)$ is a least-fixed-point (_resp._ greatest-
fixed-point) formula, then $X$ is called a least-fixed-point (_resp._
greatest-fixed-point) variable. We can define a partial order over fixed-point
variables, such that $X\leq Y$ iff $\mathsf{fx}(X)$ is a subformula of
$\mathsf{fx}(Y)$, and $X<Y$ when $X\leq Y$ and $X\neq Y$. If $X$ is
$\leq$-minimal among the free variables of $\varphi$, then we define the
_closure_ of $\varphi$ to be $cl(\varphi)=cl(\varphi[\mathsf{fx}(X)/X])$,
where $\varphi[\psi/X]$ is the usual substitution operation. Note that if
$\varphi$ is closed, then $cl(\varphi)=\varphi$.

We define $\mathsf{sub}(\varphi)$ as the set of subformulas of $\varphi$. The
size of $\varphi$, denoted as $|\varphi|$, is the cardinality of
$\mathsf{sub}(\varphi)$, which is bounded by the length of $\varphi$ as a
string of symbols. Negation, $\neg\varphi$, and implication,
$\varphi\rightarrow\psi$, can be defined in the usual way. Then, we define
$\overline{\mathsf{sub}}(\varphi)=\mathsf{sub}(\varphi)\cup\\{\neg\psi\mid\psi\in\mathsf{sub}(\varphi)\\}$.

##### Semantics

We interpret formulas on the states of a _Kripke model_. A Kripke model, or
simply model, is a triple $M=$ $(W,R,V)$ where $W$ is a nonempty set of
states, ${R}\subseteq W\times\text{\sc Ag}\times W$ is a transition relation,
and $V:W\to 2$${}^{\text{\sc PVar}}$ determines the propositional variables
that are true at each state. $(W,R)$ is called a _frame_. We usually write
$(u,v)\in R_{\alpha}$ or $uR_{\alpha}v$ instead of $(u,\alpha,v)\in R$, or
$uRv$, when Ag is a singleton $\\{\alpha\\}$.

Formulas are evaluated in the context of an _environment_ $\rho:\text{\sc
LVar}\to 2^{W}$, which gives values to the logical variables. For an
environment $\rho$, variable $X$, and set $S\subseteq W$, we write
$\rho[X\mapsto S]$ for the environment that maps $X$ to $S$ and all $Y\neq X$
to $\rho(Y)$. The semantics for our formulas is given through a function
${\left\llbracket-\right\rrbracket}_{\mathcal{M}}$, defined in Table 1.

$\displaystyle{\left\llbracket[\alpha]\varphi,\rho\right\rrbracket}$
$\displaystyle=\left\\{s~{}\big{|}~{}\forall t.\ sR_{\alpha}t\text{ implies
}t\in{\left\llbracket\varphi,\rho\right\rrbracket}\right\\},$
$\displaystyle{\left\llbracket\varphi_{1}{\land}\varphi_{2},\rho\right\rrbracket}$
$\displaystyle={\left\llbracket\varphi_{1},\rho\right\rrbracket}\cap{\left\llbracket\varphi_{2},\rho\right\rrbracket},$
$\displaystyle{\left\llbracket\langle\alpha\rangle\varphi,\rho\right\rrbracket}$
$\displaystyle=\left\\{s~{}\big{|}~{}\exists t.\ sR_{\alpha}t\text{ and
}t\in{\left\llbracket\varphi,\rho\right\rrbracket}\right\\},$
$\displaystyle{\left\llbracket\varphi_{1}{\lor}\varphi_{2},\rho\right\rrbracket}$
$\displaystyle={\left\llbracket\varphi_{1},\rho\right\rrbracket}\cup{\left\llbracket\varphi_{2},\rho\right\rrbracket},$
$\displaystyle{\left\llbracket\mu X.\varphi,\rho\right\rrbracket}$
$\displaystyle=\bigcap\left\\{S~{}\big{|}~{}S\supseteq{\left\llbracket\varphi,\rho[X\mapsto
S]\right\rrbracket}\right\\},$ $\displaystyle{\left\llbracket
X,\rho\right\rrbracket}$ $\displaystyle=\rho(X),$
$\displaystyle{\left\llbracket\nu X.\varphi,\rho\right\rrbracket}$
$\displaystyle=\bigcup\left\\{S~{}\big{|}~{}S\subseteq{\left\llbracket\varphi,\rho[X\mapsto
S]\right\rrbracket}\right\\}.$ Table 1. Semantics of modal formulas on a model
$\mathcal{M}=(W,R,V)$. We omit $\mathcal{M}$ from the notation.

The semantics of $\neg\varphi$ is constructed as usual, where
${\left\llbracket\neg
X,\rho\right\rrbracket}_{\mathcal{M}}=W{\setminus}\rho(X)$.

We sometimes use $\mathcal{M},s\models_{\rho}\varphi$ for
$s\in{\left\llbracket\varphi,\rho\right\rrbracket}_{\mathcal{M}}$, and as the
environment has no effect on the semantics of a closed formula $\varphi$, we
often drop it from the notation and write $\mathcal{M},s\models\varphi$ or
$s\in{\left\llbracket\varphi\right\rrbracket}_{\mathcal{M}}$. If
$\mathcal{M},s\models\varphi$, we say that $\varphi$ is true, or satisfied, in
$s$. When the particular model does not matter, or is clear from the context,
we may omit it.

Depending on how we further restrict our syntax and the model, we can describe
several logics. Without further restrictions, the resulting logic is the
$\mu$-calculus [Koz83]. The max-fragment (resp. min-fragment) of the
$\mu$-calculus is the fragment that only allows the $\nu X$ (resp. the $\mu
X$) recursive operator. If $|\text{\sc Ag}|=k\in\mathbb{N}^{+}$ and we allow
no recursive operators (or recursion variables), then we have the basic modal
logic ${\mathbf{K}}_{k}$ (or ${\mathbf{K}}$, if $k=1$), and further
restrictions on the frames can result in a wide variety of modal logics (see,
for instance, [BdRV01]). We give names to the following frame conditions, or
frame constraints, for the case where $\text{\sc Ag}=\\{\alpha\\}$. These
conditions correspond to the usual axioms for normal modal logics — see
[BvBW06, BdRV01, FHMV95], which we will revisit in Section 3.

$D$::

$R$ is serial: $\forall s\exists t,~{}sRt$;

$T$::

$R$ is reflexive: $\forall s,~{}sRs$;

$B$::

$R$ is symmetric: $\forall s,t,~{}{sRt\text{ implies }tRs}$;

$4$::

$R$ is transitive: $\forall s,t,r,$ if $sRt$ and $tRr$ then $sRr$;

$5$::

$R$ is euclidean: $\forall s,t,r,$ if $sRt$ and $sRr$, then $tRr$.

We consider modal logics that are interpreted over models that satisfy a
combination of these constraints for each agent. $T$, which we call Factivity,
is a special case of $D$, which we call Consistency. Constraint $4$ is
Positive Introspection and $5$ is called Negative Introspection.222These are
names for properties or axioms of a logic. When we refer to these conditions
as conditions on a frame or model, we may refer to them with the name of the
corresponding relation condition: seriality, reflexivity, symmetry,
transitivity, and euclidicity. Given a logic ${\mathbf{L}}$ and constraint
$c$, we write ${\mathbf{L}}+c$ for the logic that is interpreted over all
models with frames that satisfy all the constraints of ${\mathbf{L}}$ and $c$.
The name of a single-agent logic is a combination of the constraints that
apply to its frames, including $K$, if the constraints are contained in
$\\{4,5\\}$. Therefore, logic ${\mathbf{D}}$ is ${\mathbf{K}}+D$,
${\mathbf{T}}$ is ${\mathbf{K}}+T$, ${\mathbf{B}}$ is ${\mathbf{K}}+B$,
${\mathbf{K4}}={\mathbf{K}}+4$,
${\mathbf{D4}}={\mathbf{K}}+D+4={\mathbf{D}}+4$, and so on. We use the special
names ${\mathbf{S4}}$ for ${\mathbf{T4}}$ and ${\mathbf{S5}}$ for
${\mathbf{T45}}$. We define a (multi-agent) logic ${\mathbf{L}}$ on Ag as a
map from agents to single-agent logics. ${\mathbf{L}}$ is interpreted on
Kripke models of the form $(W,R,V)$, where for every $\alpha\in\text{\sc Ag}$,
$(W,R_{\alpha})$ is a frame for ${\mathbf{L}}(\alpha)$.

For a logic ${\mathbf{L}}$, ${\mathbf{L}}^{\mu}$ is the logic that results
from ${\mathbf{L}}$ after we allow recursive operators in the syntax — in case
they were not allowed in $\mathbf{L}$. Furthermore, if for every
$\alpha\in\text{\sc Ag}$, ${\mathbf{L}}(\alpha)$ is the same single-agent
logic ${{\mathbf{L}}}$, we write ${\mathbf{L}}$ as ${{\mathbf{L}}}_{k}$, where
$|\text{\sc Ag}|=k$. Therefore, the $\mu$-calculus is
${\mathbf{K}}^{\mu}_{k}$.

From now on, unless we explicitly say otherwise, by a logic, we mean one of
the logics we have defined above. We call a formula satisfiable for a logic
${\mathbf{L}}$, if it is satisfied in some state of a model for
${\mathbf{L}}$.

######  Example 1.

For a formula $\varphi$, we define $Inv(\varphi)=\nu X.(\varphi\land[\text{\sc
Ag}]X)$. $Inv(\varphi)$ asserts that $\varphi$ is true in _all_ reachable
states, or, alternatively, it can be read as an assertion that $\varphi$ is
common knowledge. We dually define $Eve(\varphi)=\mu
X.(\varphi\lor\langle\text{\sc Ag}\rangle X)$, which asserts that $\varphi$ is
true in _some_ reachable state.

###  2.2. Known Results

For logic ${\mathbf{L}}$, the satisfiability problem for ${\mathbf{L}}$, or
${\mathbf{L}}$-satisfiability, is the problem that asks, given a formula
$\varphi$, if $\varphi$ is satisfiable. Similarly, the model checking problem
for ${\mathbf{L}}$ asks if $\varphi$ is true at a given state of a given
finite model.

Ladner [Lad77] established the classical result of
$\mathsf{PSPACE}$-completeness for the satisfiability of $\mathbf{K}$,
$\mathbf{T}$, $\mathbf{D}$, $\mathbf{K4}$, $\mathbf{D4}$, and $\mathbf{S4}$ as
well as $\mathsf{NP}$-completeness for the satisfiability of $\mathbf{S5}$.
Halpern and Rêgo later characterized the $\mathsf{NP}$–$\mathsf{PSPACE}$ gap
for one-action logics by the presence or absence of Negative Introspection
[HR07], resulting in Theorem 1 below. Later, Rybakov and Shkatov proved the
$\mathsf{PSPACE}$-completeness of $\mathbf{B}$ and $\mathbf{T}$ $\mathbf{B}$
in [RS18].

There is plenty of relevant work on the $\mu$-calculus on restricted frames,
mainly in its single-agent form. Alberucci and Facchini examine the
alternation hierarchy of the $\mu$-calculus over reflexive, symmetric, and
transitive frames in [AF09]. D’Agostino and Lenzi have studied the
$\mu$-calculus over different classes of frames in great detail. In [DL10],
they reduce the $\mu$-calculus over finite transitive frames to first-order
logic. In [DL13], they prove that ${\mathbf{S5}}^{\mu}$-satisfiability is
$\mathsf{NP}$-complete, and that the two-agent version of
${\mathbf{S5}}^{\mu}$ does not have the finite-model property. In [DL15], they
consider finite symmetric frames, and they prove that
${\mathbf{B}}^{\mu}$-satisfiability is in 2$\mathsf{EXP}$, and
$\mathsf{EXP}$-hard. They also examine planar frames in [DL18], where they
show that the alternation hierarchy of the $\mu$-calculus over planar frames
is infinite.

######  Theorem 1 ([Lad77, HR07, RS18]).

If
${\mathbf{L}}\in\\{{\mathbf{K}},{\mathbf{T}},{\mathbf{D}},{\mathbf{B}},{\mathbf{T}}{\mathbf{B}},{\mathbf{K4}},{\mathbf{D4}},{\mathbf{S4}}\\}$,
then ${\mathbf{L}}$-satisfiability is $\mathsf{PSPACE}$-complete; and
${\mathbf{L}}+5$-satisfiability and $({\mathbf{L}}+5)^{\mu}$-satisfiability
are $\mathsf{NP}$-complete.

######  Theorem 2 ([HM92]).

If $k>1$ and ${\mathbf{L}}$ has a combination of constraints from $D,T,4,5$
and no recursive operators, then ${\mathbf{L}}_{k}$-satisfiability is
$\mathsf{PSPACE}$-complete.

######  Remark 2.1.

We note that Halpern and Moses in [HM92] only prove these bounds for the cases
of ${\mathbf{K}}_{k},{\mathbf{T}}_{k},{\mathbf{S4}}_{k},{\mathbf{KD45}}_{k},$
and ${\mathbf{S5}}_{k}$; moreover D’Agostino and Lenzi in [DL13] only prove
the $\mathsf{NP}$-completeness of satisfiability for ${\mathbf{S5}}^{\mu}$.
However, it is not hard to see that their respective methods also work for the
rest of the logics of Theorems 1 and 2. ∎

######  Theorem 3 ([Koz83]).

The satisfiability problem for the $\mu$-calculus is $\mathsf{EXP}$-complete.

When a formula is given in conjunction with a model, the question of whether
the given formula holds in this fixed model is called the model checking
problem.

######  Theorem 4 ([EJS01]).

The model checking problem for the $\mu$-calculus is in
${\mathsf{NP}}\cap{\mathsf{coNP}}$.333In fact, the problem is known to be in
${\mathsf{UP}}\cap{\mathsf{coUP}}$, and can be solved in pseudo-polynomial
time — see [Jur98].

Finally we have the following results about the complexity of satisfiability,
when we have recursive operators. Theorem 5 and Proposition 6 have already
been observed in [AAFI20].

######  Theorem 5.

The satisfiability problem for the min- and max-fragments of the
$\mu$-calculus is $\mathsf{EXP}$-complete, even when $|\text{\sc Ag}|=1$.

######  Proof 2.2 (Proof sketch).

It is known that satisfiability for the min- and max-fragments of the
$\mu$-calculus (on one or more action) is $\mathsf{EXP}$-complete. It is in
$\mathsf{EXP}$ due to Theorem 3 and as shown in [Pra81], these fragments
suffice _•_ to describe the PDL formula that is constructed by the reduction
used in [FL79] to prove $\mathsf{EXP}$-hardness for PDL. Therefore, that
reduction can be adjusted to prove that satisfiability for the min- and max-
fragments of the $\mu$-calculus is $\mathsf{EXP}$-complete.

It is not hard to express in logics with both frame constraints and recursion
operators that formula $\varphi$ is common knowledge, with formula $\nu
X.\varphi\land[\text{\sc Ag}]X$. Since validity for ${\mathbf{L}}_{k}$ with
common knowledge (and without recursive operators) and $k>1$ is
$\mathsf{EXP}$-complete [HM92]444Similarly to Remark 2.1, [HM92] does not
explicitly cover all these cases, but the techniques can be adjusted.,
${\mathbf{L}}_{k}^{\mu}$ is ${\mathsf{EXP}}$-hard.

######  Proposition 6.

Satisfiability for ${\mathbf{L}}_{k}^{\mu}$, where $k>1$, is
$\mathsf{EXP}$-hard.

##  3\. Complexity Through Translations

In this section, we examine $\mathbf{L}$-satisfiability and use formula
translations to reduce the satisfiability of one logic to the satisfiability
of another. We investigate the properties of these translations and how they
compose with each other, and we achieve complexity bounds for several logics.

In the context of this chapter, a formula translation from logic
${\mathbf{L}}_{1}$ to logic ${\mathbf{L}}_{2}$ is a mapping $f$ on formulas
such that each formula $\varphi$ is ${\mathbf{L}}_{1}$ -satisfiable if and
only if $f(\varphi)$ is ${\mathbf{L}}_{2}$ -satisfiable. We only consider
translations that can be computed in polynomial time, and therefore, our
translations are polynomial-time reductions, transfering complexity bounds
between logics.

According to Theorem 3, ${\mathbf{K}}^{\mu}_{k}$-satisfiability, that is,
satisfiability for the $\mu$-calculus, is $\mathsf{EXP}$-complete, and
therefore for each logic ${\mathbf{L}}$, we aim to connect
${\mathbf{K}}^{\mu}_{k}$ and ${\mathbf{L}}$ via a sequence of translations in
either direction, to prove complexity bounds for
${\mathbf{L}}$-satisfiability.

###  3.1. Translating Towards ${\mathbf{K}}_{k}$

We begin by presenting translations from logics with more frame conditions to
logics with fewer ones. To this end, we study how taking the closure of a
frame under one condition affects other frame conditions.

####  3.1.1. Composing Frame Conditions

We now discuss how the conditions for frames affect each other. For example,
to construct a transitive frame, one can take the transitive closure of a
possibly non-transitive frame. The resulting frame will satisfy condition $4$.
As we will see, taking the closure of a frame under condition $x$ may affect
whether that frame maintains condition $y$, depending on $x$ and $y$. In the
following, we observe that one can apply the frame closures in certain orders
that preserve the properties one acquires with each application.

We define: Let $F=(W,R)$ be a frame, and $x$ a frame restriction among
$T,B,4,$ and $5$. $R_{\alpha}^{x}$ is the closure of $R_{\alpha}$ under $x$.
For and agent $\alpha\in A\subseteq\text{\sc Ag}$, ${R}^{x,A}$ is defined by

  * •

${R}^{x,A}_{\beta}={R_{\beta}}^{x}$, if $\beta\in A$, and

  * •

${R}^{x,A}_{\beta}=R_{\beta}$, otherwise.

Thus, ${F}^{x,A}=(W,{R}^{x,A})$.

We make the following observation.

######  Lemma 7.

Let $x$ be a frame restriction among $D,T,B,4,$ and $5$, and $y$ a frame
restriction among $T,B,4,$ and $5$, such that
$(x,y)\not\in\\{(4,B),(5,T),(5,B)\\}$. Then, for every frame $F$ that
satisfies $x$, ${F}^{y}$ also satisfies $x$.

According to Lemma 7, frame conditions are preserved as seen in Figure 1.

$4$$T$$B$$5$$D$ Figure 1. The frame property hierarchy

In Figure 1, an arrow from $x$ to $y$ indicates that property $x$ is preserved
though the closure of a frame under $y$. Dotted red arrows indicate one-way
arrows. For convenience, we define ${F}^{D}=(W,{R}^{D})$, where
${R}^{D}=R\cup\\{(s,s)\in W^{2}\mid\centernot{\exists}t:(s,t)\in R\\}$.

######  Remark 3.3.

We note that, in general, not all frame conditions are preserved through all
closures under another condition. For example, the accessibility relation
$\\{(s,t),(t,t)\\}$ is euclidean, but its reflexive closure
$\\{(s,t),(t,t),(s,s)\\}$ is not.

There is at least one linear ordering of the frame conditions $D,T,B,4,$
and$5$, such that all preceding conditions are preserved by closures under the
conditions following them. We call such an order a closure-preserving order.
We use the linear order $D,T,B,4,5$ in the rest of the paper.

For each logic ${\mathbf{L}}$, $\alpha\in\text{\sc Ag}$, and frame $F=(W,R)$,
we also denote $R_{\alpha}^{\mathbf{L}}$ to be the closure of $R_{\alpha}$
under the conditions of ${\mathbf{L}}(\alpha)$;
$R^{\mathbf{L}}=(R_{\alpha}^{\mathbf{L}})_{\alpha\in\text{\sc Ag}}$, and
$F^{\mathbf{L}}=(W,R^{\mathbf{L}})$.

####  3.1.2. Modal Logics

We start with translations that map logics without recursive operators to
logics with fewer constraints. As mentioned in Subsection 2.2, all of the
logics
${\mathbf{L}}\in\\{{\mathbf{K}},{\mathbf{T}},{\mathbf{D}},{\mathbf{K4}},{\mathbf{D4}},{\mathbf{S4}}\\}$
and ${\mathbf{L}}+5$ with one agent have known completeness results, and the
complexity of modal logic is well-studied for multi-agent modal logics as
well. The missing cases are very few and concern the combination of frame
conditions (other than $5$) as well as the multi-agent case. However, we take
this opportunity to present an intuitive introduction to our general
translation method. In fact, the translations that we use for logics without
recursion are surprisingly straightforward. Each frame condition that we
introduced in Section 2 is associated with an axiom for modal logic, such that
whenever a model has the condition, every substitution instance of the axiom
is satisfied in all worlds of the model (see [BvBW06, BdRV01, FHMV95]). For
each frame condition $x$ and agent $\alpha$, we define the axiom
$\mathsf{ax}^{x}_{\alpha}$ as follows:

$\mathsf{ax}^{D}_{\alpha}$: :

$\langle\alpha\rangle\mathtt{tt}$

$\mathsf{ax}^{T}_{\alpha}$: :

$[\alpha]p\rightarrow p$

$\mathsf{ax}^{B}_{\alpha}$: :

$\langle\alpha\rangle[\alpha]p\rightarrow p$

$\mathsf{ax}^{4}_{\alpha}$: :

$[\alpha]p\rightarrow[\alpha][\alpha]p$

$\mathsf{ax}^{5}_{\alpha}$: :

$\langle\alpha\rangle[\alpha]p\rightarrow[\alpha]p$

For each formula $\varphi$ and $d\geq 0$, let
$Inv_{d}(\varphi)=\bigwedge_{i\leq d}[\text{\sc Ag}]^{i}\varphi$, where
$[\text{\sc Ag}]^{0}\varphi=\varphi$ and $[\text{\sc
Ag}]^{i+1}\varphi=[\text{\sc Ag}][\text{\sc Ag}]^{i}\varphi$ . Our first
translations are straightforwardly defined from the above axioms.

######  Translation 3.1 (One-step Translation).

Let $A\subseteq\text{\sc Ag}$ and let $x$ be one of the frame conditions. For
every formula $\varphi$, let $d=md(\varphi)$ if $x\neq 4$, and
$d=md(\varphi)|\varphi|$, if $x=4$. We define:

$\mathsf{F}_{A}^{x}({\varphi})=\varphi\wedge
Inv_{d}\Bigg{(}\bigwedge_{\begin{subarray}{c}\psi\in\overline{\mathsf{sub}}(\varphi)\\\
\alpha\in A\end{subarray}}\mathsf{ax}^{x}_{\alpha}[\psi/p]\Bigg{)}.$

######  Theorem 8.

Let $A\subseteq\text{\sc Ag}$, $x$ be one of the frame conditions, and let
${\mathbf{L}}_{1},{\mathbf{L}}_{2}$ be logics without recursion operators,
such that
${\mathbf{L}}_{1}(\alpha)=\begin{cases}{\mathbf{L}}_{2}(\alpha)+x&\text{ when
}\alpha\in A\\\ {\mathbf{L}}_{2}(\alpha)&\text{ otherwise. }\end{cases}$
Assume that ${\mathbf{L}}_{2}(\alpha)$ only includes frame conditions that
precede $x$ in the fixed order of frame conditions. Then, $\varphi$ is
${\mathbf{L}}_{1}$-satisfiable if and only if $\mathsf{F}_{A}^{x}({\varphi})$
is ${\mathbf{L}}_{2}$-satisfiable.

Before proving this theorem, we will define the _unfolding_ of a model, which
will be used both in this proof but also repeatedly though the paper. Our
definition is a variation of the one in [GO07].

[Tree unfolding, [Sah75, GO07]] Let $\mathcal{M}=(W,R,V)$, and $w_{0}\in W$.
Construct a new model $\mathcal{M}^{\prime}=(W_{u},R^{\prime},V^{\prime})$,
such that:

  * •

$W_{u}$ consists of all finite sequences
$w_{0}\alpha_{1}w_{1}\alpha_{2}\cdots\alpha_{n}w_{n}$ for all $n$, where
$w_{i}\in W$, for every $0\leq i\leq n$, and $w_{i}R_{\alpha_{i+1}}w_{i+1}$,
for every $0\leq i\leq n-1$. We call these $W$-sequences.

  * •

$R_{\alpha}=\\{(u,u\alpha w)\in(W_{u})^{2}\mid w\in W\\}$.

  * •

For every atomic variable $p$, $u\alpha w\in V^{\prime}(p)$ iff $w\in V(p)$.

The pair $\mathcal{M}^{\prime},w_{0}$ is called the _tree unfolding_ of
$\mathcal{M},w_{0}$.

######  Lemma 3.4 ([Sah75]).

The tree unfolding of $\mathcal{M},w$ is bisimilar to $\mathcal{M},w$.
Furthermore, if $\mathcal{M}$ is an ${\mathbf{L}}$-model, then the closure of
the unfolding of $\mathcal{M},w$ under the ${\mathbf{L}}$ conditions is
bisimilar to $\mathcal{M},w$.

######  Proof 3.5.

The first statement follows from [Sah75] – but see also [GO07]. For the second
statement, simply observe that if $\alpha$ has seriality in $\mathcal{M}$, it
does so in the unfolding; and any transition that is introduced to satisfy any
other closure conditions preserves all bisimulations.

We also state the following general observation, for the case of transitive
frames, which will be used in one of the subcases of this theorem.

######  Lemma 9.

Let $\mathcal{M}$ be a Kripke structure. For each $v\in W$ and
$\alpha\in\text{\sc Ag}$, let
$b_{\alpha}(v)=\\{[\alpha]\psi\mid\mathcal{M}^{u},(v)\models[\alpha]\psi\\}$,
and
$d_{\alpha}(v)=\\{\langle\alpha\rangle\psi\mid\mathcal{M}^{u},(v)\models\langle\alpha\rangle\psi\\}$.
Assume $R_{\alpha}$ is transitive and $uR_{\alpha}v$. Then:

  1. (1)

$b_{\alpha}(u)\subseteq b_{\alpha}(v)$, and

  2. (2)

$d_{\alpha}(v)\subseteq d_{\alpha}(u)$

The proof of the above is straightforward, due to the inclusion of any
children worlds of $v$ to the children of $u$ which is enforced by the
transitivity of $R_{\alpha}$. We are now ready to proceed with the proof of
Theorem 8

######  Proof 3.6 (Proof of Theorem 8).

Assume first that $\mathcal{M},w\models\varphi$, where $\mathcal{M}$ is an
${\mathbf{L}}_{1}$-model. For every subformula $\psi$ of $\varphi$ and
$\alpha\in A$, $\mathsf{ax}^{x}_{\alpha}[cl(\psi)/p]$ is an instantiation of
the axiom $\mathsf{ax}^{x}_{\alpha}$, and therefore it holds at all states of
$\mathcal{M}$ that are reachable from $w$. Thus,
$\displaystyle\mathcal{M},w\models
Inv_{d}\Bigg{(}\bigwedge_{\begin{subarray}{c}\psi\in\mathsf{sub}(\varphi)\\\
\alpha\in A\end{subarray}}\mathsf{ax}^{x}_{\alpha}[\psi/p]\Bigg{)}$, which
yields that $\mathcal{M},w\models\mathsf{F}_{A}^{x}({\varphi})$.

For the other direction, assume that
$\mathcal{M},w\models\mathsf{F}_{A}^{x}({\varphi})$ for some
${\mathbf{L}}_{2}$-model $\mathcal{M}=(W,R,V)$ and state $w$. We will use
$\mathcal{M}$ to construct a model for $\varphi$. For convenience and by Lemma
3.4, we assume we are working with the unfolding of $\mathcal{M},w$ which is
defined in Definition 8, something that implies that for every
$\alpha,\beta\in\text{\sc Ag}$, if $\alpha\neq\beta$, then $R_{\alpha}\cap
R_{\beta}=\emptyset$. For each $k\geq 0$, we use the notation
$W_{k}=\\{w\alpha_{1}w_{1}\alpha_{2}\cdots\alpha_{r}w_{r}\in W\mid 0\leq r\leq
k\\}$. Let $d=md(\varphi)$ if $x\neq 4$, and $d=md(\varphi)|\varphi|$, if
$x=4$. We define the models:

  * •

$\mathcal{M}^{c}=(W,R^{{\mathbf{L}}_{2}},V)$;

  * •

$\mathcal{M}^{\prime}=(W^{\prime},R^{\prime},V^{\prime})$, where
$W^{\prime}=W_{d}$, $R^{\prime}$ is the possible $D$-closure for each $\alpha$
where ${\mathbf{L}}(\alpha)$ has $D$, of the restriction of
$R^{\\{}{\mathbf{L}}_{2}\\}$ on $W^{\prime}$, and $V^{\prime}$ is the
restriction of $V$ on $W^{\prime}$; and

  * •

$\mathcal{M}^{x}=(W^{\prime},{R}^{x},V^{\prime})$, where we abuse notation by
denoting ${R^{\prime}}^{x,A}$ as $R^{x}$.

By Lemma 3.4, $\mathcal{M},w$ is bisimilar to $\mathcal{M}^{c},w$. We also
observe that $\mathcal{M}^{\prime}$ remains an ${\mathbf{L}}_{2}$-model:
removing states only affects condition $D$, and the $D$-closure does not
affect the other conditions. Finally, $\mathcal{M}^{x}$ is an
${\mathbf{L}}_{1}$-model.

For the cases where $x\neq 4$, one can see, by induction on $\psi$, and using
Lemma 3.4, that for every formula $\psi$ with $md(\psi)\leq d$, and every
$v\in W_{d-md(\psi)}$, $\mathcal{M}^{c},v\models\psi$ if and only if
$\mathcal{M}^{\prime},v\models\psi$: propositional cases are straightforward,
and modal cases ensure that $md(\psi)>0$, and therefore $v\in W_{d-1}$, so we
can conclude by the inductive hypothesis. Specifically,
$\mathcal{M}^{\prime},w\models\varphi$.

It remains to prove that for every subformula $\psi$ of $\varphi$, and every
$v\in W_{d-md(\psi)}$, $\mathcal{M}^{\prime},v\models\psi$ if and only if
$\mathcal{M}^{x},v\models\psi$.

##### We first handle the case for $x\in\\{D,T\\}$.

We continue by induction on the structure of $\psi$. The propositional and
diamond cases are straightforward, since they are preserved by the
introduction of pairs in the accessibility relation. We now consider the case
of $\psi=[\alpha]\psi^{\prime}$. We observe that $md(\psi)>0$, and therefore
$v\in W_{d-1}$. Specifically, if $md(\psi)=e$, then $v\in W_{d-e}$. If
$\alpha\notin A$, then the accessible states from $v$ remain the same in
$\mathcal{M}^{\prime}$ and in $\mathcal{M}^{x}$, and we are done. Therefore,
we assume that $\alpha\in A$. If there is some $v{R_{\alpha}^{\prime}}^{x}u$,
but not $vR_{\alpha}^{\prime}u$, then we take cases for $x$:

$x=D$:

We observe that $md(\langle\alpha\rangle\mathtt{tt})=1$, and therefore
$\mathcal{M}^{\prime},v\models\langle\alpha\rangle\mathtt{tt}$, since we
observe above that $v\in W_{d-1}$. This contradicts our assumtion that
$v{R_{\alpha}^{\prime}}^{x}u$ but not $vR_{\alpha}^{\prime}u$, due to
definition of ${R_{\alpha}^{\prime}}^{D}$.

$x=T$:

We observe that
$md([\alpha]\psi^{\prime}\rightarrow\psi^{\prime})=md([\alpha]\psi^{\prime})=e$,
and therefore
$\mathcal{M}^{\prime},v\models[\alpha]\psi^{\prime}\rightarrow\psi^{\prime}$,
yielding that $\mathcal{M}^{\prime},v\models\psi^{\prime}$, and, by the
inductive hypothesis, $\mathcal{M}^{x},v\models\psi^{\prime}$. By the
definition of the $T$-closure, $v=u$, and therefore
$\mathcal{M}^{x},u\models\psi^{\prime}$.

##### We now consider the case for $x=B$.

We examine the case for $\psi=[\alpha]\psi^{\prime}$, where $a\in A$. If for
some $v\in W_{d-e}$ and $u\in W_{k}$, $v{R_{\alpha}^{\prime}}^{x}u$, but not
$vR_{\alpha}^{\prime}u$, then we see that $k=d-e-1$, and
$uR_{\alpha}^{\prime}v$. Then,
$\mathcal{M}^{\prime},u\models\langle\alpha\rangle[\alpha]\psi^{\prime}\rightarrow\psi^{\prime}$,
and therefore
$\mathcal{M}^{\prime},u\models\langle\alpha\rangle[\alpha]\psi^{\prime}$ and
we are done by the inductive hypothesis.

##### We now consider the case for $x=5$.

We examine the case for $\psi=[\alpha]\psi^{\prime}$, where $\alpha\in A$. Let
$v{R^{\prime}_{\alpha}}^{x}u$, but not $vR_{\alpha}^{\prime}u$. It suffices to
prove that $\mathcal{M}^{u},u\models\psi^{\prime}$. From our assumption that
$v{R^{\prime}_{\alpha}}^{x}u$, but not $vR_{\alpha}^{\prime}u$, the euclidean
closure condition, and the tree-structure of $\mathcal{M}^{u}$, we can see
that there are some $a,b,c\in W^{\prime}$, such that
$aR^{\prime}_{\alpha}b,c$, and $v$ is $R^{\prime}_{\alpha}$-reachable from
$b$, and $u$ is $R^{\prime}_{\alpha}$-reachable from $c$. Observe that for
every $\psi\in\overline{\mathsf{sub}}(\varphi)$, $\alpha\in A$ and
$v_{1},v_{2}\in W_{d}$, $v_{1}R_{\alpha}^{c}v_{2}$,
$\mathcal{M}^{c},v_{1}\models\langle\alpha\rangle\psi$ implies
$\mathcal{M}^{c},v_{2}\models\langle\alpha\rangle\psi$, and
$\mathcal{M}^{c},v_{2}\models[\alpha]\psi$ implies
$\mathcal{M}^{c},v_{1}\models[\alpha]\psi$.

Assume that $\mathcal{M}^{u},u\not\models\psi^{\prime}$, to reach a
contradiction. We can see that there is some $u^{\prime}$ that is
$R^{\prime}_{\alpha}$-reachable from $a$ and $u^{\prime}R^{u}u$, such that
$\mathcal{M}^{u},u^{\prime}\models\langle\alpha\rangle\neg\psi^{\prime}$; in
other words, $\mathcal{M}^{u},u^{\prime}\not\models[\alpha]\psi^{\prime}$, and
by the definition of $\mathsf{ax}^{5}_{\alpha}$, it must be the case that
$\mathcal{M}^{u},u^{\prime}\not\models\langle\alpha\rangle[\alpha]\psi^{\prime}$.
Therefore, $\mathcal{M}^{u},u^{\prime}\models[\alpha]\neg\psi$, and by the
definition of $\mathsf{ax}^{5}_{\alpha}$, it must be the case that
$\mathcal{M}^{u},a\models[\alpha]\neg\psi$, or, equivallently,
$\mathcal{M}^{u},a\models[\alpha]\langle\alpha\rangle\neg\psi^{\prime}$. In
turn, this yields that
$\mathcal{M}^{u},b\models\langle\alpha\rangle\neg\psi^{\prime}$, and therefore
$\mathcal{M}^{u},v\models\neg\psi$, which is a contradiction.

##### We now consider the case for $x=4$.

For this case, we construct the models $\mathcal{M}^{\prime}$ and
$\mathcal{M}^{x}$ in a different way.

Due to Lemma 9, for all $vR_{\alpha}v^{\prime}$, where $v\in W_{k}$,
$v^{\prime}\in W_{k^{\prime}}$, $\alpha\in A$ and $k\leq d$,
$b_{\alpha}(v)\subseteq b_{\alpha}(v^{\prime})$ and
$d_{\alpha}(v^{\prime})\subseteq d_{\alpha}(v)$. We call a state $pv\in
W_{k+1}$ _$\alpha$ -stable_, when $pR_{\alpha}^{c}pv\in W_{k+1}$, and
$b_{\alpha}(p)=b_{\alpha}(pv)$ and $d_{\alpha}(p)=d_{\alpha}(pv)$ for some
$\alpha\in A$, and write $p\triangleright_{\alpha}pv$. Observe that, by the
Pigeonhole Principle, for $\alpha\in A$, in any sequence
$pR_{\alpha}pv_{1}R_{\alpha}\cdots R_{\alpha}pv_{1}\cdots v_{l}$, where each
$pv_{1}\cdots v_{i}\in W_{i}$ and $l\geq|\varphi|$, there must be an
$\alpha$-stable state.

Let for each $\alpha\notin A$, $R^{4}_{\alpha}=R^{c}_{\alpha}$, and for each
$\alpha\in A$,

$R^{4}_{\alpha}=\\{(a,b)\in R^{c}\mid a\text{ is not
$\alpha$-stable}\\}\cup\\{(a,b)\mid\exists
c\triangleright_{\alpha}a.~{}cR^{c}_{\alpha}b\\}.$

Observe that if $a\triangleright_{\alpha}bR^{c}_{\alpha}c$, then $c$ is not
reachable from $w$ by $R^{4}$.

Let $\mathcal{M}_{4}=(W^{\prime},R^{4},V^{\prime})$ and
$\mathcal{M}^{\prime}=(W^{\prime},R^{\prime},V^{\prime})$, where

$W^{\prime}=\\{v\in W_{d}\mid v\text{ is reachable from }w\text{ by
}R^{4}\\},$

$R^{\prime}$ is the closure of the restriction of $R^{4}$ on $W^{\prime}$
under the ${\mathbf{L}}_{2}$ constraints, and $V^{\prime}$ is the restriction
of $V$ on $W^{\prime}$. $\mathcal{M}^{\prime}$ is now a
${\mathbf{L}}_{2}$-model. We prove, by induction on $\psi$, that for every
formula $\psi\in\mathsf{sub}(\varphi)$ and every $v\in W_{k}\subseteq
W^{\prime}$, where $k\leq d-md(\psi)|\varphi|$, $\mathcal{M}^{c},v\models\psi$
if and only if $\mathcal{M}^{4},v\models\psi$ if and only if
$\mathcal{M}^{\prime},v\models\psi$. The propositional cases are
straightforward for both biimplications.

The modal cases $\psi=\langle\alpha\rangle\psi^{\prime}$ or
$\psi=[\alpha]\psi^{\prime}$ ensure that $md(\psi)>0$, and therefore $v\in
W_{d-1}$, and there is some $(v,u)\in R_{\alpha}^{4}$. We first prove that
$\mathcal{M}^{c},v\models\psi$ if and only if $\mathcal{M}^{4},v\models\psi$.
If $\alpha\notin A$ or $v$ is not $\alpha$-stable, then this case follows from
the observation that the accessible states from $v$ in $\mathcal{M}^{c}$ and
in $\mathcal{M}^{4}$ are the same. If $\alpha\in A$ and
$v^{\prime}\triangleleft v$, then $v^{\prime}$ is not $\alpha$-stable, because
otherwise $v\notin W^{\prime}$, as it would not be reachable from $w$ by
$R^{4}$ in $\mathcal{M}^{c}$. From $v^{\prime}\triangleleft v$, we get that
$\mathcal{M}^{c},v^{\prime}\models\psi$; by the inductive hypothesis, for
every state $uR^{4}_{\alpha}v^{\prime}$,
$\mathcal{M}^{c},u\models\psi^{\prime}$ implies
$\mathcal{M}^{4},u\models\psi^{\prime}$, and since $v^{\prime}$ has the same
accessible states in $\mathcal{M}^{c}$ and in $\mathcal{M}^{4}$,
$\mathcal{M}^{c},v^{\prime}\models\psi$. This completes the induction, and we
conclude that $\mathcal{M}^{c},v\models\psi$ if and only if
$\mathcal{M}^{4},v\models\psi$.

To prove the second biimplication, note that we have that for every formula
$\psi\in\mathsf{sub}(\varphi)$ and every $v=pu\in W_{k}\subseteq\in
W^{\prime}$, where $k\leq d-md(\psi)|\varphi|$, $(pu,puu^{\prime})\in
R^{4}_{\alpha}$. Furthermore, for every $(pu,puu^{\prime})\in R^{4}_{\alpha}$,
we have that $(u,u^{\prime})\in R_{\alpha}$. We then see that, since
$\mathcal{M}$ is an ${\mathbf{L}}_{2}$-model, for every $(pu,puu^{\prime})\in
R^{4}_{\alpha}$, it holds that $(u,u^{\prime})\in R_{\alpha}$. We can then
conclude that $\mathcal{M}^{4},v\models\psi$ if and only if
$\mathcal{M}^{\prime},v\models\psi$. Specifically,
$\mathcal{M}^{\prime},w\models\varphi$.

Let $\mathcal{M}^{x}=(W^{\prime},{R^{\prime}}^{x,A},V^{\prime})$. It is
straightforward now to prove that for every subformula $\psi$ of $\varphi$,
and every $v\in W_{d-md(\psi)}$, $\mathcal{M}^{\prime},v\models\psi$ if and
only if $\mathcal{M}^{x},v\models\psi$, and the proof is complete.

$p,q$$\Box(\neg p\vee\neg q)$$p,\neg q$$\neg p,q$ Figure 2. An example where
the use of the alternative axiom for symetricity would wield a non-valid
translation.

######  Remark 3.7.

The attentive reader must have noted that we used the contra-positive version
of the axioms for symmetric and euclidean conditions on a frame. It turns out
that the original axioms $p\rightarrow\Box\Diamond p$ for symmetricity
($\Diamond p\rightarrow\Box\Diamond p$ for euclidean) would not work with the
translation we defined. To see this consider the case of a translation defined
based on this version of the axiom. A non-symetric frame satisfying the
translation could satisfy some formula of the form $\Box\psi^{\prime}$ in a
world $s$, but not satisfy $\psi^{\prime}$ in all the worlds predecessors
(because at this point $s$’s predecessors are not necessarily connected to
it). The translation would still be valid though, because
$\Box\Diamond\psi^{\prime}$ could be valid in $s$ through it’s successors.
Thus there would not be a way to add symmetric edges to this model without
losing the validity of $\Box\psi^{\prime}$ in $s$. See figure 2 for such an
example.

Theorem 8 together with Ladner’s classic result for the complexity of the
satisfiability of ${\mathbf{K}}$ [Lad77] yield an alternative proof of the
following statement.

######  Corollary 10.

The satisfiability problem for ${\mathbf{L}}+x$, with
$x\in{\mathbf{T}},{\mathbf{D}},{\mathbf{B}},{\mathbf{K4}},{\mathbf{K5}}$,
without fixed-point operators is in $\mathsf{PSPACE}$.

####  3.1.3. Modal Logics with Recursion

In the remainder of this section we will modify our translations and proof
technique, in order to lift our results to logics with fixed-point operators.
It is not clear whether the translations of Subsection 3.1.2 can be extended
straightforwardly in the case of logics with recursion, by using unbounded
invariance $Inv$, instead of the bounded $Inv_{d}$. To see this, consider the
following example.

######  Example 3.8.

Consider the formula $\varphi_{f}=$ $\mu$$X.\Box X$, which requires all paths
in the model to be finite, and thus it is not satisfiable in reflexive frames.
In Subsection 3.1.2, to translate formulas from reflexive models, we did not
need to add the negations of subformulas as conjuncts. In this case, such a
translation would give

$\varphi_{t}:=\varphi_{f}\land
Inv((\Box\varphi_{f}\rightarrow\varphi_{f})\land(\Box\Box\varphi_{f}\rightarrow\Box\varphi_{f})).$

Indeed, on reflexive frames, the formulas
$\Box\varphi_{f}\rightarrow\varphi_{f}$ and
$\Box\Box\varphi_{f}\rightarrow\Box\varphi_{f}$ are valid, and therefore
$\varphi_{t}$ is equivalent to $\varphi_{f}$, which is
$\mathbf{K}$-satisfiable. This was not an issue in Subsection 3.1.2, as the
finiteness of all the paths in a model cannot be expressed without recursion.

One would then naturally wonder whether conjoining over
$\overline{\mathsf{sub}}(\varphi_{f})$ in the translation would make a
difference. The answer is affirmative, as the tranlation

$\varphi_{f}\wedge
Inv\Bigg{(}\bigwedge_{\psi\in\overline{\mathsf{sub}}(\varphi_{f})}\Box\psi\rightarrow\psi\Bigg{)}$

would then yield a formula that is not satisfiable over reflexive frames.
However, our constructions would not work to prove that such a translation
preserves satisfiability. For example, consider $\mu
X.\Box(p\rightarrow(r\land(q\rightarrow X)))$, whose translation is satisfied
on a model that satisfies at the same time $p$ and $q$. We invite the reader
to verify the details.

The only case where the approach that we used for the logics without recursion
can be applied is for the case of seriality (condition $D$), as
$Inv(\langle\alpha\rangle\mathtt{tt})$ directly ensures the seriality of a
model.

######  Translation 3.2.

Let $A\subseteq\text{\sc Ag}$. We define:

$\mathsf{F}_{A}^{D^{\mu}}({\varphi})=\varphi\wedge
Inv\big{(}\bigwedge_{\alpha\in A}\langle\alpha\rangle\mathtt{tt}\big{)}.$

######  Theorem 11.

Let $A\subseteq\text{\sc Ag}$ and $|\text{\sc Ag}|=k$, and let ${\mathbf{L}}$
be a logic, such that ${\mathbf{L}}(\alpha)={\mathbf{D}}$ when $\alpha\in A$,
and ${\mathbf{K}}$ otherwise. Then, $\varphi$ is ${\mathbf{L}}$-satisfiable if
and only if $\mathsf{F}_{A}^{D^{\mu}}({\varphi})$ is
${\mathbf{K}}_{k}^{\mu}$-satisfiable.

For the cases of reflexivity and transitivity, our simple translations
substitute the modal subformulas of a formula to implicitly enforce the
corresponding condition.

######  Translation 3.3.

Let $A\subseteq\text{\sc Ag}$. The function $\mathsf{F}_{A}^{T^{\mu}}({-})$ is
defined homomorphically apart from the following two clauses when $\alpha\in
A$.

  * •

$\mathsf{F}_{A}^{T^{\mu}}({[\alpha]\varphi})=[\alpha]\mathsf{F}_{A}^{T^{\mu}}({\varphi})\wedge\mathsf{F}_{A}^{T^{\mu}}({\varphi})$;

  * •

$\mathsf{F}_{A}^{T^{\mu}}({\langle\alpha\rangle\varphi})=\langle\alpha\rangle\mathsf{F}_{A}^{T^{\mu}}({\varphi})\vee\mathsf{F}_{A}^{T^{\mu}}({\varphi})$,
and;

  * •

$\mathsf{F}_{A}^{T^{\mu}}({-})$ commutes with all other operations.

######  Theorem 12.

Let ${\mathbf{L}}_{1},{\mathbf{L}}_{2}$ be logics, such that
${\mathbf{L}}_{1}(\alpha)={\mathbf{L}}_{2}(\alpha)+T$ when $\alpha\in A$, and
${\mathbf{L}}_{1}(\alpha)={\mathbf{L}}_{2}(\alpha)$ otherwise, and
${\mathbf{L}}_{2}(\alpha)$ at most includes frame condition $D$. Then,
$\varphi$ is ${\mathbf{L}}_{1}$-satisfiable if and only if
$\mathsf{F}_{A}^{T^{\mu}}({\varphi})$ is ${\mathbf{L}}_{2}$-satisfiable.

######  Proof 3.9.

First we assume that $\mathcal{M},w\models\varphi$, where
$\mathcal{M}=(W,R,V)$ is an ${\mathbf{L}}_{1}$-model and $w\in W$. We can
easily verify, by induction on every subformula $\psi$ of $\varphi$ on every
environment $\rho$ and state $s$ of $W$, that
$\mathcal{M},s\models_{\rho}\psi$ if and only if
$\mathcal{M},s\models_{\rho}\mathsf{F}_{A}^{T^{\mu}}({\psi})$. We then
conclude that $\mathcal{M},w\models\mathsf{F}_{A}^{T^{\mu}}({\varphi})$, and
thus the translated formula remains satisfiable.

For the converse implication, we assume an ${\mathbf{L}}_{2}$-model
$\mathcal{M}=(W,R,V)$ and $w\in W$, such that
$\mathcal{M},w\models\mathsf{F}_{A}^{T^{\mu}}({\varphi})$. We construct an
${\mathbf{L}}_{1}$-model that satisfies ${\varphi}$: let
$\mathcal{M}_{p}=(W,R^{p},V^{p})$, where for each $\alpha\in A$,
$R^{p}_{\alpha}=R_{\alpha}\cup\\{(u,u)\mid u\in W\\}$, the reflexive closure
of $R_{\alpha}$, and for each $\alpha\notin A$, $R^{p}_{\alpha}=R_{\alpha}$.
It now suffices to prove that for every $v\in W$, environment $\rho$, and
$\psi\in\mathsf{sub}(\varphi)$,
$\mathcal{M},v\models_{\rho}\mathsf{F}_{A}^{T^{\mu}}({\psi})$ if and only if
$\mathcal{M}_{p},v\models_{\rho}\psi$. We proceed by induction on $\psi$. The
cases of propositional and recursion variables and boolean connectives are
straightforward. The cases of fixed-points are also not hard by using the
inductive hypothesis. Finally, for modalities, it is easy to show that box-
prefixed formulas are preserved by applying a reflexive closure, while no
diamonds are introduced.

######  Translation 3.4.

Let $A\subseteq\text{\sc Ag}$. The function $\mathsf{F}_{A}^{4^{\mu}}({-})$ is
defined to be such that

  * •

$\mathsf{F}_{A}^{4^{\mu}}({[\alpha]\psi})=Inv([\alpha](\mathsf{F}_{A}^{4^{\mu}}({\psi}))$,

  * •

$\mathsf{F}_{A}^{4^{\mu}}({\langle\alpha\rangle\psi})=Eve(\langle\alpha\rangle(\mathsf{F}_{A}^{4^{\mu}}({\psi}))$,
and

  * •

$\mathsf{F}_{A}^{4^{\mu}}({-})$ commutes with all other operations.

######  Theorem 13.

Let $A\subseteq\text{\sc Ag}$, ${\mathbf{L}}_{1},{\mathbf{L}}_{2}$ be logics,
such that ${\mathbf{L}}_{1}(\alpha)={\mathbf{L}}_{2}(\alpha)+4$ when
$\alpha\in A$, and ${\mathbf{L}}_{2}(\alpha)$ otherwise, and
${\mathbf{L}}_{2}(\alpha)$ at most includes frame conditions $D,T,B$. Then,
$\varphi$ is ${\mathbf{L}}_{1}$-satisfiable if and only if
$\mathsf{F}_{A}^{4^{\mu}}({\varphi})$ is ${\mathbf{L}}_{2}$-satisfiable.

######  Proof 3.10.

If $\mathsf{F}_{A}^{4^{\mu}}({\varphi})$ is satisfied in a model $M=(W,R,V)$,
let $M^{\prime}=(W,R^{+},V)$, where $R^{+}_{\alpha}$ is the transitive closure
of $R_{\alpha}$, if $\alpha\in A$, and $R^{+}_{\alpha}=R_{\alpha}$, otherwise.
It is now not hard to use induction on $\psi$ to show that for every (possibly
open) subformula $\psi$ of $\varphi$ and for every environment $\rho$,
${\left\llbracket\mathsf{F}_{A}^{4^{\mu}}({\psi}),\rho\right\rrbracket}_{\mathcal{M}}={\left\llbracket\psi,\rho\right\rrbracket}_{\mathcal{M}^{\prime}}$.
The other direction is more straightforward, similarly demonstrating that if
$\varphi$ is satisfied in an ${\mathbf{L}}_{1}$-model $M=(W,R,V)$ (where
$R_{\alpha}$ is already transitive for $\alpha\in A$), then for every
(possibly open) subformula $\psi$ of $\varphi$ and for every environment
$\rho$,
${\left\llbracket\mathsf{F}_{A}^{4^{\mu}}({\psi}),\rho\right\rrbracket}_{\mathcal{M}}={\left\llbracket\psi,\rho\right\rrbracket}_{\mathcal{M}}$.

In order to produce a similar translation for symmetric frames, we needed to
use a more intricate type of construction. Moreover, we only prove the
correctness of the following translation for formulas without least-fixed-
point operators.

######  Translation 3.5.

Let $A\subseteq\text{\sc Ag}$. The function
$\mathsf{F}_{A}^{{\mathbf{B}}^{\mu}}({-})$ is defined as

$\mathsf{F}_{A}^{{\mathbf{B}}^{\mu}}({\varphi})=\varphi\bigwedge_{\alpha\in
A}Inv\big{(}[\alpha]\langle\alpha\rangle
p\wedge\bigwedge_{\psi\in\overline{\mathsf{sub}}(\varphi)}(\psi\rightarrow[\alpha][\alpha](p\rightarrow\psi))\big{)},$

where $p$ is a new propositional variable, not occurring in $\varphi$.

######  Theorem 14.

Let ${\mathbf{L}}_{1},{\mathbf{L}}_{2}$ be logics, such that
${\mathbf{L}}_{1}(\alpha)={\mathbf{L}}_{2}(\alpha)+{\mathbf{B}}$ when
$\alpha\in A$, and ${\mathbf{L}}_{2}(\alpha)$ otherwise, and
${\mathbf{L}}_{2}(\alpha)$ at most includes frame conditions $D,T$. Then, a
formula $\varphi$ that has no $\mu X$ operators is
${\mathbf{L}}_{1}$-satisfiable if and only if
$\mathsf{F}_{A}^{{\mathbf{B}}^{\mu}}({\varphi})$ is
${\mathbf{L}}_{2}$-satisfiable.

######  Proof 3.11.

First we assume that the $\mu$-free formula $\varphi$ is satisfied in
$\mathcal{M},w$, where $\mathcal{M}=(W,R,V)$ is an ${\mathbf{L}}_{1}$-model
and $w\in W$. We assume that $p\notin V(u)$ for every $u\in W$. We construct
an ${\mathbf{L}}_{2}$-model that satisfies
$\mathsf{F}_{A}^{B^{\mu}}({\varphi})$. Let $\mathcal{M}_{p}=(W_{u}\cup
W_{p},R^{p},V^{p})$ and $\mathcal{M}_{u}=(W_{u}\cup W_{u},R^{u},V^{u})$,
where:

  * •

$\mathcal{M}_{u}$ is the unfolding of $\mathcal{M}$.

  * •

$W_{p}=\\{u_{p}\mid u\in W_{u}\\}$ is a set of distinct copies of states from
$W_{u}$;

  * •

For each $u\in W_{u}$, $V^{p}(u)=V(u)$ and $V^{p}(u_{p})=V(u)\cup\\{p\\}$.

  * •

$R_{\alpha}^{p}=R_{\alpha}^{u}\cup\\{(s_{p},t),(t,s_{p})\mid(s,t)\in
R^{u}_{\alpha}\\}$, if $\alpha\in A$, and $R_{\alpha}^{p}=R_{\alpha}^{u}$
otherwise.

This construction is demonstrated Figure 3.

$s$$t_{1}$$t_{2}$$s_{p}$ Figure 3. The new model, based on a world $s$ in
$\mathcal{M}$, with two neighbors $t_{1},t_{2}$.

It is easy to see that we have $Inv\big{(}[\alpha]\langle\alpha\rangle p)$ in
all worlds $s$ of $\mathcal{M}_{p}$. Namely, for each original world $s$ in
the unfolding, we have that if any world was accessible from it, now there is
a new world $s_{p}$ at distance $2$ from $s$, where $p$ holds. Moreover, since
$\mathcal{M}_{u}$ is an unfolding, all other worlds $t_{p}$ in $W_{p}$ are at
distance strictly larger or smaller than $2$ from $s$ since they have been
only connected to either $s$ itself or to worlds that are not neighbors of
$s$. Since the world $s_{p}$ has identical neighbors and propositional
variables as $s$ we have that they are bissimilar and thus they satisfy the
same formulas. For all worlds $w\in W_{p}$, we have that they can reach
themselves in $2$ steps, and for all other worlds they can reach in $2$ steps
(remember that $\mathcal{M}_{u}$ is an unfolding and thus each world has
exactly one incoming edge), $p$ does not hold. Thus we can also see that the
whole translation of $\varphi$ is satisfied in $\mathcal{M}^{\prime}$.
Furthermore, it is not hard to see that if we take the reflexive closure of
$R_{\alpha}^{p}$ for each $\alpha$ such that ${\mathbf{L}}_{2}(\alpha)$ has
condition $T$, then each state in the resulting model would be bisimilar to
itself in $\mathcal{M}^{p}$; and that the respective serial closure would not
affect the model.

For the converse, we assume an ${\mathbf{L}}_{2}(\alpha)$ model
$\mathcal{M}=(W,R,V)$ and $w\in W$, such that
$\mathcal{M},w\models\mathsf{F}_{A}^{B^{\mu}}({\varphi})$, and we construct an
${\mathbf{L}}_{1}$-model $\mathcal{M}^{\prime}$ that satisfies ${\varphi}$.
Let $\mathcal{M}^{\prime}=(W,R^{\prime},V)$, where $R_{\alpha}^{\prime}$ is
the symmetric closure of $R_{\alpha}$, if $\alpha\in A$, and
$R^{\prime}_{\alpha}=R_{\alpha}$ otherwise. Let $\rho$ be an environment such
that for every $Y$, $\rho(Y)={\left\llbracket cl(Y)\right\rrbracket}$ – that
is, each $X$ is mapped to the interpretation of its recursive closure. We
prove that for every state $v\in W$ that is reachable from $w$ and
$\psi\in\mathsf{sub}(\varphi)$,
$\mathcal{M},v\models_{\rho}\mathsf{F}_{A}^{B^{\mu}}({\psi})$ implies that
$\mathcal{M}^{\prime},v\models_{\rho}\psi$. First, notice that for every
$\alpha\in A$ and $vR_{\alpha}v_{1}R_{\alpha}v_{2}$,
$\mathcal{M},v\models_{\rho}\psi$ iff
$\mathcal{M},v_{2}\models_{\rho}\mathsf{F}_{A}^{B^{\mu}}({\psi})$. We now
proceed by induction on $\psi$.

  * •

Propositional cases, the case of logical variables, and the case of
$\psi=[\alpha]\psi^{\prime}$, where $\alpha\notin A$, are straightforward.

  * •

For the case of $\psi=\langle\alpha\rangle\psi^{\prime}$, notice that
introducing pairs in the accessibility relation preserves diamonds.

  * •

For the case of $\psi=[\alpha]\psi^{\prime}$, where $\alpha\in A$, let
$(v,v^{\prime})\in R^{\prime}_{\alpha}$. It suffices to prove that
$\mathcal{M}^{\prime},v^{\prime}\models\psi^{\prime}$. If $(v,v^{\prime})\in
R_{\alpha}$, then we are done. If not, then $v^{\prime}R_{\alpha}v$, and
therefore there is some $(v,v^{\prime\prime})\in R_{\alpha}$, such that
$\mathcal{M},v^{\prime\prime}\models p$. Therefore,
$\mathcal{M},v^{\prime\prime}\models_{\rho}{\psi^{\prime}}$, yielding
$\mathcal{M},v^{\prime}\models_{\rho}{\psi^{\prime}}$.

  * •

For the case of $\psi=\nu Y.\psi^{\prime}$, notice that
${\left\llbracket\psi^{\prime},\rho[Y\mapsto{\left\llbracket
cl(Y)\right\rrbracket}_{\mathcal{M}}]\right\rrbracket}_{\mathcal{M}^{\prime}}={\left\llbracket\psi^{\prime},\rho\right\rrbracket}_{\mathcal{M}^{\prime}}={\left\llbracket\psi^{\prime},\rho\right\rrbracket}_{\mathcal{M}}$,
by the inductive hypothesis. Therefore,
${\left\llbracket\psi^{\prime},\rho\right\rrbracket}_{\mathcal{M}}\subseteq{\left\llbracket\psi^{\prime},\rho\right\rrbracket}_{\mathcal{M}^{\prime}}$,
which is what we wanted to prove.

######  Remark 3.12.

A translation for euclidean frames and for the full logic on symmetric frames
would need different approaches. D’Agostino and Lenzi show in [DL13] that
${\mathbf{S5}}_{2}^{\mu}$ does not have a finite-model property, and their
result can be easily extended to any logic ${\mathbf{L}}$ with fixed-point
operators, where there are at least two distinct agents $\alpha,\beta$, such
that ${\mathbf{L}}(\alpha)$ and ${\mathbf{L}}(\beta)$ have constraint $B$ or
$5$. Therefore, as our constructions for the translations to
${\mathbf{K}}^{\mu}_{k}$ guarantee the finite-model property for the
corresponding logics, they do not apply to multimodal logics with $B$ or $5$.

###  3.2. Embedding ${\mathbf{K}}_{n}^{\mu}$

In this subsection, we present translations from logics with fewer frame
conditions to ones with more conditions. These translations will allow us to
prove $\mathsf{EXP}$-completeness results in the following subsection. Let
$p,q$ be distinguished propositional variables that do not appear in our
formulas. We let $\vec{p}$ range over $p$, $\neg p$, $p\wedge q$, $p\wedge\neg
q$, and $\neg p\wedge q$.

[Function $next$] $next(p\wedge q)=p\wedge\neg q$, $next(p\wedge\neg q)=\neg
p\wedge q$, and $next(\neg p\wedge q)=p\wedge q$; and $next(p)=\neg p$ and
$next(\neg p)=p$.

We use a uniform translation from ${\mathbf{K}}^{\mu}_{k}$ to any logic with a
combination of conditions $D,T,B$. The intuition behind this translation is to
describe a model where we duplicate worlds and mark them with the values of
$p$ and $q$. Then we use the value of $p$ and $q$ in a world to distinguish
whether the world we are at is a duplicate or a ”true” successor of the
original.

######  Translation 3.6.

Let $A\subseteq\text{\sc Ag}$. The function
$\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({-})$ on formulas is defined such that:

  * •

$\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({\langle\alpha\rangle\psi})=\bigwedge_{\vec{p}}(\vec{p}\rightarrow\langle\alpha\rangle(next(\vec{p})\wedge\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({\psi})))$,
if $\alpha\in A$;

  * •

$\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({[\alpha]\psi})=\bigwedge_{\vec{p}}(\vec{p}\rightarrow[\alpha](next(\vec{p})\rightarrow\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({\psi})))$,
if $\alpha\in A$;

  * •

$\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({-})$ commutes with all other operations.

We note that there are simpler translations for the cases of logics with only
$D$ or $T$ as a constraint, but the $\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({-})$
is uniform for all the logics that we consider in this subsection.

######  Theorem 15.

Let $\emptyset\neq A\subseteq\text{\sc Ag}$, $|\text{\sc Ag}|=k$, and let
${\mathbf{L}}$ be such that ${\mathbf{L}}(\alpha)$ includes only frame
conditions from ${\mathbf{D}},{\mathbf{T}},{\mathbf{B}}$ when $\alpha\in A$,
and ${\mathbf{L}}(\alpha)={\mathbf{K}}$ otherwise. Then, $\varphi$ is
${\mathbf{K}}_{k}^{\mu}$-satisfiable if and only if
$\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({\varphi})$ is
${\mathbf{L}}$-satisfiable.

######  Proof 3.13.

For the “only if” direction, let $\mathcal{M}=(W,R,V)$ be an unfolded model
and $w\in W$ be its root, such that $\mathcal{M},w\models\varphi$. Variables
$p$ and $q$ do not appear in $\varphi$, so we can assume that
$\mathcal{M},w\models p\land q$, and that for each $vR_{\alpha}v^{\prime}$
with $\alpha\in A$, then for each $\vec{p}$, $\mathcal{M},v\models\vec{p}$
implies that $\mathcal{M},v^{\prime}\models next(\vec{p})$. Let
$\mathcal{M}^{\prime}=(W,R^{\prime},V)$, where $R\textasciiacute$ is the
appropriate closure of $R$ under the conditions of ${\mathbf{L}}$. We observe
that for every $\alpha\in A$,
$R_{\alpha}=R_{\alpha}^{\prime}\cap\bigcup_{\vec{p}}{\left\llbracket\vec{p}\right\rrbracket}\times{\left\llbracket
next(\vec{p})\right\rrbracket}$. We prove that for any environment $\rho$, any
$\psi\in\mathsf{sub}(\varphi)$, and any $v\in W$,
$\mathcal{M},v\models_{\rho}\psi$ iff
$\mathcal{M}^{\prime},v\models_{\rho}\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({\psi})$.
The proof proceeds by induction on $\psi$. We fix a $v\in W$ and a $\vec{p}$,
such that $\mathcal{M},v\models\vec{p}$.

  * •

The propositional cases and the case of $\psi=X$ are immediate, and so are the
cases of $\psi=\langle\alpha\rangle\psi^{\prime}$ and
$\psi=[\alpha]\psi^{\prime}$, where $\alpha\notin A$.

  * •

For the case of $\psi=\nu X.\psi^{\prime}$ or $\psi=\mu X.\psi^{\prime}$, note
that due to the inductive hypothesis, for any $S\subseteq W$,
${\left\llbracket\psi^{\prime},\rho[X\mapsto
S]\right\rrbracket}_{\mathcal{M}}={\left\llbracket\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({\psi^{\prime}}),\rho[X\mapsto
S]\right\rrbracket}_{\mathcal{M}^{\prime}}$, and therefore
${\left\llbracket\psi,\rho\right\rrbracket}_{\mathcal{M}}={\left\llbracket\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({\psi}),\rho\right\rrbracket}_{\mathcal{M}^{\prime}}$.

  * •

For the case of $\psi=\langle\alpha\rangle\psi^{\prime}$, where $\alpha\in A$,
$\mathcal{M},v\models_{\rho}\psi$ iff
$\mathcal{M},v\models_{\rho}\langle\alpha\rangle\psi^{\prime}$ iff there is
some $(v,v^{\prime})\in R_{\alpha}$,
$\mathcal{M},v^{\prime}\models_{\rho}\psi^{\prime}$ iff there is some
$(v,v^{\prime})\in R^{\prime}_{\alpha}$, where $\mathcal{M},v^{\prime}\models
next(\vec{p})$, $\mathcal{M},v^{\prime}\models_{\rho}\psi^{\prime}$, iff there
is some $(v,v^{\prime})\in R^{\prime}_{\alpha}$,
$\mathcal{M},v^{\prime}\models next(\vec{p})\wedge\psi^{\prime}$ iff

$\mathcal{M},v^{\prime}\models\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({\langle\alpha\rangle\psi^{\prime}})=\bigwedge_{\vec{p}}(\vec{p}\rightarrow\langle\alpha\rangle(next(\vec{p})\wedge\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({\psi^{\prime}}))).$

  * •

For the case of $\psi=[\alpha]\psi^{\prime}$, where $\alpha\in A$,
$\mathcal{M},v\models_{\rho}\psi$ iff
$\mathcal{M},v\models_{\rho}[\alpha]\psi^{\prime}$ iff for every
$(v,v^{\prime})\in R_{\alpha}$,
$\mathcal{M},v^{\prime}\models_{\rho}\psi^{\prime}$ iff for every
$(v,v^{\prime})\in R^{\prime}_{\alpha}$, where $\mathcal{M},v^{\prime}\models
next(\vec{p})$, $\mathcal{M},v^{\prime}\models_{\rho}\psi^{\prime}$, iff for
every $(v,v^{\prime})\in R^{\prime}_{\alpha}$, $\mathcal{M},v^{\prime}\models
next(\vec{p})\rightarrow\psi^{\prime}$ iff

$\mathcal{M},v^{\prime}\models\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({[\alpha]\psi^{\prime}})=\bigwedge_{\vec{p}}(\vec{p}\rightarrow[\alpha](next(\vec{p})\rightarrow\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({\psi^{\prime}}))),$

which completes the proof by induction.

For the “if” direction, let $\mathcal{M}=(W,R,V)$ be an ${\mathbf{L}}$-model
and $w\in W$, such that
$\mathcal{M},w\models\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({\varphi})$. Let
$\mathcal{M}^{\prime}=(W,R^{\prime},V)$, where for every $\alpha\in A$,
$R^{\prime}_{\alpha}=R_{\alpha}\cap\bigcup_{\vec{p}}{\left\llbracket\vec{p}\right\rrbracket}\times{\left\llbracket
next(\vec{p})\right\rrbracket}$, and for every $\alpha\notin A$,
$R_{\alpha}^{\prime}=R_{\alpha}$. We can prove that for any environment
$\rho$, any $\psi\in\mathsf{sub}(\varphi)$, and any $v\in W$,
$\mathcal{M},v\models_{\rho}\mathsf{F}_{A}^{{\mathbf{K}}^{\mu}}({\psi})$ iff
$\mathcal{M}^{\prime},v\models_{\rho}\psi$. The proof proceeds by induction on
$\psi$ and is very similar to the one for the “only if” direction.

###  3.3. Complexity Results

We observe that our translations all result in formulas of size at most linear
with respect to the original. The exceptions are Translations 3.1 and 3.5,
which have a quadratic cost.

######  Corollary 16.

If ${\mathbf{L}}$ only has frame conditions $D,T$, then its satisfiability
problem is $\mathsf{EXP}$-complete; if ${\mathbf{L}}$ only has frame
conditions $D,T,4$, then its satisfiability problem is in $\mathsf{EXP}$.

######  Proof 3.14.

Immediately from Theorems 11, 12, 13, and 15.

######  Corollary 17.

If ${\mathbf{L}}$ only has frame conditions $D,T,B$, then

  1. (1)

${\mathbf{L}}$-satisfiability is $\mathsf{EXP}$-hard; and

  2. (2)

the restriction of ${\mathbf{L}}$-satisfiability on formulas without $\mu X$
operators is $\mathsf{EXP}$-complete.

######  Proof 3.15.

Immediately from Theorems 11, 12, 14, and 15.

$\\#$ agents | Restrictions on syntax/frames | Upper Bound | Lower Bound
---|---|---|---
| frames with B or 5 | ? |  $\mathsf{EXP}$-hard 6
$\geq 2$ | not B , 5 |  $\mathsf{EXP}$ 16 |  $\mathsf{EXP}$-hard 6
| not 5, not $\mu$. X |  $\mathsf{EXP}$ 17 |  $\mathsf{EXP}$-hard 5
| with 5 (or B4) |  $\mathsf{NP}$ 1 |  $\mathsf{NP}$-hard 1
1 | with 4 |  $\mathsf{EXP}$ 16 |  $\mathsf{PSPACE}$-hard 1
| Any other restrictions |  $\mathsf{EXP}$ 3 |  $\mathsf{EXP}$-hard 3
Table 2. Summary of the complexity of satisfiability checking for various
modal logics with recursion up to Section 3. A logic has the complexity of the
first line from the top of the table that contains its description. The
respective theorems from either this work or already known are linked.

A summary of our results can be seen in Table 2. The only mentioned result
that was already known is that the full $\mu$-calculus over one agent is
$\mathsf{EXP}$-complete.

We can clearly see in this summary that when it comes to single-agent
$\mu$-calculus over transitive frames the bound we have is not tight.
Specifically, the translations established already only guarantee that the
problem is in $\mathsf{EXP}$, but the only available lower bound is
$\mathsf{PSPACE}$-hardness from the corresponding modal logic (without
recursion). Thus, to have a tight bound, we would need to prove that the
satisfiability checking for ${\mathbf{K4}}^{\mu}$ is either in
$\mathsf{PSPACE}$, or that it is $\mathsf{EXP}$-hard.

To apply our translation technique to show membership in $\mathsf{PSPACE}$ we
would need to translate formulas in ${\mathbf{K4}}^{\mu}$ to formulas of some
logic whose satisfiability problem is in $\mathsf{PSPACE}$, and thus our
options would be modal logics without recursion. Among those, ${\mathbf{K4}}$
seems to be the most natural candidate, since the transitivity of its models
can be exploited to optimize the translation. Therefore we could focus our
efforts on removing recursion from formulas in ${\mathbf{K4}}^{\mu}$ while
preserving satisfiability over transitive frames.

The above task might seem relatively easy for $\Box$-free formulas since we
can easily see how to remove consecutive diamonds from formulas due to the
transitivity restriction of the frames. At the same time, we know that writing
a ${\mathbf{K4}}$ formula starting with a box this would immediately extend up
to all reachable nodes from the root and could thus simulate some forms of
recursion.

It turns out, though, that tackling the modalities is much harder and
eventually forbids the use of this method altogether. We demonstrate here our
argument on why such a (trivial) translation would not be possible. To do so,
assume that such a translation exists and consider again the formula
$\varphi_{f}=$ $\mu$$X.\Box X$, which requires all paths in the model to be
finite, from Example 3.8. The formula is both recursive and its satisfiability
is not affected by the transitivity restriction. Therefore, due to the
translation, there should exist property $\phi^{\prime}$ in ${\mathbf{K4}}$
that expresses exactly that all paths of the model are finite, and let $k$ be
the number of subformulas of $\phi^{\prime}$. We now write a formula
$\psi\in{\mathbf{K4}}^{\mu}$ such that $\psi$ is exactly satisfied on a
(transitive) model having $2k$-many worlds connected in a path. Said formula
can even be expressed without recursion and its model $\mathcal{M}$ is shown
in Figure 4 (before the addition of the red edge connecting $n_{i+1}$ to
itself).

$n_{1}$$n_{2}$$\ldots$$n_{i}$$n_{i+1}$$n_{2*k}$ Figure 4. The model
$\mathcal{M}$ of property $\psi$, before and after adding the loop edge.

We now study $\mathcal{M}$ and its relation to $\phi^{\prime}$. We see that we
should have $\mathcal{M}\models\phi^{\prime}$ as all paths of $\mathcal{M}$
are indeed finite. However, the length of the longest path of $\mathcal{M}$ is
$2*k$ which is larger than the modal depth of $\phi^{\prime}$. Moreover, since
$\mathcal{M}$ is transitive we know that as we “move away” from the root node
we have more box-formulas satisfied, due to the transitivity axiom $\Box
p\implies\Box\Box p$, the number of one box-prefixed formulas are a subset of
2-box-prefixed formulas etc. Thus the number of subformulas of $\phi^{\prime}$
satisfiable in the worlds of $\mathcal{M}$ increases the further we move away
from the root. Finally, we know the number of $\Box$ prefixed sub-formulas of
$\phi^{\prime}$ is finite and bounded by $k$.

Thus, there must exist nodes $n_{i}$, $n_{i+1}$, as shown in Figure 4, that
satisfy exactly the same number of box-prefixed subformulas of
$\phi^{\prime}$. We now add the red loop-edge on $n_{i+1}$ as seen in the
figure. The addition of said edge cannot affect the validity of any diamond-
prefixed subformula of $\phi^{\prime}$, since it only extends the reachable
worlds of $n_{i_{i}}$. Regarding the boxes, we inspect whether the addition of
the loop-edge could affect the boxes of $n_{i+1}$. However, the boxes of
$n_{i}$ are the same with those of $n_{i+i}$ (before the addition of the
loop), and due to transitivity and the form of $\mathcal{M}$ the worlds
reachable by $n_{i}$ are exactly $n_{i+1}$ and the worlds reachable by
$n_{i_{1}}$. Therefore, all box-prefixed formulas of $n_{i}$ are also applied
in $n_{i+1}$, and thus the addition of the loop does not “break” any of the
box-formulas of $n_{i+1}$.

We now have constructed the model $\mathcal{M}^{\prime}$ (after the addition
of the red loop-edge), which satisfies identical subformulas of
$\phi^{\prime}$ in the identical worlds as $\mathcal{M}$. Thus it must be that
$\mathcal{M}^{\prime}\models\phi^{\prime}$, which is impossible as
$\phi^{\prime}$ only has models with paths of finite length. This leads us to
a contradiction, and we know that it cannot be the case that there is a
straightforward translation from ${\mathbf{K4}}^{\mu}$ to ${\mathbf{K4}}$.

This indicates that applying the translation method would not be trivial to
obtain this result. Instead we will utilize the tableaux we will now present
in Section 4 to produce a $\mathsf{PSPACE}$ algorithm for the missing tight
bound in the case of satisfiability checking for single agent formulas over
transitive frames.

##  4\. Tableaux for ${\mathbf{L}}_{k}^{\mu}$

We give a sound and complete tableau system for logic ${\mathbf{L}}$.
Furthermore, if ${\mathbf{L}}$ has a finite-model property, then we give
terminating conditions for its tableau. The system that we give in this
section is based on Kozen’s tableaux for the $\mu$-calculus [Koz83] and the
tableaux of Fitting [Fit72] and Massacci [Mas94] for modal logic. We can use
Kozen’s finite model theorem [Koz83] to help us ensure the termination of the
tableau for some of these logics.

######  Theorem 18 ([Koz83]).

There is a computable $\kappa:{\rm Nature}\to{\rm Nature}$, such that every
${\mathbf{K}}_{k}^{\mu}$-satisfiable formula $\varphi$ is satisfied in a model
with at most $\kappa(|\varphi|)$ states.555The tableau in [Koz83] yields an
upper bound of $2^{2^{O(n^{3})}}$ for $\kappa_{0}(n)$, but that bound is not
useful to obtain a “good” decision procedure. The purpose of this section is
not to establish any good upper bound for satisfiability testing, which is
done in Sections 5 and 6.

######  Corollary 19.

If ${\mathbf{L}}$ only has frame conditions $D,T,4$, then there is a
computable $\kappa:{\rm Nature}\to{\rm Nature}$, such that every
${\mathbf{L}}$-satisfiable formula $\varphi$ is satisfied in a model with at
most $\kappa(|\varphi|)$ states.

######  Proof 4.16.

Immediately, from Theorems 18, 11, 12, and 13, and Lemma 7.

######  Remark 4.17.

We note that not all modal logics with recursion have a finite-model property
— see Remark 3.12.

Intuitively, a tableau attempts to build a model that satisfies the given
formula. When it needs to consider two possible cases, it branches, and thus
it may generate several branches. Each branch that satisfies certain
consistency conditions, which we define below, represents a corresponding
model.

Our tableaux use _prefixed formulas_ , that is, formulas of the form
$\sigma~{}\varphi$, where $\sigma\in(\text{\sc Ag}\times{\mathbf{L}})^{*}$ and
$\varphi\in{\mathbf{L}}$; $\sigma$ is the prefix of $\varphi$ in that case,
and we say that $\varphi$ is prefixed by $\sigma$. We note that we separate
the elements of $\sigma$ with a dot. We say that the prefix $\sigma$ is
$\alpha$-flat when $\alpha$ has axiom $5$ and
$\sigma=\sigma^{\prime}.\alpha\langle\psi\rangle$ for some $\psi$. Each prefix
possibly represents a state in a corresponding model, and a prefixed formula
$\sigma~{}\varphi$ declares that $\varphi$ is satisfied in the state
represented by $\sigma$. As we will see below, the prefixes from $(\text{\sc
Ag}\times{\mathbf{L}})^{*}$ allow us to keep track of the diamond formula that
generates a prefix through the tableau rules. For agents with condition $5$,
this allows us to restrict the generation of new prefixes and avoid certain
redundancies, due to the similarity of euclidean binary relations to
equivalence relations [NT85, HR07]. For single-agent logics with condition
$4$, this notation will further let us avoid redundancies and achieve a more
efficient decision procedure — see Section 5.

$\sigma~{}\pi X.\varphi$ (fix) $\sigma~{}\varphi$ $\sigma~{}X$ (X)
$\sigma~{}\mathsf{fx}(X)$ $\sigma~{}\varphi\lor\psi$ (or)
$\sigma~{}\varphi\mid\sigma~{}\psi$ $\sigma~{}\varphi\land\psi$ (and)
$\sigma~{}\varphi$ $\sigma~{}\psi$ $\sigma~{}[\alpha]\varphi$ (B)
$\sigma.\alpha\langle\psi\rangle~{}\varphi$
$\sigma~{}\langle\alpha\rangle\varphi$ (D)
$\sigma.\alpha\langle\varphi\rangle~{}\varphi$ $\sigma~{}[\alpha]\varphi$ (d)
$\sigma.\alpha\langle\varphi\rangle~{}\varphi$ $\sigma~{}[\alpha]\varphi$ (4)
$\sigma.\alpha\langle\psi\rangle~{}[\alpha]\varphi$

where, for rules (B) and (4), $\sigma.\alpha\langle\psi\rangle$ has already
appeared in the branch; and for (D), $\sigma$ is not $\alpha$-flat.

$\sigma.\alpha\langle\psi\rangle~{}[\alpha]\varphi$ (B5)
$\sigma~{}[\alpha]\varphi$
$\sigma.\alpha\langle\psi\rangle~{}\langle\alpha\rangle\varphi$ (D5)
$\sigma.\alpha\langle\psi\rangle.\alpha\langle\varphi\rangle~{}\varphi$
$\sigma.\alpha\langle\psi\rangle~{}[\alpha]\varphi$ (b) $\sigma~{}\varphi$
$\sigma~{}[\alpha]\varphi$ (t) $\sigma~{}\varphi$
$\sigma.\alpha\langle\psi\rangle~{}[\alpha]\varphi$ (B55)
$\sigma.\alpha\langle\psi^{\prime}\rangle~{}[\alpha]\varphi$
$\sigma.\alpha\langle\psi\rangle.\alpha\langle\psi^{\prime}\rangle~{}\langle\alpha\rangle\varphi$
(D55) $\sigma.\alpha\langle\psi\rangle.\alpha\langle\varphi\rangle~{}\varphi$
$\sigma.\alpha\langle\psi\rangle~{}[\alpha]\varphi$ (b4)
$\sigma~{}[\alpha]\varphi$

where, for rule (B55), $\sigma.\alpha\langle\psi^{\prime}\rangle$ has already
appeared in the branch; for rule (D5), $\sigma$ is not $\alpha$-flat, and
$\sigma~{}\langle\alpha\rangle\varphi$ does not appear in the branch; for rule
(D55), $\sigma~{}\langle\alpha\rangle\varphi$ does not appear in the branch.

Table 3. The tableau rules for ${\mathbf{L}}={\mathbf{L}}^{\mu}_{n}$.

The tableau rules that we use appear in Table 3. These include fixed-point and
propositional rules, as well as rules that deal with modalities. Depending on
the logic that each agent $\alpha$ is based on, a different set of rules
applies for $\alpha$: for rule (d), ${\mathbf{L}}(\alpha)$ must have condition
$D$; for rule (t), ${\mathbf{L}}(\alpha)$ must have condition $T$; for rule
(4), ${\mathbf{L}}(\alpha)$ must have condition $4$; for rule (B5), (D5), and
(D55), ${\mathbf{L}}(\alpha)$ must have condition $5$; for (b)
${\mathbf{L}}(\alpha)$ must have condition $B$; and for (b4)
${\mathbf{L}}(\alpha)$ must have both $B$ and $4$. Rule (or) is the only rule
that splits the current tableau branch into two. A tableau branch is
propositionally closed when $\sigma~{}\mathtt{ff}$ or both $\sigma~{}p$ and
$\sigma~{}\neg p$ appear in the branch for some prefix $\sigma$. For each
prefix $\sigma$ that appears in a fixed tableau branch, let $\Phi(\sigma)$ be
the set of formulas prefixed by $\sigma$ in that branch. We use the notation
$\sigma\prec\sigma^{\prime}$ to mean that
$\sigma^{\prime}=\sigma.\sigma^{\prime\prime}$ for some
$\sigma^{\prime\prime}$, in which case $\sigma$ is an ancestor of
$\sigma^{\prime}$. We denote with $\sigma(b)$ the set of prefixes that appear
in a branch $b$.

We define the relation $\xrightarrow{X}$ on prefixed formulas in a tableau
branch as $\chi_{1}\xrightarrow{X}\chi_{2}$, if $\chi_{2}$ was introduced to
the branch by a tableau rule with $\chi_{1}$ as its premise, and $\chi_{1}$ is
not of the form $\sigma~{}Y$, where $X<Y$; then, $\xrightarrow{X}^{+}$ is the
transitive closure of $\xrightarrow{X}$ and $\xrightarrow{X}^{*}$ is its
reflexive and transitive closure. We can also extend this relation to
prefixes, so that $\sigma\xrightarrow{X}\sigma^{\prime}$, if and only if
$\sigma~{}\psi\xrightarrow{X}\sigma^{\prime}~{}\psi^{\prime}$, for some
$\psi\in\Phi(\sigma)$ and $\psi^{\prime}\in\Phi(\sigma^{\prime})$. If in a
branch there is a $\xrightarrow{X}$-sequence where $X$ is a least fixed-point
and appears infinitely often, then the branch is called fixed-point-closed. A
branch is closed when it is either fixed-point-closed or propositionally
closed; if it is not closed, then it is called open.

Now, assume that there is a $\kappa:{\rm Nature}\to{\rm Nature}$, such that
every ${\mathbf{L}}$-satisfiable formula $\varphi$ is satisfied in a model
with at most $\kappa(|\varphi|)$ states. An open tableau branch is called
(_resp. locally_) _maximal_ when all tableau rules (_resp. the tableau rules
that do not produce new prefixes_) have been applied. A branch is called
_sufficient_ for $\varphi$ when it is locally maximal and for every
$\sigma~{}\psi$ in the branch, for which a rule can be applied and has not
been applied to $\sigma~{}\psi$, $|\sigma|>|\text{\sc
Ag}|\cdot\kappa(|\varphi|)^{|\varphi|^{2}}\cdot 2^{2|\varphi|+1}$. A tableau
is called maximal when all of its open branches are maximal, and closed when
all of its branches are closed. It is called sufficiently closed for $\varphi$
if it is propositionally closed, or for some least fixed-point variable $X$,
it has a $\xrightarrow{X}$-path, where $X$ appears at least
$\kappa(|\varphi|)+1$ times. A sufficient branch for $\varphi$ that is not
sufficiently closed is called sufficiently open for $\varphi$.

A tableau for $\varphi$ starts from $\varepsilon~{}\varphi$ and is built using
the tableau rules of Table 3. A tableau proof for $\varphi$ is a closed
tableau for the negation of $\varphi$.

######  Theorem 20 (Soundness, Completeness, and Termination of
${\mathbf{L}}_{k}^{\mu}$-Tableaux).

From the following, the first two are equivalent for any formula $\varphi\in
L$ and any logic ${\mathbf{L}}$. Furthermore, if there is a $\kappa:{\rm
Nature}\to{\rm Nature}$, such that every ${\mathbf{L}}$-satisfiable formula
$\varphi$ is satisfied in a model with at most $\kappa(|\varphi|)$ states,
then all the following are equivallent.

  1. (1)

$\varphi$ has a maximal ${\mathbf{L}}$-tableau with an open branch;

  2. (2)

$\varphi$ is ${\mathbf{L}}$-satisfiable; and

  3. (3)

$\varphi$ has an ${\mathbf{L}}$-tableau with a sufficiently open branch for
$\varphi$.

Here we state and prove certain definitions and lemmata that will be used in
the main proof of this Theorem. For an agent $\alpha\in\text{\sc Ag}$ and a
state $s$ in a model $(W,R,V)$, let $Reach_{\alpha}(s)$ be the states that are
reachable in $W$ by $R_{\alpha}$. We also use $R|_{S}$ for the restriction of
a relation $R$ on a set $S$.

For a logic ${\mathbf{L}}$, we call a state $s$ in a model
$\mathcal{M}=(W,R,V)$ for ${\mathbf{L}}$ _flat_ when for every
$\alpha\in\text{\sc Ag}$ for which ${\mathbf{L}}(\alpha)$ has constraint $5$,
there is a set of states $W_{0}$, such that:

  * •

$Reach_{\alpha}(s)=\\{s\\}\cup W_{0}$;

  * •

$R_{\alpha}|_{Reach_{\alpha}(s)}=E_{0}\cup E_{1}$, where

$E_{0}\subseteq\\{s\\}\times W_{0}$ and

$E_{1}=W_{0}^{2}$; and

  * •

if ${\mathbf{L}}(\alpha)$ has constraint $T$, or $E_{0}\neq\emptyset$ and
${\mathbf{L}}(\alpha)$ has constraint $B$, then $s\in W_{0}$.

######  Lemma 21 ([NT85, HR07]).

Every pointed ${\mathbf{L}}$-model is bisimilar to ${\mathbf{L}}$-model whose
states are all flat.

We are now ready to proceed with our proof of Theorem 20.

######  Proof 4.18 (Proof of Theorem 20).

To prove that 1 implies 2,:

let $b$ be a maximal open branch in the tableau for $\varphi$. We construct a
${\mathbf{K}}_{k}^{\mu}$-model $\mathcal{M}=(W,R,V)$ for $\varphi$ in the
following way. Let $W$ be the set of prefixes that appear in the branch, and
let, for each $\alpha\in\text{\sc Ag}$,

$R_{\alpha}^{0}=\\{\sigma,\sigma.\alpha\langle\psi\rangle\in
W^{2}\\}\cup\left\\{\sigma,\sigma\in W^{2}\mid{\mathbf{L}}(\alpha)\text{ has
}\begin{array}[]{l}\text{ reflexive frames, or }\\\ \text{ serial frames and
}\\\ \forall\psi.\sigma.\alpha\langle\psi\rangle\notin
W^{2}\end{array}\right\\};$

$R_{\alpha}^{1}$ is the symmetric closure of $R_{\alpha}^{0}$, if
${\mathbf{L}}(\alpha)$ has symmetric frames, and it is $R_{\alpha}^{0}$
otherwise; $R_{\alpha}^{2}$ is the euclidean closure of $R_{\alpha}^{1}$, if
${\mathbf{L}}(\alpha)$ has euclidean frames, and it is $R_{\alpha}^{1}$
otherwise; and finally, $R_{\alpha}$ is the transitive closure of
$R_{\alpha}^{2}$, if ${\mathbf{L}}(\alpha)$ has transitive frames, and it is
$R_{\alpha}^{2}$ otherwise. By Lemma 7, $R_{a}$ satisfies all the necessary
closure conditions. We also set $V(p)=\\{\sigma\in W\mid\sigma~{}p\text{
appears in the branch }\\}$.

It is now possible to prove, by straightforward induction, that for every
subformula $\psi$ of $\varphi$, if $\sigma~{}\psi$ appears in the branch, then
for any environment $\rho$, such that $\\{\sigma^{\prime}\in
W\mid\sigma~{}\psi\xrightarrow{X}^{*}\sigma^{\prime}~{}X\\}\subseteq\rho(X)$,
$\sigma\in{\left\llbracket\psi,\rho_{\sigma,\psi}\right\rrbracket}$. The only
interesting cases are fixed-point formulas, so let $\psi=\nu X.\psi^{\prime}$.
Let $S_{X}$ be the set of prefixes of $X$ in the branch. We can immediately
see that if $\sigma~{}X$ appears in the branch, then so does
$\sigma~{}\psi^{\prime}$, and therefore, by the inductive hypothesis,
$S_{X}\subseteq{\left\llbracket\psi,\rho[X\mapsto S_{X}]\right\rrbracket}$.
From the semantics in Table 1,
$\sigma\in{\left\llbracket\psi,\rho\right\rrbracket}$.

On the other hand, if $\psi=\mu X.\psi^{\prime}$, then we prove that if
$\sigma\notin S\subseteq W$, then
$S\not\supseteq{\left\llbracket\psi^{\prime},\rho[X\mapsto
S]\right\rrbracket}$. Let $\Psi=\\{\sigma^{\prime}~{}\chi
S\mid\sigma~{}\psi^{\prime}\xrightarrow{X}^{*}\sigma^{\prime}~{}\chi\text{
}\sigma^{\prime}\notin S\\}$. We know that $\sigma~{}\psi^{\prime}\in\Psi$, so
$\Psi\neq\emptyset$. There are no infinite $\xrightarrow{X}$-paths in the
branch, so there is some $\sigma^{\prime}~{}\psi^{\prime}\in\Psi$, such that
$\sigma^{\prime}~{}\psi^{\prime}\not\xrightarrow{X}^{+}\sigma^{\prime\prime}~{}\psi^{\prime}$
for any $\sigma^{\prime\prime}$. Then, we see that
$\\{\sigma^{\prime\prime}\in
W\mid\sigma^{\prime}~{}\psi\xrightarrow{X}^{*}\sigma^{\prime\prime}~{}X\\}\subseteq
S$, because if
$\sigma^{\prime}~{}\psi\xrightarrow{X}^{*}\sigma^{\prime\prime}~{}X$, then
$\sigma^{\prime}~{}\psi^{\prime}\xrightarrow{X}^{*}\sigma^{\prime\prime}~{}\psi^{\prime}$.
But then, by the inductive hypothesis,
$\sigma^{\prime}\in{\left\llbracket\psi^{\prime},\rho[X\mapsto
S]\right\rrbracket}$, and therefore
$S\not\supseteq{\left\llbracket\psi^{\prime},\rho[X\mapsto
S]\right\rrbracket}$, which was what we wanted to prove.

To prove that 2 implies 3,:

let $\mathcal{M}=(W,R,V)$ be a ${\mathbf{L}}$-model and $w\in W$, such that
$\mathcal{M},w\models\varphi$, and $W$ has at most $\kappa(|\varphi|)$ states.
Let the environment $\rho$ be such that
$\rho(X)={\left\llbracket\mathsf{fx}(X),\rho\right\rrbracket}_{\mathcal{M}}$
for every variable $X$. We say that $\rightarrow\subseteq(W\times L)^{2}$ is a
dependency relation on $\mathcal{M}$ when it satisfies the following
conditions:

  * •:

if $u\models_{\rho}\psi_{1}\land\psi_{2}$, then
$(u,\psi_{1}\land\psi_{2})\rightarrow(u,\psi_{1})$ and
$(u,\psi_{1}\land\psi_{2})\rightarrow(u,\psi_{2})$;

  * •:

if $u\models_{\rho}\psi_{1}\lor\psi_{2}$, then
$(u,\psi_{1}\lor\psi_{2})\rightarrow(u,\psi_{1})$ and
$u\models_{\rho}\psi_{1}$ or
$(u,\psi_{1}\land\psi_{2})\rightarrow(u,\psi_{2})$ and
$u\models_{\rho}\psi_{2}$;

  * •:

if $u\models_{\rho}[\alpha]\psi$, then $(u,[\alpha]\psi)\rightarrow(v,\psi)$
for all $v\in W$, such that $uR_{\alpha}v$;

  * •:

if $u\models_{\rho}\langle\alpha\rangle\psi$, then
$(u,\langle\alpha\rangle\psi)\rightarrow(v,\psi)$ for some $v\in W$, such that
$uR_{\alpha}v\models\psi$;

  * •:

if $u\models_{\rho}\mu X.\psi$ or $u\models_{\rho}\nu X.\psi$, then
$(u,\mathsf{fx}(X))\rightarrow(u,\psi)$; and

  * •:

if $u\models_{\rho}X$, then $(u,X)\rightarrow(u,\mathsf{fx}(X))$.

For each variable $X$ and dependency relation $\rightarrow$, we also define
$\xrightarrow{X}$, such that $(w_{1},\psi_{1})\xrightarrow{X}(w_{2},\psi_{2})$
whenever $(w_{1},\psi_{1})\rightarrow(w_{2},\psi_{2})$ and $\psi_{1}\neq Y$
for all variables $Y$ where $\mathsf{fx}(Y)$ is not a subformula of
$\mathsf{fx}(X)$. We call a dependency relation $\rightarrow$ lfp-finite, if
for every least-fixed-point variable $X$, $X$ appears finitely many times on
every $\xrightarrow{X}$-sequence.

_Claim:_ There is a lfp-finite dependency relation. The claim amounts to the
memoryless determinacy of parity games and it can be proven similarly, as in
[Zie98]. Thus, we fix such a lfp-finite dependency relation.

The tableau starts with $\varepsilon~{}\varphi$ and we can keep expanding this
branch to a sufficient one using the tableau rules, such that every prefix is
mapped to a state in $W$, whenever $\sigma$ is mapped to $u$,
$\mathcal{M},u\models_{\rho}\psi$ for every $\psi\in\Phi(\sigma)$, and if
$\sigma.\alpha\langle\psi\rangle$ to $v$, then $uR_{\alpha}v$; furthermore,
this can be done by following the lfp-finite dependency relation. This is by
straightforward induction on the application of the tableau rules. A special
case are the agents with euclidean accessibility relations, for which we can
use Lemma 21. It is not hard to see that in this way we generate a set of
branches that are not propositionally closed. Furthermore, since the tableau
rule applications follow a lfp-finite dependency relation and $W$ has at most
$\kappa(|\varphi|)$ states, it is not hard to see that for every least-fixed-
point variable $X$, on every $\xrightarrow{X}$-path, $X$ appears at most
$\kappa(|\varphi|)$ times.

To prove that 3 implies 1,:

we assume that there is a sufficient open branch $b$ in a tableau for
$\varphi$ and we demonstrate that $\varphi$ has a maximal tableau with an open
branch — specifically, we construct such an open branch from $b$.

We call a prefix $\sigma$ a leaf when there is no $\sigma^{\prime}\neq\sigma$
in the branch, such that $\sigma\prec\sigma^{\prime}$; we call $\sigma$
productive when a tableau rule on a formula $\sigma~{}\psi$ in the branch can
produce a new prefix. We call $\sigma$ ready if it is of the form
$\sigma^{\prime}.\alpha\langle\psi_{1}\rangle.\alpha\langle\psi_{2}\rangle$,
or if $\sigma$ is not $\alpha$-flat for any $\alpha\in\text{\sc Ag}$.

For each $\sigma~{}\psi$ in $b$ and each least-fixed-point variable $X$, let

$c(\sigma~{}\psi,X)=\max\\{n\mid\text{there is a
}\xrightarrow{X}\begin{array}[]{l}\text{-path that ends in }\sigma~{}\psi,\\\
\text{where }X\text{ appears }n\text{ times}\end{array}\\}.$

Since $b$ is not sufficiently closed, always
$c(\sigma~{}\psi,X)\leq\kappa(|\varphi|)$. We use the notation
$\sigma\sim\sigma^{\prime}$ to mean that
$\sigma=\sigma_{1}.\alpha\langle\psi_{1}\rangle$,
$\sigma=\sigma_{2}.\alpha\langle\psi_{2}\rangle$ for some
$\sigma_{1},\sigma_{2},\alpha$, and $\Phi(\sigma)=\Phi(\sigma^{\prime})$; and
the notation $\sigma\equiv\sigma^{\prime}$ to mean that
$\sigma\sim\sigma^{\prime}$ for every least-fixed-point variable $X$ and
$\psi\in\Phi(\sigma)$, $c(\sigma~{}\psi,X)=c(\sigma^{\prime}~{}\psi,X)$ and
either both are ready, or both $\sigma$ and $\sigma^{\prime}$ are not ready
and $\sigma+1\sim\sigma_{2}$, where
$\sigma=\sigma_{1}.\alpha\langle\psi\rangle$ and
$\sigma^{\prime}=\sigma_{2}.\alpha\langle\psi^{\prime}\rangle$. We then say
that $\sigma$ and $\sigma^{\prime}$ are equivalent.

Every productive leaf $\sigma$ in the branch has an ancestor $e(\sigma)$ that
has more that has a distinct, ready, and $\equiv$-equivalent ancestor; let
$s(\sigma)$ be such an ancestor of $e(\sigma)$. We further assume that
$e(\sigma)$ is the $\prec$-minimal ancestor of $\sigma$ with these properties.
We note that for any two productive leaves $\sigma_{1}$ and $\sigma_{2}$, if
$e(\sigma_{1})\prec\sigma_{2}$, then $e(\sigma_{1})=e(\sigma_{2})$.

Let $b_{0}$ be the branch that results by removing from $b$ all prefixed
formulas of the form $\sigma.\alpha\langle\psi_{1}\rangle~{}\psi_{2}$, where
$e(\sigma^{\prime})\prec\sigma$ for some productive leaf $\sigma^{\prime}$.
Observe that $b_{0}$ is such that each of its productive leafs has an
equivalent ancestor that is not a leaf. To complete the proof, it suffices to
show how to extend any branch $b_{i}$, where each of its productive leafs
$\sigma$ has an equivalent proper ancestor $s(\sigma)$, to a branch $b_{i+1}$
that preserves this property, and has an increased minimum length of its
productive leafs. To form $b_{i+1}$, simply add to $b_{i}$ all formulas of the
form $\sigma.\sigma^{\prime}~{}\psi$, where $s(\sigma).\sigma^{\prime}~{}\psi$
appears in $b_{i}$.

Finally, observe that the finite-model property of ${\mathbf{L}}$ was only
used to prove equivalence with the third statement of the theorem.

######  Corollary 22.

${\mathbf{L}}$-tableaux are sound and complete for ${\mathbf{L}}$.

######  Example 4.19.

Let $\text{\sc Ag}=\\{a,b\\}$ and ${\mathbf{L}}$ be a logic, such that
${\mathbf{L}}(a)={\mathbf{K}}^{\mu}$ and
${\mathbf{L}}(b)={\mathbf{K5}}^{\mu}$. Let

$\displaystyle\varphi_{1}$ $\displaystyle=(p\land\langle a\rangle p)\land\mu
X.(\neg p\vee[a]X)$ $\displaystyle and$ $\displaystyle\varphi_{2}=\langle
b\rangle p\land\mu X.([b]\neg p\vee[b])X.$

As we see in Figure 5, the tableau for $\varphi_{1}$ produces an open branch,
while the one for $\varphi_{2}$ has all of its branches closed, the leftmost
one due to an infinite $\xrightarrow{X}$-sequence.

$\varepsilon~{}(p\land\langle a\rangle p)\land\mu X.(\neg p\vee[a]X)$
$\varepsilon~{}\mu X.(\neg p\vee[a]X)$ $\varepsilon~{}p\land\langle a\rangle
p$ $\varepsilon~{}p$ $\varepsilon~{}\langle a\rangle p$ (fix)
$\varepsilon~{}\neg p\vee[a]X$ $\varepsilon~{}[a]X$ (D) $a\langle
p\rangle~{}p$ (B) $a\langle p\rangle~{}X$ (X) $a\langle p\rangle~{}\mu X.(\neg
p\vee[a]X)$ (fix) $a\langle p\rangle~{}\neg p\vee[a]X$ $a\langle
p\rangle~{}[a]X$ $a\langle p\rangle~{}\neg p$ $\mathtt{x}$ $\varepsilon~{}\neg
p$ $\mathtt{x}$

$\varepsilon~{}\langle b\rangle p\land\mu X.([b]\neg p\vee[b]X)$
$\varepsilon~{}\mu X.([b]\neg p\vee[b]X)$ $\varepsilon~{}\langle b\rangle p$
(D) $b\langle p\rangle~{}p$ (fix) $\varepsilon~{}[b]\neg p\vee[b]X$
$\varepsilon~{}[b]X$ (B) $b\langle p\rangle~{}X$ (X) $b\langle p\rangle~{}\mu
X.([b]\neg p\vee[b]X)$ (fix) $b\langle p\rangle~{}[b]\neg p\vee[b]X$ $b\langle
p\rangle~{}[b]X$ (B5) $\varepsilon~{}[b]X$ (B) $b\langle p\rangle~{}X$ (X) ⋮
$b\langle p\rangle~{}[b]\neg p$ (B5) $\varepsilon~{}[b]\neg p$ (B) $b\langle
p\rangle~{}\neg p$ $\mathtt{x}$ $\varepsilon~{}[b]\neg p$ (B) $b\langle
p\rangle~{}\neg p$ $\mathtt{x}$

Figure 5. Tableaux for $\varphi_{1}$ and $\varphi_{2}$. The dots represent
that the tableau keeps repeating as from the identical node above. The x mark
represents a propositionally closed branch.

##  5\. The case of ${\mathbf{K4}}^{\mu}$

In this section, we prove that the satisfiability problem for the (single-
agent) logics ${\mathbf{K4}}^{\mu}$, ${\mathbf{D4}}^{\mu}$, and
${\mathbf{S4}}^{\mu}$ is in $\mathsf{PSPACE}$, using an optimized decision
procedure based on the tableaux from Section 4. To achieve this, we will
examine how transitivity allows us to restrict the parts of a branch that we
need to examine, in order to verify that a formula is satisfiable.

The tableaux rules we use are shown in Table 4, and are the restriction of the
rules defined in Table 3 to ${\mathbf{K4}}^{\mu}$, ${\mathbf{D4}}^{\mu}$, and
${\mathbf{S4}}^{\mu}$.

$\sigma~{}\pi X.\varphi$ (fix) $\sigma~{}\varphi$ $\sigma~{}X$ (X)
$\sigma~{}\mathsf{fx}(X)$ $\sigma~{}\varphi\lor\psi$ (or)
$\sigma~{}\varphi\mid\sigma~{}\psi$ $\sigma~{}\varphi\land\psi$ (and)
$\sigma~{}\varphi$ $\sigma~{}\psi$ $\sigma~{}\Box\varphi$ (B)
$\sigma.\langle\psi\rangle~{}\varphi$ $\sigma~{}\Diamond\varphi$ (D)
$\sigma.\langle\varphi\rangle~{}\varphi$ $\sigma~{}\Box\varphi$ (d)
$\sigma.\langle\varphi\rangle~{}\varphi$ $\sigma~{}\Box\varphi$ (4)
$\sigma.\langle\psi\rangle~{}\Box\varphi$ $\sigma~{}\Box\varphi$ (t)
$\sigma~{}\varphi$

where, for rules (B) and (4), $\sigma.\langle\psi\rangle$ has already appeared
in the branch.

Table 4. The tableau rules for ${\mathbf{L}}={\mathbf{{\mathbf{K4}}}}^{\mu}$.

Given a branch $b$ and prefix $\sigma\in\sigma(b)$,
$b[\sigma:]=\\{\sigma^{\prime}~{}\psi\mid\sigma.\sigma^{\prime}~{}\psi\in
b\\}$. A branch $b$ for $\varphi$ is called _repeating_ if
$b[\sigma\langle\psi\rangle:]=b[\sigma\langle\psi\rangle\sigma^{\prime}\langle\psi\rangle:]$
for every
$\sigma\langle\psi\rangle\sigma^{\prime}\langle\psi\rangle\in\sigma(b)$.

######  Lemma 23.

Let
${\mathbf{L}}\in\\{{\mathbf{K4}}^{\mu},{\mathbf{D4}}^{\mu},{\mathbf{S4}}^{\mu}\\}$.
A formula $\varphi$ is ${\mathbf{L}}$-satisfiable if and only if it has a
maximal open, repeating branch $b$.

######  Proof 5.20.

Let $\varphi$ be satisfiable. By Corollary 19, $\varphi$ has a finite model
$\mathcal{M}=(W,R,V)$. We revisit the proof of Theorem 20, and specifically
the construction of the tableau from the finite model. We can ensure that when
a new prefix $\sigma\langle\psi\rangle$ is mapped to a state
$u_{\sigma\langle\psi\rangle}$, that state is in a strongly connected
component (SCC) that is maximally deep in the dag of the SCCs in $(W,R)$, such
that $\mathcal{M},u_{\sigma\langle\psi\rangle}\models\psi$. So, if an
extension $\sigma\langle\psi\rangle\sigma^{\prime}\langle\psi\rangle$ is
mapped to some state $v$, then either the SCC of
$u_{\sigma\langle\psi\rangle}$ is not maximal or $v$ and
$u_{\sigma\langle\psi\rangle}$ are in the same SCC, and therefore we can
ensure that $v=u_{\sigma\langle\psi\rangle}$. The reverse direction is
immediate from Theorem 20.

Repeating branches ensure that an algorithm that checks for the satisfiability
of $\varphi$ only needs to consider prefixes of length linear with respect to
$|\varphi|$. We can go further and consider branches with less redundancy: due
to transitivity, the satisfaction of certain diamond formulas in some prefix
may be further postponed.

We call a branch $b$ _terse_ , if no formula appears twice in a prefix, and
for all $\psi_{1}\neq\psi_{2}$, if
$\sigma.\langle\psi_{1}\rangle,\sigma.\langle\psi_{2}\rangle\in\sigma(b)$,
then $\Diamond\psi_{2}$ is not prefixed by any extension of
$\sigma.\langle\psi_{1}\rangle$ in $b$. The branch $b$ is _maximally terse_ ,
if it is terse, and closed under the tableau rules, except $(D)$ and $(d)$,
but if $\sigma~{}\Diamond\psi\in b$ (_resp._ or $\sigma~{}\Box\psi\in b$, if
$(d)$ is a tableau rule), then $\sigma^{\prime}\langle\psi\rangle~{}\psi\in b$
for some $\sigma^{\prime}$, where $\sigma^{\prime}$ is an extension of
$\sigma$ or $\sigma$ is an extension of $\sigma^{\prime}$; and if
$\sigma~{}\Box\psi\in b$ and $\sigma~{}\Diamond\psi^{\prime}\in b$, then
$\sigma^{\prime}\langle\psi^{\prime}\rangle~{}\psi\in b$ for any $\sigma$ that
is an extension of $\sigma^{\prime}\langle\psi^{\prime}\rangle$.

A maximally terse branch $b$ is called $4$-open when $b$ remains open, after
extending the definition of $\xrightarrow{X}$, so that additionally:

  * •

$\sigma~{}\Diamond\psi\xrightarrow{X}\sigma^{\prime}\langle\psi\rangle~{}\psi$
for every $\sigma^{\prime}$, where $\sigma^{\prime}$ is an extension of
$\sigma$ or $\sigma$ is an extension of $\sigma^{\prime}$;

  * •

$\sigma~{}\Box\psi\xrightarrow{X}\sigma^{\prime}\langle\psi\rangle~{}\psi$ for
every $\sigma^{\prime}$, where $\sigma^{\prime}$ is an extension of $\sigma$
or $\sigma$ is an extension of $\sigma^{\prime}$, if $(d)$ is included in the
tableau rules; and

  * •

$\sigma~{}\Box\psi\xrightarrow{X}\sigma^{\prime}\langle\psi^{\prime}\rangle~{}\psi$
for every $\sigma^{\prime}$, where $\sigma$ is an extension of
$\sigma^{\prime}\langle\psi\rangle$ and $\sigma~{}\Diamond\psi^{\prime}\in b$.

######  Lemma 24.

Let
${\mathbf{L}}\in\\{{\mathbf{K4}}^{\mu},{\mathbf{D4}}^{\mu},{\mathbf{S4}}^{\mu}\\}$.
A formula $\varphi$ is ${\mathbf{L}}$-satisfiable if and only if it has a
maximally terse, $4$-open branch.

######  Proof 5.21.

If $\varphi$ has a maximally terse, $4$-open repeating branch, we can
construct a model for $\varphi$, similarly as in the proof of Theorem 20.

Let $\varphi$ be satisfiable and let $b$ be a maximal, open, repeating branch
for $\varphi$ by Lemma 23. Let $b^{-}$ be a maximal terse sub-branch of $b$.
It is immediate that $b^{-}$ is closed under the tableau rules, except $(D)$
and $(d)$. Due to the maximality of $b^{-}$, if $\sigma~{}\Diamond\psi\in
b^{-}$ (_resp._ or $\sigma~{}\Box\psi\in b$, if $(d)$ is a tableau rule), then
$\sigma^{\prime}\langle\psi\rangle~{}\psi\in b$ for some $\sigma^{\prime}$,
where $\sigma^{\prime}$ is an extension of $\sigma$ or $\sigma$ is an
extension of $\sigma^{\prime}$ – otherwise, $b^{-}$ can be extended to a
larger sub-branch of $b$. Since $b$ is repeating, if $\sigma~{}\Box\psi\in
b^{-}$ and $\sigma~{}\Diamond\psi^{\prime}\in b^{-}$, then
$\sigma^{\prime}\langle\psi^{\prime}\rangle~{}\psi\in b^{-}$ for any $\sigma$
that is an extension of $\sigma^{\prime}\langle\psi^{\prime}\rangle^{-}$.
Therefore, $b^{-}$ is maximally terse.

We can extend the definition of $\xrightarrow{X}$, so that

  * •

$\sigma~{}\Diamond\psi\xrightarrow{X}\sigma^{\prime}\langle\psi\rangle~{}\psi$
for every $\sigma^{\prime}$, where $\sigma^{\prime}$ is an extension of
$\sigma$ or $\sigma$ is an extension of $\sigma^{\prime}$;

  * •

$\sigma~{}\Box\psi\xrightarrow{X}\sigma^{\prime}\langle\psi\rangle~{}\psi$ for
every $\sigma^{\prime}$, where $\sigma^{\prime}$ is an extension of $\sigma$
or $\sigma$ is an extension of $\sigma^{\prime}$, if $(d)$ is included in the
tableau rules; and

  * •

$\sigma~{}\Box\psi\xrightarrow{X}\sigma^{\prime}\langle\psi^{\prime}\rangle~{}\psi$
for every $\sigma^{\prime}$, where $\sigma$ is an extension of
$\sigma^{\prime}$ and $\sigma~{}\Diamond\psi\in b$.

By the transitivity of $R$ and following the proof of Theorem 20, since $b$ is
repeating, and due to rule $(4)$, every $\xrightarrow{X}$-cycle in
${\mathbf{B}}^{-}$ corresponds to an infinite $\xrightarrow{X}$-path in $b$,
and therefore $b^{-}$ is $4$-open.

######  Corollary 25.

Let
${\mathbf{L}}\in\\{{\mathbf{K4}}^{\mu},{\mathbf{D4}}^{\mu},{\mathbf{S4}}^{\mu}\\}$.
A formula $\varphi$ is ${\mathbf{L}}$-satisfiable if and only if it is
satisfied in a model of at most $2|\varphi|!-1$ states.

######  Lemma 26.

Let $b$ be a terse branch. If a $\xrightarrow{X}$-path in $b$ visits two
prefixes, then one is an extension of the other.

######  Theorem 27.

The satisfiability problem for ${\mathbf{K4}}^{\mu}$, ${\mathbf{D4}}^{\mu}$,
and ${\mathbf{S4}}^{\mu}$, is $\mathsf{PSPACE}$-complete.

######  Proof 5.22.

$\mathsf{PSPACE}$-hardness results from Theorem 1. We prove that
${\mathbf{K4}}^{\mu}$-, ${\mathbf{D4}}^{\mu}$-, and
${\mathbf{S4}}^{\mu}$-satisfiability is in $\mathsf{PSPACE}$. We describe a
non-deterministic polynomial-space algorithm that, given a formula $\varphi$,
constructs and explores a maximally terse, $4$-open
${\mathbf{K4}}^{\mu}$-branch for $\varphi$, if one exists, and it verifies
that the branch is $4$-open. By Lemma 24, this suffices for checking the
satisfiability of $\varphi$.

Our algorithm can generate and explore a maximally terse branch $b$ with a
depth-first-search on its prefixes. Note that the maximality and $4$-openness
conditions for $b$ require only checking pairs of prefixes where one is an
extension of the other. The algorithm keeps track of the diamond formulas (or
also the box formulas, in case of rule (D)) that have generated a prefix. When
the algorithm has visited a maximally long prefix $\sigma$, it can verify that
it contains no $\xrightarrow{X}$-cycles where $X$ appears. It also verifies
that no $\sigma^{\prime}~{}\Diamond\psi$ is marked as having generated
$\sigma^{\prime}\langle\psi\rangle$, where $\sigma$ extends $\sigma^{\prime}$
but not $\sigma^{\prime}\langle\psi\rangle$. If either of those verifications
fail, the algorithm rejects. The algorithm then backtracks until all these
formulas have generated a prefix. If there is some maximally terse, $4$-open
branch for $\varphi$, then the algorithm will succeed by following that
branch. If, on the other hand, the algorithm succeeds, then the prefixed
formulas it generates form a branch that is terse, as it marks the diamond
formulas that generate a prefix, and verifies that the terseness condition is
satisfied. It is also not hard to see that the generated branch is maximally
terse and $4$-open. The algorithm uses at most polynomial space to store a
maximal prefix, the prefixed formulas, and the markings of these formulas,
while it performs the depth-first-search exploration. The verifications it
performs at each maximal prefix only require polynomial space.

##  6\. Translations through Tableaux

In this section we give a uniform translation from every modal logic with
fixed-points that we have defined in this paper to the $\mu$-calculus. This
translation thus establishes the decidability and an upper complexity bound
for the complexity of satisfiability for all the cases that were not provided
an upper bound via the methods used in Section 3. The key observation in this
section is that we already have prefixed tableau proof systems for our logics,
with the following properties:

  * •

the subformula property, in that all formulas that appear in a tableau are
prefixed subformulas of the starting formula;

  * •

the tableau rules are local, in that they relate formulas prefixed either with
the same prefix, or with prefixes that differ very little from one another;

  * •

when the starting formula is satisfiable, the tableau produces a complete open
branch.

An open branch has a bounded-branching tree structure with respect to the
prefixes; that tree can be infinite. The fact that a model or a branch can be
infinite appears to cause difficulties in deciding the satisfiability of a
logic, especially when symmetry or negative introspection is involved [DL13].
However, we observe that the fixed-points in the $\mu$-calculus, the logic
that is the target of our translations, are explicitly designed to describe
infinite models. Our approach is to view an open branch as a model and to
describe the property that the branch is open via a $\mu$-calculus formula.
The caveat is that our translation results in a formula that can be
exponentially larger than the original, and thus yields a double-exponential
upper bound for the satisfiability problem. For the sake of simplicity, in
what follows we first assume that axiom $5$ is not present. We explain how to
adjust our construction afterwards, to also handle agents with negative
introspection.

For a given formula $\varphi$, we construct a new formula that describes an
open tableau branch for $\varphi$. For that, we introduce exponentially many
new propositional variables, each a directed graph of subformulas of $\varphi$
and their negations, with edges that describe the tableau productions. We then
describe in the $\mu$-calculus that the model describes a propositionally open
branch that is closed under the tableau rules, and then that the branch is
open.

Let $\varphi$ be a formula where all fixed-point variables are distinct, and
let $mV$ be the set of least-fixed-point variables in $\varphi$. Let
${\mathbf{G}}$ be the set of labeled directed graphs of the form
$g=(\Phi,(\xrightarrow{X})_{X\in mV},\ell)$, where
$\Phi\subseteq\overline{\mathsf{sub}}(\varphi)$ is its set of vertices; each
edge is labeled with a variable from $mV$; and each node $\psi$ is
additionally labeled with a set
$\ell(\psi)\subseteq\\{in,out\\}\times\\{tob,bot\\}\times mV$. We use the
notation $\Phi_{g}$, $\xrightarrow{X}_{g}$, and $\ell_{g}$ for $\Phi$,
$\xrightarrow{X}$, and $\ell$, respectively, when
$g=(\Phi,(\xrightarrow{X})_{X\in mV},\ell)$. We also abuse notation and write
that $(\psi,u,v)\in g$ to mean that $\psi\in\Phi_{g}$ and
$(u,v)\in\ell_{g}(\psi)$.

We say that $g=(\Phi,(\xrightarrow{X})_{X\in mV},\ell)\in{\mathbf{G}}$ is
_compatible with the tableau rules_ and write $com(g)$ when for every
$\psi\in\Phi$ and $X\in mV$, where $\psi\neq Y$ for any $X<Y$:

  1. (1)

for every tableau rule of the form
$\frac{\sigma~{}\psi}{\sigma~{}\psi^{\prime}}$, $\psi^{\prime}\in\Phi$ and
$\psi\xrightarrow{X}\psi^{\prime}$;

  2. (2)

for every tableau rule of the form
$\frac{\sigma~{}\psi}{\genfrac{}{}{0.0pt}{1}{\sigma~{}\psi_{1}}{\sigma~{}\psi_{2}}}$,
$\psi_{1}\in\Phi$, $\psi\xrightarrow{X}\psi_{1}$, $\psi_{2}\in\Phi$, and
$\psi\xrightarrow{X}\psi_{2}$;

  3. (3)

for every tableau rule of the form
$\frac{\sigma~{}\psi}{\sigma~{}\psi_{1}~{}\mid~{}\sigma~{}\psi_{2}}$,
$\psi_{1}\in\Phi$ and $\psi\xrightarrow{X}\psi_{1}$, or $\psi_{2}\in\Phi$ and
$\psi\xrightarrow{X}\psi_{2}$;

  4. (4)

for every tableau rule of the form
$\frac{\sigma~{}\psi}{\sigma^{\prime}~{}\psi^{\prime}}$, where
$\sigma^{\prime}$ is a strict extension of $\sigma$, then
$(out,bot)\in\ell(\psi)$;

  5. (5)

for every tableau rule of the form
$\frac{\sigma~{}\psi}{\sigma^{\prime}~{}\psi^{\prime}}$, where $\sigma$ is a
strict extension of $\sigma^{\prime}$, $(out,top)\in\ell(\psi)$; and

  6. (6)

$\neg\psi\notin\Phi$.

Let ${\mathbf{G}}^{t}$ be restriction of ${\mathbf{G}}$ on graphs that are
compatible with the tableau rules.

Let $\alpha\in\text{\sc Ag}$, $\chi\in\overline{\mathsf{sub}}(\varphi)$, and
$g=(\Phi_{g},(\xrightarrow{X}_{g})_{X\in
mV},\ell_{g}),~{}h=(\Phi_{h},(\xrightarrow{X}_{h})_{X\in mV},\ell_{h})\in
G^{t}$. We say that $g$ is an $\alpha\langle\chi\rangle$-child of $h$, and
write $c_{\alpha\langle\chi\rangle}(h,g)$ when:

  1. (1)

$\langle\alpha\rangle\chi\in\Phi_{h}$ and $\chi\in\Phi_{g}$ and
$(in,top)\in\ell_{g}(\chi)$;

  2. (2)

if $[\alpha]\psi\in\Phi_{h}$ and
$\frac{\sigma~{}[\alpha]\psi}{\sigma.\alpha\langle\psi_{1}\rangle~{}\psi_{2}}$
is a tableau rule, then $\psi_{2}\in\Phi_{g}$ and
$(in,top)\in\ell_{g}(\psi_{2})$; and

  3. (3)

if $[\alpha]\psi\in\Phi_{g}$ and
$\frac{\sigma.\alpha\langle\psi_{1}\rangle~{}[\alpha]\psi}{\sigma~{}\psi_{2}}$
is a tableau rule, then $\psi_{2}\in\Phi_{h}$ and
$(in,bot)\in\ell_{h}(\psi_{2})$.

We can similarly define that $g$ is an $\alpha$-child of $h$, and write
$c_{\alpha}(h,g)$, by omitting the first condition.

Observe that the size of ${\mathbf{G}}$ is at most exponential with respect to
$\varphi$ and that it takes at most polynomial time to verify $com(g)$ and
$c(g,h)$.

We use each $g\in G^{t}$ and $\ulcorner\psi\urcorner$, where
$\psi\in\overline{\mathsf{sub}}(\varphi)$, as a propositional variable. Let

$\displaystyle{\mathbf{rules}}:=Inv\left(\bigvee_{g\in
G^{t}}g\land\bigwedge_{g,h\in G^{t}}\neg(g\land
h)\land\bigwedge_{\begin{subarray}{c}g\in G^{t}\\\
\langle\alpha\rangle\psi\in\Phi_{g}\end{subarray}}g\rightarrow\langle\alpha\rangle\bigvee_{c_{\alpha\langle\psi\rangle}(g,h)}h\land\bigwedge_{g\in
G^{t}}g\rightarrow[\alpha]\bigvee_{c_{\alpha}(g,h)}h\right)$

Let $b$ be a tableau branch and $\sigma$ a prefix in $b$. We define
$g_{b}(\sigma)=(\Phi,(\xrightarrow{X}_{g})_{X\in mV},\ell)$, where
$\Phi=\\{\sigma~{}\psi\in b\\}$, for each $X\in mV$, $\xrightarrow{X}_{g}$ is
the restriction of $\xrightarrow{X}$ to $\Phi$, and for each $\psi\in\Phi$,
$(in,top)\in\ell(\psi)$ (_resp._ $(in,bot)\in\ell(\psi)$) iff
$\sigma^{\prime}~{}\psi^{\prime}\xrightarrow{X}\sigma~{}\psi$ for some
$\sigma^{\prime}~{}\psi^{\prime}\in b$, where $\sigma^{\prime}$ is a strict
prefix of $\sigma$ (_resp._ $\sigma$ is a strict prefix of $\sigma^{\prime}$).
Similarly, $(out,top)\in\ell(\psi)$ (_resp._ $(out,bot)\in\ell(\psi)$) iff
$\sigma~{}\psi\xrightarrow{X}\sigma^{\prime}~{}\psi^{\prime}$ for some
$\sigma^{\prime}~{}\psi^{\prime}\in b$, where $\sigma^{\prime}$ is a strict
prefix of $\sigma$ (_resp._ $\sigma$ is a strict prefix of $\sigma^{\prime}$).
We may omit $b$ from $g_{b}(\sigma)$ and write $g(\sigma)$ instead, if $b$ is
clear from the context.

Let $b$ be a tableau branch, $\mathcal{M}=(W,R,V)$ be a model, using $G^{t}$
as the set of propositional variables, and $s\in W$. We say that
$\mathcal{M},s$ _represent_ $b$ when there is a mapping $f:\sigma(b)\to W$,
such that:

  1. (1)

$f(\epsilon)=s$;

  2. (2)

for every $\sigma\in\sigma(b)$, $g(\sigma)\in G^{t}$ and
$\mathcal{M},f(\sigma)\models g_{b}(\sigma)$;

  3. (3)

for every $\sigma\in\sigma(b)$ and $g\in G^{t}$, if
$\mathcal{M},f(\sigma)\models g$, then $g=g_{b}(\sigma)$;

  4. (4)

for every $\sigma.\alpha\langle\psi\rangle\in\sigma(b)$,
$f(\sigma)R_{\alpha}f(\sigma.\alpha\langle\psi\rangle)$; and

  5. (5)

for every $\sigma\in\sigma(b)$ and $s\in W$, $f(\sigma)R_{\alpha}s$ implies
that $f(\sigma.\alpha\langle\psi\rangle)=s$ for some
$\sigma.\alpha\langle\psi\rangle\in\sigma(b)$.

If the above conditions are satisfied, then we use the notation
$f:b\xrightarrow{r}\mathcal{M},s$.

######  Lemma 28.

For every model $\mathcal{M}=(W,R,V)$ and state $s\in W$:

  1. (1)

$\mathcal{M},s\models{\mathbf{rules}}$ if and only if $\mathcal{M},s$
represent some branch that is maximal and not propositionally closed; and

  2. (2)

if $\mathcal{M},s\models{\mathbf{rules}}$ and $\mathcal{M},s$ represent $b$,
then $b$ is maximal and not propositionally closed.

######  Proof 6.23.

We first prove the second statement of the lemma. Let $b$ be represented by
$\mathcal{M},s\models{\mathbf{rules}}$. As every prefix is mapped to a state
that is reachable from $s$ (item 4 of Definition 6), because of item 2, $b$ is
locally maximal. We further observe that item 4 of Definition 6 and the
conjunct

$\bigwedge_{g\in G^{t}}g\rightarrow[\alpha]\bigvee_{c_{\alpha}(g,h)}h$

in ${\mathbf{rules}}$ ensures that $b$ is closed under all box rules; and item
5 of Definition 6 and the conjunct

$\bigwedge_{\begin{subarray}{c}g\in G^{t}\\\
\langle\alpha\rangle\psi\in\Phi_{g}\end{subarray}}g\rightarrow\langle\alpha\rangle\bigvee_{c_{\alpha\langle\psi\rangle}(g,h)}h$

in ${\mathbf{rules}}$ ensures that $b$ is closed under all diamond rules.
Therefore, $b$ is maximal and not propositionally closed.

We now prove the first statement of the lemma. If
$\mathcal{M},s\models{\mathbf{rules}}$, then we demonstrate how to construct a
branch $b$ that is represented by $\mathcal{M},s$, together with the mapping
$f$ of the prefixes to the states that are reachable from $s$, as in
Definition 6. As we have already proven the second part of the lemma, $b$ is
maximal and not propositionally closed. Note that at every state $t$ that is
reachable from $s$, exactly one variable from $G^{t}$ is true, and we call it
$g(t)$. The construction of $b$ is by straightforward recursion:

  * •

The branch $b$ includes the prefix $\varepsilon$, $f(\varepsilon)=s$, and
$g(\varepsilon)=g(s)$.

  * •

For every $\sigma\in\sigma(b)$ and
$\langle\alpha\rangle\psi\in\Phi_{f(\sigma)}$,
$\sigma.\alpha\langle\psi\rangle$ is a prefix in $b$; from the conjunct

$\bigwedge_{\begin{subarray}{c}g\in G^{t}\\\
\langle\alpha\rangle\psi\in\Phi_{g}\end{subarray}}g\rightarrow\langle\alpha\rangle\bigvee_{c_{\alpha\langle\psi\rangle}(g,h)}h$

in ${\mathbf{rules}}$, there is at least one state $t$, such that
$f(\sigma)R_{\alpha}t$ and $c_{\alpha\langle\psi\rangle}(g(f(\sigma)),g(t))$.
Let $f(\sigma.\alpha\langle\psi\rangle)=t$ for one of these states $t$, and
$g(\sigma.\alpha\langle\psi\rangle)=g(t)$.

It is now straightforward to verify that $\mathcal{M},s$ represent $b$.

We are now left to prove that if $\mathcal{M},s$ represent some branch $b$
that is maximal and not propositionally closed, then
$\mathcal{M},s\models{\mathbf{rules}}$. First observe that for every prefix
$\sigma\in\sigma(b)$, $g(\sigma)\in G^{t}$. Together with item 2 of Definition
6, this means that $\mathcal{M},s\models Inv\left(\bigvee_{g\in
G^{t}}g\right)$. Item 3 of Definition 6 yields that $\mathcal{M},s\models
Inv\left(\bigwedge_{g,h\in G^{t}}\neg(g\land h)\right)$; while items 4 and 5
yield that

$\mathcal{M},s\models Inv\left(\bigwedge_{\begin{subarray}{c}g\in G^{t}\\\
\langle\alpha\rangle\psi\in\Phi_{g}\end{subarray}}g\rightarrow\langle\alpha\rangle\bigvee_{c_{\alpha\langle\psi\rangle}(g,h)}h\land\bigwedge_{g\in
G^{t}}g\rightarrow[\alpha]\bigvee_{c_{\alpha}(g,h)}h\right).$

Since $Inc(\varphi_{1})\land Inv(\varphi_{2})$ are logically equivalent to
$Inv(\varphi_{1}\land\varphi_{2})$, it follows that
$\mathcal{M},s\models{\mathbf{rules}}$, which was to be shown.

######  Lemma 29.

For every propositionally open, maximal branch $b$, there is a pointed model
$(\mathcal{M},s)$, such that $\mathcal{M},s$ represent $b$.

######  Proof 6.24.

We define model $\mathcal{M}=(W,R,V)$, such that $W=\sigma(b)$,
$R_{\alpha}=\\{(\sigma,\sigma.\alpha\langle\psi\rangle)\in W^{2}\\}$ for each
$\alpha\in\text{\sc Ag}$, and $V(\sigma)=g(\sigma)$ for each $\sigma\in W$;
and $s=\varepsilon$. It is now straightforward to verify that $\mathcal{M},s$
represent $b$.

Let $X\in mV$. For a certain prefix $\sigma$ of the tableau, we want to
describe that there is no $\xrightarrow{X}$-path where $X$ appears infinitely
often. Infinite $\xrightarrow{X}$-paths may include infinitely many prefixed
formulas, or a cycle with finitely many formulas. From a local view on a
tableau prefix, it can be hard to tell whether two paths are part of the same
infinite path of concern. Thus, we need to rule out all possible combinations
of paths that, combined with paths inside other prefixes, can give us
infinitely many occurrences of $X$.

We use the additional notation: we write $(\psi_{1},\psi_{2})\in g$ to mean
that $(\psi_{1},in,top)\in g$ and $(\psi_{2},out,top)\in g$; and for
$(\langle\alpha\rangle\psi_{1},out,bot),(\psi_{2},in,bot)\in g$, we define
$nx(\langle\alpha\rangle\psi_{1},\psi_{2})=(\psi_{1},[\alpha]\psi_{2})$ and
$\alpha(\langle\alpha\rangle\psi_{1},\psi_{2})=\alpha$.

Given a graph $g=(\Phi,(\xrightarrow{X})_{X\in mV},\ell)\in G$,
$T=(\psi_{1},\psi_{2})\in(\overline{\mathsf{sub}}(\varphi))^{2}$,
$S\subseteq(\overline{\mathsf{sub}}(\varphi))^{2}$, and $X\in mV$, we write
$T\xrightarrow{g,X}S$ to mean that

  1. (1)

$\psi_{1},\psi_{2}\in\Phi$, $(in,top)\in\ell(\psi_{1})$,
$(out,top)\in\ell(\psi_{2})$,

  2. (2)

for each $(\psi_{1}^{\prime},\psi_{2}^{\prime})\in S$,
$\psi_{1}^{\prime},\psi_{2}^{\prime}\in\Phi$,
$(out,bot)\in\ell(\psi_{1}^{\prime})$, $(in,bot)\in\ell(\psi_{2}^{\prime})$,
and

  3. (3)

$\\{\psi_{1}^{\prime},\psi_{2}^{\prime},X\mid(\psi_{1}^{\prime},\psi_{2}^{\prime})\in
S\\}$ are on a path from $\psi_{1}$ to $\psi_{2}$ in
$(\Phi,\xrightarrow{X}\cup\\{(\psi_{2},\psi_{1})\\}\cup S)$.

We write $\emptyset\xrightarrow{g,X}S$ to mean that Condition 2 above is
satisfied, and
$\\{\psi_{1}^{\prime},\psi_{2}^{\prime},X\mid(\psi_{1}^{\prime},\psi_{2}^{\prime})\in
S\\}$ is part of a cycle in $(\Phi,\xrightarrow{X}\cup S)$. We can similarly
define $T\xrightarrow{g}S$ and $\emptyset\xrightarrow{g}S$ by not requiring
that $X$ is part of the path.

We write $\psi_{1}\xrightarrow{g,X}S,\psi_{2}$ to mean that

  1. (1)

$\psi_{1},\psi_{2}\in\Phi$, $(in,top)\in\ell(\psi_{1})$,
$(out,bot)\in\ell(\psi_{2})$,

  2. (2)

for each $(\psi_{1}^{\prime},\psi_{2}^{\prime})\in S$,
$\psi_{1}^{\prime},\psi_{2}^{\prime}\in\Phi$,
$(out,bot)\in\ell(\psi_{1}^{\prime})$, $(in,bot)\in\ell(\psi_{2}^{\prime})$,
and

  3. (3)

$\\{\psi_{1}^{\prime},\psi_{2}^{\prime},X\mid(\psi_{1}^{\prime},\psi_{2}^{\prime})\in
S\\}$ are on a path from $\psi_{1}$ to $\psi_{2}$ in
$(\Phi,\xrightarrow{X}\cup\\{(\psi_{2},\psi_{1})\\}\cup S)$.

We can similarly define $\psi_{1}\xrightarrow{g}S,\psi_{2}$ by not requiring
that $X$ is part of path.

To describe that there are no $\xrightarrow{X}$-paths where $X$ appears
infinitely often, we first describe that _there exists_ some
$\xrightarrow{X}$-path where $X$ appears infinitely often. We do so, by
defining the following formulas, recursively on two parameters $\varpi$ and
$\varpi_{X}$, that are _partial permutations_ of
$\\{\emptyset\\}\cup\overline{\mathsf{sub}}(\varphi)^{2}$ or
$\overline{\mathsf{sub}}(\varphi)$. These permutations keep track of the path
from the root of the syntax tree of the constructed formula, to the current
subformula, allowing the construction to detect when to use a recursive call.
For $T\in\overline{\mathsf{sub}}(\varphi)^{2}$ or $T=\emptyset$:

$\displaystyle{\mathbf{finb}}^{X}(T,\varpi)$
$\displaystyle:=\begin{cases}\bigvee_{\emptyset\xrightarrow{g,X}\emptyset}g\lor\bigvee_{\emptyset\centernot{\xrightarrow{g,X}}\emptyset}(g\land{\mathbf{finb}}^{X}(\emptyset,\varepsilon,g))&\text{
if $T=\emptyset$}\\\ Z^{X}_{T}&\text{if $T$ appears in }\varpi\\\ \mu
Z_{T}^{X}.\bigvee_{\begin{subarray}{c}T\in g\\\
T\xrightarrow{g,X}\emptyset\end{subarray}}g\lor\bigvee_{\begin{subarray}{c}T\in
g\\\
T\centernot{\xrightarrow{g,X}}\emptyset\end{subarray}}(g\land{\mathbf{finb}}^{X}(T,\varpi,g)),&\text{
otherwise}\end{cases}$ $\displaystyle{\mathbf{finb}}(T,\varpi)$
$\displaystyle:=\begin{cases}Z_{T}&\text{ if $T$ appears in }\varpi\\\ \mu
Z_{T}.\bigvee_{\begin{subarray}{c}T\in g\\\
T\xrightarrow{g}\emptyset\end{subarray}}g\lor\bigvee_{\begin{subarray}{c}T\in
g\\\
T\centernot{\xrightarrow{g}}\emptyset\end{subarray}}(g\land{\mathbf{finb}}(T,\varpi,g)),&\text{
otherwise}\end{cases}$ $\displaystyle{\mathbf{finb}}^{X}(T,\varpi,g)$
$\displaystyle:=\bigvee_{\begin{subarray}{c}S\subseteq\Phi_{g}^{2}\\\
T\xrightarrow{g}S\end{subarray}}\bigvee_{s\in
S}\langle\alpha(s)\rangle{\mathbf{finb}}^{X}(nx(s),\varpi
T)\land\bigwedge_{s\in
S}\langle\alpha(s)\rangle{\mathbf{finb}}(nx(s),\varepsilon)$
$\displaystyle\qquad\qquad\lor\bigvee_{\begin{subarray}{c}S\subseteq\Phi_{g}^{2}\\\
T\xrightarrow{g,X}S\end{subarray}}\bigwedge_{s\in
S}\langle\alpha(s)\rangle{\mathbf{finb}}(nx(s),\varepsilon)$
$\displaystyle{\mathbf{finb}}(T,\varpi,g)$
$\displaystyle:=\bigvee_{\begin{subarray}{c}S\subseteq\Phi_{g}^{2}\\\
T\xrightarrow{g}S\end{subarray}}\bigwedge_{s\in
S}\langle\alpha(s)\rangle{\mathbf{finb}}(nx(s),\varpi T)$

######  Lemma 30.

For every $T,T^{\prime}\in\overline{\mathsf{sub}}(\varphi)^{2}$,

${\left\llbracket{\mathbf{finb}}^{X}(T,\varepsilon)\right\rrbracket}={\left\llbracket{\mathbf{finb}}^{X}(T,T^{\prime})[{\mathbf{finb}}^{X}(T^{\prime},\varepsilon)/Z^{X}_{T^{\prime}}]\right\rrbracket}={\left\llbracket{\mathbf{finb}}^{X}(T,T^{\prime}),\rho\left[Z^{X}_{T^{\prime}}\mapsto{\left\llbracket{\mathbf{finb}}^{X}(T^{\prime},\varepsilon)\right\rrbracket}\right]\right\rrbracket}.$

######  Proof 6.25.

Specifically, we prove the stronger statement, that for any partial
permutation $\varpi$ where $T^{\prime}$ does not appear,

${\left\llbracket{\mathbf{finb}}^{X}(T,\varpi),\rho\right\rrbracket}={\left\llbracket{\mathbf{finb}}^{X}(T,T^{\prime}\varpi)[{\mathbf{finb}}^{X}(T^{\prime},\varpi)/Z^{X}_{T^{\prime}}],\rho\right\rrbracket}$

and

${\left\llbracket{\mathbf{finb}}^{X}(T,T^{\prime}\varpi)[{\mathbf{finb}}^{X}(T^{\prime},\varpi)/Z^{X}_{T^{\prime}}],\rho\right\rrbracket}={\left\llbracket{\mathbf{finb}}^{X}(T,T^{\prime}\varpi),\rho\left[Z^{X}_{T^{\prime}}\mapsto{\left\llbracket{\mathbf{finb}}^{X}(T^{\prime},\varpi)\right\rrbracket}\right],\rho\right\rrbracket}.$

The second equality is a straightforward property of fixed-point operators. We
prove the first one by induction on ${\mathbf{finb}}^{X}(T,T^{\prime}\varpi)$.

If ${\mathbf{finb}}^{X}(T,T^{\prime}\varpi)=Z^{X}_{T}$,:

then $T$ appears in $T^{\prime}\varpi$. If $T=T^{\prime}$, then

${\mathbf{finb}}^{X}(T,\varpi)={\mathbf{finb}}^{X}(T^{\prime},\varpi)=Z^{X}_{T}[{\mathbf{finb}}^{X}(T^{\prime},\varpi)/Z^{X}_{T^{\prime}}]={\mathbf{finb}}^{X}(T,T^{\prime}\varpi)[{\mathbf{finb}}^{X}(T^{\prime},\varpi)/Z^{X}_{T^{\prime}}],$

yielding the required semantic equality. On the other hand, if $T\neq
T^{\prime}$, then $T$ appears in $\varpi$, and therefore
${\mathbf{finb}}^{X}(T,\varpi)={\mathbf{finb}}^{X}(T,T^{\prime}\varpi)[{\mathbf{finb}}^{X}(T^{\prime},\varpi)/Z^{X}_{T^{\prime}}]=Z^{X}_{T}$.

Otherwise, :

the inductive step is straightforward from the definition of the formulas.

######  Definition 6.26.

Let $X\in mV$, $\psi_{1},\psi_{2}\in\overline{\mathsf{sub}}(\varphi)$,
$f:b\xrightarrow{r}\mathcal{M},s$, and $\sigma\in\sigma(b)$. We write
$cyc((\psi_{1},\psi_{2}),\sigma)$ to denote that the following hold:

  1. (1)

$\sigma~{}\psi_{1},\sigma~{}\psi_{2}\in b$,

  2. (2)

$\sigma=\sigma^{\prime}.\alpha\langle\psi\rangle$ for some
$\sigma^{\prime},\alpha,\psi$,

  3. (3)

$\sigma^{\prime}~{}\psi_{1}^{\prime}\xrightarrow{X}\sigma~{}\psi_{1}$ for some
$\psi_{1}^{\prime}\in\overline{\mathsf{sub}}(\varphi)$,

  4. (4)

$\sigma~{}\psi_{2}\xrightarrow{X}\sigma^{\prime}~{}\psi_{2}^{\prime}$ for some
$\psi_{2}^{\prime}\in\overline{\mathsf{sub}}(\varphi)$, and

  5. (5)

there is a finite $\xrightarrow{X}$-path in $b$, from $\sigma~{}\psi_{1}$ to
$\sigma~{}\psi_{2}$ (_resp._ , where $X$ appears), which only goes through
prefixes that extend $\sigma$.

We write $cyc_{X}((\psi_{1},\psi_{2}),\sigma)$ to denote that the same
conditions as for $cyc((\psi_{1},\psi_{2}),\sigma)$ are satisfied, with the
addition that $X$ appears on the finite $\xrightarrow{X}$-path from
$\sigma~{}\psi_{1}$ to $\sigma~{}\psi_{2}$.

######  Lemma 31.

Let $X\in mV$, $\psi_{1},\psi_{2}\in\overline{\mathsf{sub}}(\varphi)$,
$f:b\xrightarrow{r}\mathcal{M},s$, and $\sigma\in\sigma(b)$.

  1. (1)

$\mathcal{M},f(\sigma)\models{\mathbf{finb}}((\psi_{1},\psi_{2}),\varepsilon)$
if and only if $cyc_{X}((\psi_{1},\psi_{2}),\sigma)$, and

  2. (2)

$\mathcal{M},f(\sigma)\models{\mathbf{finb}}^{X}((\psi_{1},\psi_{2}),\varepsilon)$
if and only if $cyc((\psi_{1},\psi_{2}),\sigma)$.

######  Proof 6.27.

We only prove the second biimplication of the lemma, assuming the first one,
which can be shown following similar lines. We first prove that
$\mathcal{M},f(\sigma)\models{\mathbf{finb}}^{X}((\psi_{1},\psi_{2}),\varepsilon)$
implies $cyc_{X}((\psi_{1},\psi_{2}),\sigma)$.

For each $T$, let
$C_{Z_{T}^{X}}=\\{f(\sigma^{\prime})\mid\sigma^{\prime}\in\sigma(b)\text{ and
}cyc_{X}(T,\sigma^{\prime})\\}$. Let $T=(\psi_{1},\psi_{2})$. To prove the
implication, we proceed to prove the more general statement that $\neg
cyc_{X}(T,\sigma)$ implies that
$\mathcal{M},f(\sigma)\not\models_{\rho}{\mathbf{finb}}^{X}(T,\varpi)$ for
every $\varpi\in\overline{\mathsf{sub}}(\varphi)^{2}!$ and environment $\rho$,
such that $\rho(Z_{T^{\prime}}^{X})=C_{Z_{T^{\prime}}^{X}}$ for each
$Z_{T^{\prime}}^{X}$. We assume that $\neg cyc_{X}(T,\sigma)$ and proceed by
induction on the structure of ${\mathbf{finb}}^{X}(T,\varpi)$.

If $T$ appears in $\varpi$,:

or equivalently, ${\mathbf{finb}}^{X}(T,\varpi)=Z_{T}^{X}$, by the definition
of $\rho$, $f(\sigma)\notin\rho(Z^{X}_{T})$, so
$\mathcal{M},f(\sigma)\not\models_{\rho}{\mathbf{finb}}^{X}(T,\varpi)$.

We now assume that $T$ does not appear in $\varpi$.:

If one of the Conditions 1, 2, 3, and 4 for $cyc_{X}(T,\sigma)$ does not hold,
then it is evident from the definitions of $T\xrightarrow{g}S$,
$T\xrightarrow{g,X}S$, and $T\xrightarrow{g,X}\emptyset$ that
$\mathcal{M},f(\sigma)\not\models{\mathbf{finb}}^{X}(T,\varpi)$, and we are
done. We now assume that Conditions 1 to 4 hold, but there is no finite
$\xrightarrow{X}$-path in $b$, from $\sigma~{}\psi_{1}$ to $\sigma~{}\psi_{2}$
where $X$ appears. From the fixed-point semantics of Table 1, it suffices to
prove two statements:

  1. (1):

for every $\sigma^{\prime}\in\sigma(b)$, if
$\mathcal{M},f(\sigma^{\prime})\models\bigvee_{\begin{subarray}{c}T\in g\\\
T\xrightarrow{g,X}\emptyset\end{subarray}}g\lor\bigvee_{\begin{subarray}{c}T\in
g\\\
T\centernot{\xrightarrow{g,X}}\emptyset\end{subarray}}(g\land{\mathbf{finb}}^{X}(T,\varpi,g))$,
then $f(\sigma^{\prime})\in C_{Z_{T}^{X}}$; and

  2. (2):

$f(\sigma)\notin C_{Z_{T}^{X}}$.

The second statement is immediate from our assumption that $\neg
cyc_{X}(T,\sigma)$. We now prove the first statement. Clearly, if
$\mathcal{M},f(\sigma^{\prime})\models\bigvee_{\begin{subarray}{c}T\in g\\\
T\xrightarrow{g,X}\emptyset\end{subarray}}g$, we have
$cyc_{X}(T,\sigma^{\prime})$. Otherwise, we have that there is some $g\in
G^{t}$, such that $\mathcal{M},f(\sigma^{\prime})\models g$ and
$\mathcal{M},f(\sigma^{\prime})\models{\mathbf{finb}}^{X}(T,\varpi,g)$.
Therefore, there is some $S\subseteq\overline{\mathsf{sub}}(\varphi)^{2}$,
such that either

$T\xrightarrow{g,X}S$: