Completing the Picture: Complexity of Graded Modal Logics with Converse

TL;DR

This paper classifies the complexity of graded modal logic with converse modalities across various frame classes, revealing increased complexity over Euclidean frames and decidability over transitive frames without graded converse modalities.

Contribution

It completes the complexity classification for graded modal logic with converse modalities, including Euclidean and transitive frames, and confirms decidability in a specific variation.

Findings

NExpTime-completeness over Euclidean frames

Decidability over transitive frames without graded converse modalities

Language with graded converse modalities is undecidable

Abstract

A complete classification of the complexity of the local and global satisfiability problems for graded modal language over traditional classes of frames have already been established. By "traditional" classes of frames, we mean those characterized by any positive combination of reflexivity, seriality, symmetry, transitivity, and the Euclidean property. In this paper, we fill the gaps remaining in an analogous classification of the graded modal language with graded converse modalities. In particular, we show its NExpTime-completeness over the class of Euclidean frames, demonstrating this way that over this class the considered language is harder than the language without graded modalities or without converse modalities. We also consider its variation disallowing graded converse modalities, but still admitting basic converse modalities. Our most important result for this variation is confirming an earlier conjecture that it is decidable over transitive frames. This contrasts with the undecidability of the language with graded converse modalities.

Equations

$$\Diamond_{\leq n}\varphi:=\neg\Diamond_{\geq n+1}\varphi,\;\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{$-$}}{O}{c}{F}{F}{L}}_{\leq n}\varphi:=\neg\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{$-$}}{O}{c}{F}{F}{L}}_{\geq n+1}\varphi,\;\Box\varphi:=\neg\Diamond\neg\varphi,\;\text{and}\;\ensurestackMath{\stackengine{.5pt}{\Box}{\scalebox{0.75}[1.0]{$-$}}{O}{c}{F}{F}{L}}\varphi:=\neg\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{$-$}}{O}{c}{F}{F}{L}}\neg\varphi.$$

$$\begin{array}[]{cl@{\quad}l}(\mbox{D})&\mbox{seriality}&\forall x\exists y\,(xRy)\\ (\mbox{T})&\mbox{reflexivity}&\forall x\,(xRx)\\ (\mbox{B})&\mbox{symmetry}&\forall xy\,(xRy\Rightarrow yRx)\\ (\mbox{4})&\mbox{transitivity}&\forall xyz\,(xRy\land yRz\Rightarrow xRz)\\ (\mbox{5})&\mbox{Euclideanness}&\forall xyz\,(xRy\land xRz\Rightarrow yRz)\\ \end{array}$$

$${\mathbf{st}}_x(p)=p(x)\text{ for all p∈Π}$$

$${\mathbf{st}}_x(\phi \wedge \psi )={\mathbf{st}}_x(\phi )\wedge {\mathbf{st}}_x(\psi )\text{ similarly for ¬, ∨, etc.}$$

$${\mathbf{st}}_x({◊}_{\ge n}\phi )={\exists }_{\ge n}.y(R(x,y)\wedge {\mathbf{st}}_y(\phi ))$$

$$\displaystyle\mathbf{st}_{x}(\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{$-$}}{O}{c}{F}{F}{L}}_{\geq n}\varphi)=\exists_{\geq n}.y(R(y,x)\wedge\mathbf{st}_{y}(\varphi))$$

$${\mathbf{st}}_x(\phi )\wedge \forall x\forall y.\left(\neg lantern(x)\wedge \neg lantern(y)\to R(x,y)\right)\wedge \left(lantern(y)\to \neg R(x,y)\right).$$

$$\mathfrak{B},w_0\models \phi \text{ if and only if }{\mathfrak{B}}^{+}\models {\phi }_{\mathbf{tr}}[w_0/x]\text{ for every world w0∈B}.$$

$${\phi }_{\text{torus}}\stackrel{\text{def}}{=}{\phi }_{\text{firstCell}}\wedge \mathbf{U}\left({\phi }_{\text{partition}}\wedge {\phi }_{\text{chessboard}}\wedge {\phi }_{\text{torusSize}}\wedge {\phi }_{\text{succ}}\right)$$

$${\phi }_{\text{firstCell}}\stackrel{\text{def}}{=}inner\wedge wht\wedge \underset{i=0}{\overset{n-1}{\bigwedge }}\left(\neg v_i\wedge \neg h_i\right)$$

$$\displaystyle\varphi_{\text{partition}}\stackrel{{\scriptstyle\text{def}}}{{=}}(\mathit{lantern}\leftrightarrow\neg\mathit{inner})\wedge(\mathit{lantern}\leftrightarrow\neg\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{$-$}}{O}{c}{F}{F}{L}}\top)$$

$${\phi }_{\text{chessboard}}\stackrel{\text{def}}{=}(wht\leftrightarrow \neg blk)\wedge (wht\leftrightarrow (v_0\leftrightarrow h_0))$$

$${\phi }_{\text{torusSize}}\stackrel{\text{def}}{=}inner\to {◊}_{=2^n\cdot 2^n}\top$$

$$\varphi_{\text{succ}}\stackrel{{\scriptstyle\text{def}}}{{=}}(\mathit{lantern}\rightarrow\bigvee_{\heartsuit\in\{\mathit{vbw},\mathit{hbw},\mathit{vwb},\mathit{hwb}\}}(\heartsuit\wedge\varphi_{\heartsuit}))\wedge\\ (\mathit{inner}\rightarrow\bigwedge_{\heartsuit\in\{\mathit{vbw},\mathit{hbw},\mathit{vwb},\mathit{hwb}\}}\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{$-$}}{O}{c}{F}{F}{L}}(\mathit{lantern}\wedge\varphi_{\heartsuit}))$$

$${\phi }_{vbw}\stackrel{\text{def}}{=}{\phi }_{\text{pseudoUniqueness}}\wedge {\phi }_{\text{equalH}}\wedge {\phi }_{V_w=V_b{\oplus }_{2^n}1}.$$

$${\phi }_{\text{pseudoUniqueness}}\stackrel{\text{def}}{=}\underset{c\in \{wht,blk\}}{\bigwedge }\underset{p\in \{v,h\}}{\bigwedge }\underset{i=0}{\overset{n-1}{\bigwedge }}◊(c\wedge p_i)\to \square (c\wedge p_i)$$

$${\phi }_{\text{equalH}}\stackrel{\text{def}}{=}\underset{i=0}{\overset{n-1}{\bigwedge }}◊(blk\wedge h_i)\leftrightarrow ◊(wht\wedge h_i)$$

$${\phi }_{V_w=V_b{\oplus }_{2^n}1}\stackrel{\text{def}}{=}(◊(blk\wedge \underset{i=0}{\overset{n-1}{\bigwedge }}{v}_i)\to ◊(wht\wedge \underset{i=0}{\overset{n-1}{\bigwedge }}\neg v_i))\wedge$$

$$\underset{i=0}{\overset{n-1}{\bigvee }}(◊(blk\wedge \neg v_i\wedge \underset{j=0}{\overset{i-1}{\bigwedge }}{v}_j)\wedge ◊(wht\wedge v_i\wedge \underset{j=0}{\overset{i-1}{\bigwedge }}\neg v_j)\wedge \underset{j=i+1}{\overset{n-1}{\bigwedge }}◊(blk\wedge v_j)\leftrightarrow ◊(wht\wedge v_j))$$

$${\phi }_{hbw}$$

$${\phi }_{vwb}$$

$${\phi }_{hwb}$$

$${\phi }_{\text{tiling}}\stackrel{\text{def}}{=}\mathbf{U}({\phi }_{\text{tile}}\wedge {\phi }_{\text{initCond}}\wedge {\phi }_{\text{tilingRules}})$$

$${\phi }_{\text{tile}}\stackrel{\text{def}}{=}inner\to (\underset{t\in \mathcal{T}}{\bigvee }t)\wedge \underset{t,t^{\prime }\in \mathcal{T},t\ne t^{\prime }}{\bigwedge }(\neg t\vee \neg t^{\prime })$$

$${\phi }_{\text{initCond}}\stackrel{\text{def}}{=}\underset{i=0}{\overset{n-1}{\bigwedge }}(inner\wedge H=0\wedge V=i)\to t_i$$

$${\phi }_{\text{tilingRules}}\stackrel{\text{def}}{=}$$

$$(lantern\wedge vwb\to \underset{(t^{\prime },t)\in \mathcal{V}}{\bigvee }(◊(wht\wedge t)\wedge ◊(blk\wedge t^{\prime })))\wedge$$

$$(lantern\wedge hbw\to \underset{(t,t^{\prime })\in \mathcal{H}}{\bigvee }(◊(blk\wedge t)\wedge ◊(wht\wedge t^{\prime })))\wedge$$

$$(lantern\wedge hwb\to \underset{(t^{\prime },t)\in \mathcal{H}}{\bigvee }(◊(wht\wedge t)\wedge ◊(blk\wedge t^{\prime })))$$

$$\mathbf{tr}(p)=p(x)\text{ for all p∈Π }$$

$$\mathbf{tr}(\phi \wedge \psi )=\mathbf{tr}(\phi )\wedge \mathbf{tr}(\psi )\text{ similarly for ¬, ∨, etc.}$$

$$\mathbf{tr}({◊}_{\ge n}\phi )={\exists }_{\ge n}.x(\neg lantern(x)\wedge \mathbf{tr}(\phi ))$$

$$\mathbf{tr}({◊}_{\le n}\phi )={\exists }_{\le n}.x(\neg lantern(x)\wedge \mathbf{tr}(\phi ))$$

$$\displaystyle\mathbf{tr}(\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{$-$}}{O}{c}{F}{F}{L}}_{\geq n}\varphi)=\neg\mathit{lantern}(x)\wedge\exists_{\geq n}.x(\mathbf{tr}(\varphi))$$

$$\displaystyle\mathbf{tr}(\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{$-$}}{O}{c}{F}{F}{L}}_{\leq n}\varphi)=\mathit{lantern}(x)\vee\exists_{\leq n}.x(\mathbf{tr}(\varphi))$$

$$\mathfrak{B},w_0\models \phi \text{ if and only if }{\mathfrak{B}}^{+}\models \mathbf{tr}(\phi )[w_0/x]\text{ for every world w0}.$$

$$\eta \wedge \underset{1\le i\le l}{\bigwedge }(p_i$$

$$\displaystyle\bigwedge_{1\leq i\leq l^{\prime}}(p^{\prime}_{i}\rightarrow\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{$-$}}{O}{c}{F}{F}{L}}\pi^{\prime}_{i})\wedge\bigwedge_{1\leq i\leq m^{\prime}}(q^{\prime}_{i}\rightarrow\boxminus\neg\chi^{\prime}_{i})$$

Full text

Under consideration in Theory and Practice of Logic Programming (TPLP).

1 Introduction

For many years modal logic has been an active topic in many academic disciplines, including philosophy, mathematics, linguistics, and computer science. Regarding applications in computer science, e.g., in knowledge representation or verification, some important variations are those involving graded and converse modalities. In this paper, we investigate their computational complexity.

By a modal logic we will mean a pair $(\mathcal{L},\mathcal{F})$, represented usually as $\mathcal{F}(\mathcal{L}^{*})$, where $\mathcal{L}$ is a modal language, $\mathcal{F}$ is a class of frames, and $\mathcal{L}^{*}$ is a short symbolic representation of $\mathcal{L}$ (see the next paragraph), characterizing the modalities of $\mathcal{L}$. For example $\mbox{\rm K4}(\Diamond_{\geq})$ will denote the graded modal logic of transitive frames.

While we are mostly interested in languages with graded and converse modalities, to set the scene we need to mention languages without them. Overall, the following five languages are relevant: the basic one-way modal language ($\mathcal{L}^{*}=\Diamond$) containing only one, forward, modality $\Diamond$; graded one-way modal language ($\mathcal{L}^{*}=\Diamond_{\geq}$) extending the previous one by graded forward modalities, $\Diamond_{\geq n}$, for all $n\in{\mathbb{N}}$; two-way modal language (\mathcal{L}^{*}=\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) containing basic forward modality and the converse modality \ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}; graded two-way modal language (\mathcal{L}^{*}=\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) containing the forward modality, the converse modality and their graded versions $\Diamond_{\geq n}$, \ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq n}, for all $n\in N$; and, additionally, a restriction of the latter without graded converse modalities, but with basic converse modality (\mathcal{L}^{*}=\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}).

The meaning of graded modalities is natural: $\Diamond_{\geq n}\varphi$ means ”$\varphi$ is true at no fewer than $n$ successors of the current world”, and \ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}\varphi means ”$\varphi$ is true at no fewer than $n$ predecessors of the current world”. We also recall that $\Diamond\varphi$ means ”$\varphi$ is true at some successor of the current world” and \ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}\varphi — ”$\varphi$ is true at some predecessor of the current world”. Thus, e.g., $\Diamond$ is equivalent to $\Diamond_{\geq 1}$.

Our aim is to classify the complexity of the local (“in a world”) and global (“in all worlds”) satisfiability problems for all the logics obtained by combining any of the above languages with any class of frames from the so-called modal cube, that is a class of frames characterized by any positive combination of the axioms of reflexivity (T), seriality (D), symmetry (B), transitivity (4), and the Euclidean property (5).

See Fig. 1 for a visualization of the modal cube. Nodes of the depicted graph correspond to classes of frames and are labelled by letters denoting the above-mentioned properties, with S used in S4 and S5 for some historical reasons to denote reflexivity, and K denoting the class of all frames. If there is a path from a class $X$ to a class $Y$ then it means that any class from $Y$ also belongs to $X$ (as all the axioms of $X$ are also present in $Y$). Note that the modal cube contains only $15$ classes, since some different combinations of the relevant axioms lead to identical classes, e.g., reflexivity implies seriality, symmetry and transitivity imply Euclideanness, and so on.

A lot of work has been already done. The cases of basic one-way language and graded one-way language are completely understood. See Fig. 1. The results for the former can be established using some standard techniques, see, e.g., [Blackburn et al. (2001)] and the classical paper [Ladner (1977)]. The local satisfiability of the latter is systematically analysed in [Kazakov and Pratt-Hartmann (2009)], with complexities turning out to lie between NP and NExpTime. As for its global satisfiability, some of the results follow from [Kazakov and Pratt-Hartmann (2009)], some are given in [Zolin (2017)], and the other can be easily obtained using again some standard techniques.

In the case of non-graded two-way modal language, over most relevant classes of frames, tight complexity bounds for local and global satisfiability are also known. The notable exceptions are global satisfiability problems of the logics of transitive frames, K4(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), S4(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), D4(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), which are known to be in ExpTime (due to a result in [Demri and de Nivelle (2005)] or due to a translation to description logic $SI$, whose satisfiability is in ExpTime [Tobies (2001b)]). However, according to the survey part of [Zolin (2017)], the corresponding lower bounds are missing. In the literature we were also not able find a tight lower bound for the logics of Euclidean frames, K5(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), D5(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}). We provide both missing bounds in Section 5, obtaining them by reductions from the acceptance problem for polynomially space bounded alternating Turing machines.111As explained to the first author by Emil Jeřábek, the latter bound can be alternatively proved by a reduction from TB, whose ExpTime-hardness follows from [Chen and Lin (1994)]. See the left part of Fig. 2 for a complete complexity map in this case.

Let us now turn our attention to the most expressive two-way graded modal language with both graded forward and graded converse modalities (the right part of Fig. 2). Its local and global satisfiability problems over the class of all frames (K) are known to be, resp., PSpace-complete and ExpTime-complete (see the survey part of [Zolin (2017)] and references therein). In Section 2.2, we explain how to obtain these bounds, as well as the same bounds in all cases involving neither transitivity nor Euclideanness. For the ExpTime-bound, we employ the so-called standard translation. Over K4, D4 and S4 the logics turn out to be undecidable [Zolin (2017)]. We remark that these are the only undecidable members of the whole family of logics considered in this paper. What remains are the classes of frames involving the Euclidean property. We solve them in Section 3. We prove that the logics K5(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) and D5(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) are locally and globally NExpTime-complete. Interestingly, this is a higher complexity than the ExpTime-complexity of the language without graded modalities [Demri and de Nivelle (2005)] and NP-complexity of the language without converse [Kazakov and Pratt-Hartmann (2009)] over the same classes of frames. We also show that, when, additionally, transitivity is required, that is, for the logics K45(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) and D45(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}), the complexity drops down to NP.

Finally, we consider the above-mentioned intermediate language (\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) in which we can count the successors, we have the basic converse modality, but we cannot count the predecessors. Our main result here, presented in Section 4, is demonstrating the (local and global) finite model property for the logics of transitive frames K4, D4 and S4: whenever a formula is (locally or, resp., globally) satisfiable it is (locally, resp. globally) satisfiable over a finite frame. This implies the decidability of the (local and global) satisfiability problem (as well as the finite satisfiability problem, in which the attention is restricted to finite frames) for these logics and thus solve an open problem posed in [Zolin (2017)]. An analogous problem was formulated also in the richer setting of description logics [Kazakov et al. (2007)], [Gutiérrez-Basulto et al. (2017)], where the corresponding logic is called $\mathcal{SIQ}^{-}$. That problem only recently was also positively solved [Gogacz et al. (2019)]. The results from [Gogacz et al. (2019)] (which we will discuss in more details in a moment) allow us to derive the precise 2-ExpTime-complexity bounds for the logics \mbox{\rm K4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), \mbox{\rm D4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) and \mbox{\rm S4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}). The logics of the remaining classes of frames retain their complexities from the graded two-way case, so the picture is as in the right part of Fig. 2, but the word ”Undecidable” should be replaced by ”2-ExpTime”.

Due to a large number of papers in which the complexity bounds from Fig. 1 and Fig. 2 are scattered, we have not referenced all of them in this introduction. Readers wishing to find an appropriate reference are recommended to use an online tool prepared by the first author (bartoszjanbednarczyk.github.io/mlnavigator).

Related formalisms. Graded modalities are examples of counting quantifiers which are present in various formalisms. First of all, counting quantifiers were introduced for first-order logic: $\exists^{\geq n}x\varphi$ means: ”at least $n$ elements $x$ satisfy $\varphi$”. The satisfiability problem for some fragments of first-order logic with counting quantifiers was shown to be decidable. In particular, the two-variable fragment is NExpTime-complete [Pratt-Hartmann (2005)], the two-variable guarded fragment is ExpTime-complete [Pratt-Hartmann (2007)], and the one-variable fragment is NP-complete [Pratt-Hartmann (2008)]. We will employ the second of those results in our paper.

Counting quantifiers are also present, in the form of the so-called number restrictions, in some description logics, DLs. As some standard DLs embed modal logics (c.f. a result in [Baader et al. (2017), Section 2.6.2]), results on DLs with number restrictions may be used to infer upper bounds on the complexity of some graded modal logics.

The description logic which is particularly interesting from our point of view is the already mentioned logic $\mathcal{SIQ}^{-}$. Syntactically, it can be seen as a multi-modal logic, that is a logic whose frames interpret not just one but many accessibility relations, with different modalities associated with these relations. In the case of $\mathcal{SIQ}^{-}$ each of the accessibility relations can be independently required to be transitive or not. Recently the knowledge base satisfiability problem for this logic was shown decidable and 2-ExpTime-complete [Gogacz et al. (2019)]. As we said, from this result the decidability and 2-ExpTime complexity of both local and global satisfiability of \mbox{\rm K4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), \mbox{\rm S4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) and \mbox{\rm D4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) can be inferred. Nevertheless, our proof of the finite model property for these logics remains valuable as in [Gogacz et al. (2019)] the decidability of the finite model reasoning for $\mathcal{SIQ}^{-}$ is left open (with the exception of the case in which there is only one accessibility relation and this relation is transitive; in this case, however, our finite model construction is used and cross-referred there).

In this context it is worth noting that the logic K(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) (with the accessibility relation not necessarily being transitive) and the logic K4(\Diamond^{1}_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}^{1},\Diamond^{2}_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}^{2}) (the bi-modal variant of \mbox{\rm K4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) with two independent transitive accessibility relations) do not have the global finite model property. Both these logics are contained in $\mathcal{SIQ}^{-}$. An example K(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) formula which is globally satisfiable (e.g., over an infinite binary tree with reversed edges) but has no finite models is \ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}p\wedge\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}\neg p\wedge\Diamond_{\leq 1}\top. This example can be easily adapted to K4(\Diamond^{1}_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}^{1},\Diamond^{2}_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}^{2}). On the other hand, K(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) does have the local finite model property, as it is a fragment of the description logic $\mathcal{ALCIQ}$, whose local finite model property was shown in [Tobies (2001a)]. The status of the local finite model property for the multi-modal variants of K4(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) is open.

Plan of the paper. In Section 2 we formally define the relevant modal languages and their semantics, recall the so called standard translation and use it to derive some initial results. In Sections 3 and 4 we investigate the classes of Euclidean frames and, respectively, transitive frames. Finally, in Section 5 we provide two lower bounds filling the gaps in the classification of the complexity of non-graded languages.

This work is an extended version of our conference paper [Bednarczyk et al. (2019)].

2 Preliminaries

2.1 Languages, Kripke structures and satisfiability

Let us fix a countably infinite set $\Pi$ of propositional variables. The language of graded two-way modal logic is defined inductively as the smallest set of formulas containing $\Pi$, closed under Boolean connectives and, for any formula $\varphi$, containing $\Diamond_{\geq n}\varphi$ and \ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq n}\varphi, for all $n\in{\mathbb{N}}$. For a given formula $\varphi$, we denote its length with $|\varphi|$, and measure it as the number of symbols required to write $\varphi$, with numbers in subscripts ${}_{\geq}n$ encoded in binary (i.e., encoding a number $n$ requires $\log{n}$ bits rather than $n$ bits).

The basic modality $\Diamond$ can be defined in terms of graded modalities: $\Diamond\varphi:=\Diamond_{\geq 1}\varphi$. Analogously, for the converse modality: \ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}:=\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq 1}. Keeping this in mind, we may treat all languages mentioned in the introduction as fragments of the above-defined graded two-way modal language. We remark that we may also introduce other modalities, e.g.

[TABLE]

The semantics is defined with respect to Kripke structures, that is, structures over the relational signature composed of unary predicates $\Pi$ and with a binary predicate $R$. Such structures are represented as triples ${\mathfrak{A}}=\langle W,R,V\rangle$, where $W$ is the universe, $R$ is a binary accessibility relation on $W$, and $V$ is a function $V:\Pi\rightarrow\mathcal{P}(W)$ called valuation. Elements from the set $W$ are often called worlds.

The satisfaction relation $\models$ is defined inductively as follows:

• •

${\mathfrak{A}},w\models p$ iff $w\in V(p)$, for all $p\in\Pi$,

• •

${\mathfrak{A}},w\models\neg\varphi$ iff ${\mathfrak{A}},w\not\models\varphi$ and similarly for the other Boolean connectives,

• •

${\mathfrak{A}},w\models\Diamond_{\geq n}\varphi$ iff there are $\geq n$ worlds $v\in W$ such that $\langle w,v\rangle\in R$ and ${\mathfrak{A}},v\models\varphi$

• •

{\mathfrak{A}},w\models\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq n}\varphi iff there are $\geq n$ worlds $v\in W$ such that $\langle v,w\rangle\in R$ and ${\mathfrak{A}},v\models\varphi$.

For a given Kripke structure ${\mathfrak{A}}=\langle W,R,V\rangle$ we call the pair $\langle W,R\rangle$ its frame. For a class of frames $\mathcal{F}$, we define the local (global) satisfiability problem of a modal language $\mathcal{L}$ over $\mathcal{F}$ (or equivalently for a modal logic $\mathcal{F}(\mathcal{L}^{*})$) as follows: given a formula $\varphi$ from a language $\mathcal{L}$, verify whether $\varphi$ is satisfied at some world (all worlds) $w$ of some structure ${\mathfrak{A}}$ whose frame belongs to $\mathcal{F}$.

We announced in the introduction that we are interested in classes of frames characterized by any positive combination of the axioms of reflexivity (T), seriality (D), symmetry (B), transitivity (4), and the Euclidean property (5), recalled below.

[TABLE]

We say that a modal logic $\mathcal{F}(\mathcal{L}^{*})$ has the finite local (global) model property if any formula of $\mathcal{L}$ which is satisfied in some world (all worlds) of some structure from $\mathcal{F}$ is also satisfied in some world (all worlds) of a finite structure from $\mathcal{F}$.

2.2 Standard translations

Modal logic can be seen as a fragment of first-order logic via the so-called standard translation (see e.g., [Blackburn et al. (2001)]). Here we present its variation tailored for graded and converse modalities and discuss how it can be used to establish exact complexity bounds for some of graded two-way modal logics.

In the forthcoming definition, we define a function $\mathbf{st}_{v}$ for $v\in\{x,y\}$, which takes an input two-way modal logic formula $\varphi$ and returns an equisatisfiable first-order formula. Definitions of $\mathbf{st}_{x}$ and $\mathbf{st}_{y}$ are symmetric, hence we present the definition of $\mathbf{st}_{x}$ only.

[TABLE]

Translated formulas lie in the two-variable guarded fragment of first-order logic extended with counting quantifiers $\mathrm{GC}^{2}$. Observe that a modal formula $\varphi\in\mathcal{L}$ is (finitely) locally-satisfiable iff a formula $\exists{x}\;\mathbf{st}_{x}(\varphi)\in\mathrm{GC}^{2}$ is (finitely) satisfiable and that $\varphi$ is (finitely) globally-satisfiable iff $\forall{x}\;\mathbf{st}_{x}(\varphi)\in\mathrm{GC}^{2}$ is (finitely) satisfiable. Since definitions of symmetry, seriality and reflexivity, as recalled in the previous section, are $\mathrm{GC}^{2}$ formulas, the standard translation can be used to provide a generic upper bound for the logics \mathcal{F}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) over all classes of frames $\mathcal{F}$ involving neither transitivity nor Euclideanness. From the fact that the global satisfiability problem is ExpTime–hard even for the basic modal language $\mathcal{F}(\Diamond)$ [Blackburn and van Benthem (2007)] and from ExpTime-completeness of $\mathrm{GC}^{2}$ [Pratt-Hartmann (2007)], we conclude the following theorem:

Theorem 1

The global satisfiability problem for \mathcal{F}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) where $\mathcal{F}$ is any class of frames from the modal cube involving neither transitivity nor Euclideanness, is ExpTime-complete.

For the local satisfiability problem, its complexity decreases to PSpace. For two-way graded language over K, D and T, we can simply adapt an existing tableaux algorithm by Tobies [Tobies (2001b)], which yields a tight PSpace bound. Moreover, if a class of frames is symmetric, then forward and converse modalities coincide and thus we may simply apply the result on graded one-way languages from [Kazakov and Pratt-Hartmann (2009)]. The PSpace lower bounds for the above-mentioned logics are inherited from the basic modal logic K [Ladner (1977)] and hold even in the case of their propositional-variable-free fragment[Chagrov and Rybakov (2002)]. Thus we can conclude the following.

Theorem 2

The local satisfiability problem for \mathcal{F}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}), where $\mathcal{F}$ is any class of frames from the modal cube involving neither transitivity nor Euclideanness is PSpace-complete.

3 Euclidean frames: counting successors and predecessors

This section is dedicated to modal languages over the classes of frames satisfying Euclideanness. We demonstrate an exponential gap (NExpTime versus NP) in the complexities of modal logics over Euclidean frames (K5 and D5) and modal logics over transitive Euclidean frames (K45 and D45).

The two remaining Euclidean logics of our interest, namely KB45 and S5, whose frames are additionally symmetric, may be seen as one-way logics (as \ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq} can be always replaced by $\Diamond_{\geq}$). Hence, their NP upper bounds follows from previous works on one-way MLs [Kazakov and Pratt-Hartmann (2009)]. The lower bound is inherited from the Boolean satisfiability problem [Cook (1971)]. Thus:

Theorem 3** (Consequence of [[Kazakov and

Pratt-Hartmann (2009)](#bib.bib11)].)**

The local satisfiability and the global satisfiability problems for modal logics \mbox{\rm KB45}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) and \mbox{\rm S5}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) are NP-complete.

3.1 The shape of Euclidean frames

We start by describing the shape of frames under consideration. Let ${\mathfrak{A}}$ be a Euclidean structure, i.e., a Kripke structure ${\mathfrak{A}}=\langle W,R,V\rangle$ whose accessibility relation $R$ satisfies the Euclidean property.

A world $w\in W$ is called a lantern, if $\langle w^{\prime},w\rangle\not\in R$ holds for every $w^{\prime}\in W$. The set of all lanterns in ${\mathfrak{A}}$ is denoted with $L_{{\mathfrak{A}}}$. We say that lantern $l\in W$ illuminates a world $w\in W$, if $\langle l,w\rangle\in R$ holds. The previous definition is lifted to the sets of worlds in an obvious way: a lantern $l$ illuminates a set of worlds $I\subseteq W$ if $l$ illuminates every world $w$ from $I$.

We say that two worlds $w_{1},w_{2}\in W$ are $R$-equivalent (or simply equivalent if $R$ is known from the context), if both $\langle w_{1},w_{2}\rangle\in R$ and $\langle w_{2},w_{1}\rangle\in R$ holds. The $R$-clique for a world $w_{1}$ in a structure ${\mathfrak{A}}$ is the set $Q_{{\mathfrak{A}}}(w_{1})\subseteq W$ consisting of $w_{1}$ together with all of its $R$-equivalent worlds. With $Q_{{\mathfrak{A}}}$ we denote the set $W\setminus L_{{\mathfrak{A}}}$ of inner (i.e. non-lantern) worlds. See Fig. 3 for a drawing of an example Euclidean structure.

It is easy to observe that for any world $w_{1}\in W$, all members of the clique $Q_{{\mathfrak{A}}}(w_{1})$ are $R$-equivalent. This justifies why we have chosen the term “clique” to name such sets.

Observation 1

Any distinct worlds $w^{\prime},w^{\prime\prime}$ from the $R$-clique $Q_{{\mathfrak{A}}}(w)$ of $w$ are $R$-equivalent.

Proof 3.4**.**

From the definition of $R$-equivalence, we know that both $\langle w,w^{\prime}\rangle\in R$ and $\langle w,w^{\prime\prime}\rangle\in R$ hold. Since the relation $R$ satisfies the Euclidean property we infer that $\langle w^{\prime},w^{\prime\prime}\rangle\in R$ holds and $\langle w^{\prime\prime},w^{\prime}\rangle\in R$ holds, which implies $R$-equivalence of $w$ and $w^{\prime}$.

An immediate conclusion from the above observation is that the equality $Q_{{\mathfrak{A}}}(w)=Q_{{\mathfrak{A}}}(w_{1})$ holds for any world $w\in Q_{{\mathfrak{A}}}(w_{1})$. Thus we will say that $Q$ is an $R$-clique in ${\mathfrak{A}}$ if the equality $Q=Q_{{\mathfrak{A}}}(w_{1})$ holds for some (equivalently: for any) world $w_{1}\in Q$.

As usual in modal logics, we can restrict our attention to $R$-connected models, that is those models ${\mathfrak{A}}=\langle W,R,V\rangle$ for which $\langle W,R\cup R^{-1}\rangle$ is a connected graph. The following lemma describes the shape of Euclidean structures under consideration. It is very similar to Lemma 2 in [Kazakov and Pratt-Hartmann (2009)].

Lemma 3.5**.**

If ${\mathfrak{A}}$ is an $R$-connected structure over a Euclidean frame $\langle W,R\rangle$, then all worlds $w$ in $Q_{{\mathfrak{A}}}$ are reflexive (i.e $\langle w,w\rangle\in R$ holds) and $Q_{{\mathfrak{A}}}$ is an $R$-clique.

Proof 3.6**.**

In the course of proof we will refer to the formula (5) from Section 2.1, which defines Euclidean property. We will show that all worlds in $Q_{{\mathfrak{A}}}$ are reflexive and all worlds in $Q_{{\mathfrak{A}}}$ are $R$-equivalent. To show reflexivity take any $w\in Q_{{\mathfrak{A}}}$. By definition of $Q_{{\mathfrak{A}}}$ there exists $w^{\prime}\in W$ such that $\langle w^{\prime},w\rangle\in R$. Since ${\mathfrak{A}}$ satisfies (5), by taking $w^{\prime}$ as $x$ and $w$ as both $y$ and $z$ in (5), we infer $\langle w,w\rangle\in R$.

To demonstrate $R$-equivalence we will employ some simple observations. First, the relation $R\cap(Q_{{\mathfrak{A}}}\times Q_{{\mathfrak{A}}})$ is symmetric. To prove it take any $w_{1},w_{2}\in Q_{{\mathfrak{A}}}$ with $\langle w_{1},w_{2}\rangle\in R$. Then, use reflexivity of $w_{1}$ and the Euclidean property (with $w_{1}$ taken as $x$ and $z$ simultaneously, and $w_{2}$ as $y$ in (5)) to infer $\langle w_{2},w_{1}\rangle\in R$. Second, $R\cap(Q_{{\mathfrak{A}}}\times Q_{{\mathfrak{A}}})$ is transitive. To prove it take any $w_{1},w_{2},w_{3}\in Q_{{\mathfrak{A}}}$ with $\langle w_{1},w_{2}\rangle\in R$ and $\langle w_{2},w_{3}\rangle\in R$. Symmetry of $R\cap(Q_{{\mathfrak{A}}}\times Q_{{\mathfrak{A}}})$ gives us $\langle w_{2},w_{1}\rangle\in R$. Then, by the Euclidean property (with $w_{2}$ taken as $x$, $w_{3}$ taken as $z$, and $w_{1}$ as $y$ in (5)) we infer $\langle w_{1},w_{3}\rangle\in R$. Third, if $\langle l,w_{1}\rangle\in R$ and $\langle l,w_{2}\rangle\in R$, for some $l\in L$ and $w_{1},w_{2}\in Q_{{\mathfrak{A}}}$, then $\langle w_{1},w_{2}\rangle\in R\cup R^{-1}$. This observation again simply follows from (5).

Now take any $w\in Q_{{\mathfrak{A}}}$. We will show that $Q_{{\mathfrak{A}}}=Q_{{\mathfrak{A}}}(w)$, i.e. that $Q_{{\mathfrak{A}}}$ is the R-clique for $w$. Take any $w^{\prime}\in Q_{{\mathfrak{A}}}$. We will show that both $\langle w,w^{\prime}\rangle\in R$ and $\langle w^{\prime},w\rangle\in R$. Since ${\mathfrak{A}}$ is connected, there exists a $(R\cup R^{-1}$)-path from $w$ to $w^{\prime}$ in ${\mathfrak{A}}$. By inductive application of the third observation above we may assume that all elements of the path belong to $Q_{{\mathfrak{A}}}$. Then by the first observation (symmetry) we may assume that this is actually an $R$-path. Then, by the second observation (transitivity) the path reduces to a single edge $\langle w,w^{\prime}\rangle\in R$. In the same way we may show that $\langle w^{\prime},w\rangle\in R$. Thus all worlds in $Q_{{\mathfrak{A}}}$ are $R$-equivalent with $w$. Since all other worlds in ${\mathfrak{A}}$ are lanterns, they cannot be $R$-equivalent with $w$. Thus $Q_{{\mathfrak{A}}}$ is indeed the R-clique for $w$.

3.2 The universal modality

Before we start proving complexity results for the family of Euclidean logics, we show that global and local satisfiability problems are inter-reducible over any class of frames involving the Euclidean property.

Having restricted our attention to $R$-connected models, we will show that the universal modality $\mathbf{U}$ can be defined in terms of standard (i.e, $\Diamond$ and \ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) modalities. Recall that the semantics of $\mathbf{U}\varphi$ is defined as follows: ${\mathfrak{A}},w\models\mathbf{U}\varphi$, iff for every world $x$ the condition ${\mathfrak{A}},x\models\varphi$ holds. Taking a look at the shape of Euclidean structures (see e.g. Lemma 3.5), it is not difficult to see that to propagate satisfaction of a given formula $\varphi$ through the whole structure, it is sufficient to first traverse all inner elements and from each of them propagate the satisfaction of $\varphi$ to their predecessors. This intuition can be formalised by taking \mathbf{U}\varphi:=\varphi\wedge\Box\Box\ensurestackMath{\stackengine{.5pt}{\Box}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}\varphi.

Lemma 3.7**.**

Let ${\mathfrak{A}}=\langle W,R,V\rangle$ be an $R$-connected Euclidean structure. Then {\mathfrak{A}},w_{0}\models\varphi\wedge\Box\Box\ensurestackMath{\stackengine{.5pt}{\Box}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}\varphi holds for some world $w_{0}\in W$ iff ${\mathfrak{A}},v\models\varphi$ holds for all worlds $v\in W$.

Proof 3.8**.**

Let ${\mathfrak{A}}=\langle W,R,V\rangle$ be an $R$-connected Euclidean structure and let {\mathfrak{A}},w\models\varphi\wedge\Box\Box\ensurestackMath{\stackengine{.5pt}{\Box}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}\varphi hold for some world $w_{0}\in W$. We will show that it implies that $\varphi$ is true in every world $w\in W$ (the opposite direction of the Lemma is trivial).

First, if $R=\emptyset$ then ${\mathfrak{A}}$ is a singleton structure, because it is $R$-connected. In this case the implication trivially holds. So, assume that $R\neq\emptyset$. Define $S=R\circ R\circ R^{-1}$. We will show that $S$ is the universal relation $W\times W$. Indeed, take any $a,b\in W$. Then there exists $x\in Q_{{\mathfrak{A}}}$ such that $R(a,x)$ holds (if $a\in Q_{{\mathfrak{A}}}$ then, by Lemma 3.5, $a$ is reflexive, so take $x=a$; if $a\in L_{{\mathfrak{A}}}$, such an $x$ exists, since ${\mathfrak{A}}$ is connected). Similarly, there exists $y\in Q_{{\mathfrak{A}}}$ such that $R(b,y)$. Now we have $R(x,y)$, since $R$ is universal on $Q_{{\mathfrak{A}}}$ by Lemma 3.5. Thus we have $R(a,x)$, $R(x,y)$ and $R^{-1}(y,b)$, so $S(a,b)$ holds and thus $S=W\times W$. Therefore {\mathfrak{A}},w_{0}\models\Box\Box\ensurestackMath{\stackengine{.5pt}{\Box}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}\varphi implies {\mathfrak{A}},v\models\Box\Box\ensurestackMath{\stackengine{.5pt}{\Box}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}\varphi, for any $v\in W$.

We now argue that the local and global satisfiability problems coincide for modal logics over Euclidean frames.

Lemma 3.9**.**

Let $(\mathcal{L},\mathcal{F})$ be a modal logic whose language contains $\Diamond$ and \ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}} and $\mathcal{F}$ is a class of frames from the modal cube satisfying the Euclidean property. Then the global satisfiability problem for $\mathcal{F}(\mathcal{L}^{*})$ is LogSpace reducible to the local satisfiability problem for $\mathcal{F}(\mathcal{L}^{*})$ and vice-versa.

Proof 3.10**.**

As usual for modal logics we may restrict to satisfiability over connected structures. Since $\mathcal{F}$ is Euclidean and we have both $\Diamond$, \ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}} at our disposal, we know that the universal modality $\mathbf{U}$ is definable in $\mathcal{F}(\mathcal{L}^{*})$ (see: Lemma 3.7). From the semantics of $\mathbf{U}$ we can immediately conclude that any modal formulas $\varphi_{l},\varphi_{g}$ the following equivalences hold: $\varphi_{l}$ is locally-satisfiable iff $\neg\mathbf{U}\neg\varphi_{l}$ is globally-satisfiable and $\varphi_{g}$ is globally-satisfiable iff $\mathbf{U}\varphi_{g}$ is locally-satisfiable.

3.3 The upper bound for graded two-way K5 and D5

This Section is dedicated to the following theorem.

Theorem 3.11**.**

The local and global satisfiability problems for Euclidean Modal Logics \mbox{\rm K5}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) and \mbox{\rm D5}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) are in NExpTime.

Proof 3.12**.**

Note that here we may again restrict to satisfiability over connected frames. We start with the case of the class of all Euclidean frames K5. We translate a given modal formula $\varphi$ to the two-variable logic with counting $\mathrm{C}^{2}$, in which both graded modalities and the shape of connected Euclidean structures, as defined in Lemma 3.5, can be expressed. Since satisfiability of $\mathrm{C}^{2}$ is in NExpTime [Pratt-Hartmann (2007)], we obtain the desired conclusion. Recall the standard translation $\mathbf{st}$ from Section 2.2. Let $\mathit{lantern}(\cdot)$ be a new unary predicate and define $\varphi_{\mathbf{tr}}$ as

[TABLE]

Since $\mathbf{st}_{x}(\varphi)$ belongs to $\mathrm{GC}^{2}$, $\varphi_{\mathbf{tr}}$ belongs to $\mathrm{C}^{2}$ (but not to $\mathrm{GC}^{2}$), and has one free variable $x$. Let ${\mathfrak{B}}$ be a Kripke structure over a Euclidean frame. Expand ${\mathfrak{B}}$ to a structure ${\mathfrak{B}}^{+}$ by setting $\mathit{lantern}^{{\mathfrak{B}}^{+}}=\{w\in{\mathfrak{B}}\mid w\in L_{{\mathfrak{B}}}\}$. Taking into account Lemma 3.5 a structural induction on $\varphi$ easily establishes the following condition

[TABLE]

Thus, a \mbox{\rm K5}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) formula $\varphi$ is locally satisfiable if and only if the $\mathrm{C}^{2}$ formula $\exists_{\geq 1}{x}.\varphi_{\mathbf{tr}}$ is satisfiable, yielding a NExpTime algorithm for \mbox{\rm K5}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) local satisfiability. Membership of global satisfiability in NExpTime is implied by Lemma 3.7.

For the case of serial Euclidean frames, D5, it suffices to supplement the $\mathrm{C}^{2}$ formula defined in the case of K5 with the conjunct $\exists{x}.(\neg\mathit{lantern}(x))$ expressing seriality. Correctness follows then from the simple observation that a Euclidean frame is serial iff it contains at least one non-lantern world (recall that all these worlds are reflexive).

3.4 Lower bounds for two-way graded K5 and D5

We now show a matching NExpTime-lower bound for the logics from the previous section. We concentrate on local satisfiability, but by Lemma 3.7 the results will hold also for global satisfiability. Actually, we obtain a stronger result, namely, we show that the two-way graded modal logics K5 and D5 remain NExpTime-hard even if counting in one-way (either backward or forward) is forbidden. Hence, we show hardness of the logics \mbox{\rm K5}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) and \mbox{\rm D5}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}). We recall that this gives a higher complexity than the ExpTime-complexity of the language \Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}} [Demri and de Nivelle (2005)] and NP-complexity of the language $\Diamond_{\geq}$ [Kazakov and Pratt-Hartmann (2009)] over the same classes of frames.

In order to prove NExpTime-hardness of the Euclidean Two-Way Graded Modal Logics K5 and D5 we employ a variant of the classical tiling problem, namely exponential torus tiling problem from [Lutz (2002)].

Definition 3.13** (4.15 from [Lutz (2002)]).**

A torus tiling problem $\mathcal{P}$ is a tuple $(\mathcal{T},\mathcal{H},\mathcal{V})$, where $\mathcal{T}$ is a finite set of tile types and $\mathcal{H},\mathcal{V}\subseteq\mathcal{T}\times\mathcal{T}$ represent the horizontal and vertical matching conditions. Let $\mathcal{P}$ be a tilling problem and $c=t_{0},t_{1},\ldots,t_{n-1}\in\mathcal{T}^{n}$ an initial condition. A mapping $\tau:\{0,1,\ldots,2^{n}-1\}\times\{0,1,\ldots,2^{n}-1\}\rightarrow\mathcal{T}$ is a solution for $\mathcal{P}$ and $c$ if and only if, for all $i,j<2^{n}$, the following holds $(\tau(i,j),\tau(i\oplus_{2^{n}}1,j))\in\mathcal{H},(\tau(i,j),\tau(i,j\oplus_{2^{n}}1))\in\mathcal{V}$ and $\tau(0,i)=t_{i}$ for all $i<n$, where $\oplus_{i}$ denotes addition modulo $i$. It is well-known that there exists a NExpTime-complete torus tiling problem.

3.4.1 Outline of the proof.

The proof is based on a polynomial time reduction from a torus tiling problem as in Definition 3.13. Henceforward we assume that a NExpTime-complete torus tiling problem $\mathcal{P}=(\mathcal{T},\mathcal{H},\mathcal{V})$ is fixed. Let $c=t_{0},t_{1},\ldots,t_{n-1}\in\mathcal{T}^{n}$ be its initial condition. We write a formula which is (locally) satisfiable iff $\langle\mathcal{P},c\rangle$ has a solution. Each cell of the torus carries a position $\langle H,V\rangle\in\{0,1,\ldots,2^{n}-1\}\times\{0,1,\ldots,2^{n}-1\}$, encoded in binary in a natural way by means of propositional letters $v_{0},v_{1},\ldots,v_{n-1}$ and $h_{0},h_{1},\ldots,h_{n-1}$, with $h_{0}$ and $v_{0}$ denoting the least significant bits. In the reduction, a single cell of the torus corresponds to a unique inner, i.e., non-lantern, world. Since there are exactly $2^{n}\cdot 2^{n}$ cells, we enforce that also the total number of inner worlds is equal to $2^{n}\cdot 2^{n}$. We make use of graded modalities to specify that every inner world has exactly $2^{n}\cdot 2^{n}$ successors. We stress here that this is the only place where we employ counting. Thus the proof works in the case where graded converse modalities are disallowed (but the basic converse modality will be necessary). Alternatively we could equivalently write that every inner world has exactly $2^{n}\cdot 2^{n}$ inner predecessors, and obtain hardness of the language with graded converse modalities, but without graded forward modalities.

Once we enforced a proper size of our torus, we must be sure that two distinct inner worlds carry different positions. We do this in two steps. We first write that a world with position $(0,0)$ occurs in a model. For the second step, we assume that the grid is chessboard-like, i.e., all elements are coloured black or white in the same way as a chessboard is. Then, we say that every world is illuminated by four lanterns, where each of them propagates ${\oplus_{2^{n}}}1$ relation on the proper axis (from a black node to a white one and vice versa). Finally, having the torus prepared we encode a solution for the given tiling by simply labelling each inner world with some tile letter $t$ and ensure (from the vantage point of the lanterns) that any two horizontal or vertical neighbours do not violate the tiling constraints.

3.4.2 Encoding the exponential torus.

Our goal is now to define a formula describing the exponential torus. The shape of the formula is following:

[TABLE]

where $\mathbf{U}$ is the universal modality as in Lemma 3.7. The formula is going to say that: (i) the current world has position $(0,0)$; (ii) every world is either a lantern or an inner world; (iii) the torus is chessboard-like, i.e., its cells are with coloured with $\mathit{blk}$ (black) and with $\mathit{wht}$ (white) exactly as a real chessboard is; (iv) the overall size of the torus is equal to $2^{n}\cdot 2^{n}$; (v) each world of the torus has a proper vertical and a proper horizontal successor. The first four properties are straightforward to define:

[TABLE]

Note that the formula $\varphi_{\text{torusSize}}$ indeed expresses (iv), as the set of all inner worlds forms a clique. The obtained formulas are of polynomial length since the number $2^{n}\cdot 2^{n}$ is encoded in binary.

What remains is to define $\varphi_{\text{succ}}$. For this, for every inner world we ensure that there exists a proper lantern responsible for establishing the appropriate successor relation. There will be four different types of such lanterns, denoted by symbols: $\mathit{vbw}$, $\mathit{hbw}$, $\mathit{vwb}$, $\mathit{hwb}$. The intuition is the following: the first letter h or v indicates whether a lantern is responsible for an $H$– or $V$–relation. The last two letters say whether a successor relation will be established between black and white worlds, or in the opposite way.

[TABLE]

It suffices to define formulas $\varphi_{\mathit{vbw}}$, $\varphi_{\mathit{hbw}}$, $\varphi_{\mathit{vwb}}$ and $\varphi_{\mathit{hwb}}$. Let us first define $\varphi_{\mathit{vbw}}$. The formula below, intended to be interpreted at a lantern, consists of three parts: (i) the black and the white worlds illuminated by the lantern are pseudo-unique, i.e., all white (respectively, black) worlds illuminated by the same lantern carry the same position; uniqueness will follow later from $\varphi_{\text{torusSize}}$; (ii) all black worlds illuminated by the lantern have the same $H$-position as all white worlds illuminated by this lantern; (iii) if $V_{w}$ (respectively, $V_{b}$) encodes a $V$-position of the white (respectively, black) worlds illuminated by the lantern, then $V_{w}=V_{b}\oplus_{2^{n}}1$. Let us define $\varphi_{\mathit{vbw}}$ as:

[TABLE]

The definitions of the first and the second part of $\varphi_{\mathit{vbw}}$ are simple:

[TABLE]

[TABLE]

Finally we encode the $\oplus_{2^{n}}$-operation as the formula $\varphi_{V_{w}{=}V_{b}{\oplus_{2^{n}}}1}$ by, a rather standard, implementation of binary addition. Below we distinguish two cases: when $V_{b}$ is equal to $2^{n}{-}1$ and when $V_{b}$ is smaller than $2^{n}{-}1$.

[TABLE]

This completes the definition of $\varphi_{\mathit{vbw}}$. The following three definitions are analogous.

[TABLE]

The formula $\varphi_{\text{equalV}}$ can be obtained from $\varphi_{\text{equalH}}$ by replacing, for every $i$, the letter $h_{i}$ with the letter $v_{i}$, and defining the formulas $\varphi_{H_{w}{=}H_{b}{\oplus_{2^{n}}}1}$, $\varphi_{V_{b}{=}V_{w}{\oplus_{2^{n}}}1}$ and $\varphi_{H_{b}{=}H_{w}{\oplus_{2^{n}}}1}$ as simple modifications of $\varphi_{V_{w}{=}V_{b}{\oplus_{2^{n}}}1}$. While modifying the mentioned formula one should only switch $\mathit{blk}$ and $\mathit{wht}$ propositional symbols and possibly change $v$ to $h$ (when we consider adding $\oplus_{2^{n}}1$ on the $H$ axis).

The following Lemma simply states that the formula $\varphi_{\text{torus}}$ indeed defines a valid torus. Its proof is routine and follows directly from correctness of all presented formulas.

Lemma 3.14**.**

Assume that the the formula $\varphi_{\text{torus}}$ is locally satisfied at a world $w$ of a Euclidean structure ${\mathfrak{A}}=\langle W,R,V\rangle$. Then, set $Q_{{\mathfrak{A}}}(w)$, i.e., the $R$-clique for $w$, contains exactly $2^{n}\cdot 2^{n}$ elements and each of them carries a different position $\langle H,V\rangle$, i.e., there are no two worlds $v,v^{\prime}$ satisfying exactly the same $h_{i}$- and $v_{i}$-predicates.

Having defined a proper torus, it is quite easy to encode a solution to the torus tiling problem $\mathcal{P}$ with the initial condition $c$. Each inner node will be labelled with a single tile from $\mathcal{T}$ and using appropriate lanterns we enforce that any two neighbouring worlds do not violate the tiling rules $\mathcal{H}$ and $\mathcal{V}$. This is the purpose of the formula $\varphi_{\text{tiling}}$ defined below:

[TABLE]

The first conjunct specifies that each inner world is labeled with exactly one tile.

[TABLE]

The second conjunct distributes the initial tiling among torus cells. To define it we use handy macros $V{=}k$ and $H{=}k$, with their intuitive meaning that the binary representation of the number $k$ is written on atomic letters $v_{0},v_{1},\ldots,v_{n-1}$ and $h_{0},h_{1},\ldots,h_{n-1}$, respectively. Thus:

[TABLE]

The last formula says that any two successive worlds do not violate tiling rules. Since any two neighbours are connected via a lantern, we describe the formula from the point of view of such lantern.

[TABLE]

In the following lemma we claim that the presented reduction is correct. Its proof is once again routine and follows directly from correctness of all presented formulas.

Lemma 3.15**.**

Let $\varphi_{\text{reduction}}\stackrel{{\scriptstyle\text{def}}}{{=}}\varphi_{\text{torus}}\wedge\varphi_{\text{tiling}}$. The torus tiling problem instance $\langle\mathcal{P},c\rangle$ has a solution if and only if the formula is $\varphi_{\text{reduction}}$ locally-satisfiable.

Note that our intended models are serial. Thus, the result holds also for the logic D5. This gives the following theorem.

Theorem 3.16**.**

The local and global satisfiability problems for the logics \mbox{\rm K5}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) and \mbox{\rm D5}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) are NExpTime-hard.

Together with Theorem 3.11 this gives:

Theorem 3.17**.**

The local and global satisfiability problems for the logics \mbox{\rm K5}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), \mbox{\rm K5}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) and for logics \mbox{\rm D5}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), \mbox{\rm D5}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) are NExpTime-complete.

3.5 Transitive Euclidean frames

It turns out that the logics of transitive Euclidean frames have lower computational complexity. This is due to the following lemma.

Lemma 3.18**.**

Let ${\mathfrak{A}}$ be an $R$-connected structure over a transitive Euclidean frame $\langle W,R\rangle$. Then, every world $l\in L_{{\mathfrak{A}}}$ illuminates $Q_{{\mathfrak{A}}}$.

Proof 3.19**.**

Take any world $q\in Q_{{\mathfrak{A}}}$. We will show that a lantern $l$ illuminates $q$. Since $l$ has no $R$-predecessor and ${\mathfrak{A}}$ is $R$-connected, there exists a world $q^{\prime}\in Q_{{\mathfrak{A}}}$ such that $\langle l,q^{\prime}\rangle\in R$. By Lemma 3.5 set $Q_{{\mathfrak{A}}}$ is an $R$-clique, and thus we have $\langle q^{\prime},q\rangle\in R$. By transitivity we conclude that $\langle l,q\rangle\in R$. Thus a lantern $l$ illuminates $Q_{{\mathfrak{A}}}$.

A first-order formula stating that all non-lanterns are $R$-successors of all lanterns requires only two variables. Thus, as an immediate conclusion from Lemma 3.18, we can extend the translation developed in the previous section to handle the logic \mbox{\rm K45}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}), and obtain a NExpTime-upper bound for the satisfiability problem. In fact, the shape of transitive Euclidean structures is so simple that two-variable logic is no longer necessary. Below we translate \mbox{\rm K45}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) and \mbox{\rm D45}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) to one-variable logic with counting $\mathrm{C}^{1}$, which is NP-complete [Pratt-Hartmann (2008)].

Theorem 3.20**.**

The local and the global satisfiability problems for Transitive Euclidean Modal Logics \mbox{\rm K45}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) and \mbox{\rm D45}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) are in NP.

Proof 3.21**.**

The proof is similar in spirit to the proof of Lemma 3 in [Kazakov and Pratt-Hartmann (2009)]. Let $\mathit{lantern}(\cdot)$ be a new unary predicate. We first define translation function $\mathbf{tr}$ that, given a \mbox{\rm K45}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) formula $\varphi$, produces an equisatisfiable $\mathrm{C}^{1}$ formula $\mathbf{tr}(\varphi)$. We assume that all counting subscripts $\varphi$ are non-zero.

[TABLE]

Observe that $\mathbf{tr}(\varphi)$ is linear in the size of $\varphi$. Let ${\mathfrak{B}}$ be a Kripke structure over a transitive Euclidean frame. Expand ${\mathfrak{B}}$ to a structure ${\mathfrak{B}}^{+}$ by setting an interpretation of a symbol $\mathit{lantern}$ to be $\mathit{lantern}^{{\mathfrak{B}}^{+}}=\{w\in{\mathfrak{B}}\mid w\in L_{{\mathfrak{B}}}\}$. Taking into account Lemma 3.5 and Lemma 3.18, a structural induction on $\varphi$ easily establishes the following condition

[TABLE]

Thus, a \mbox{\rm K45}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) formula $\varphi$ is locally satisfiable if and only if $\mathrm{C}^{1}$ formula $\exists_{\geq 1}.{x}(\mathbf{tr}(x))$ is satisfiable, yielding an NP algorithm for \mbox{\rm K45}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) satisfiability. The algorithm for \mbox{\rm D45}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) is obtained by just a slight update to the one given above. It suffices to supplement the $\mathrm{C}^{1}$ formula defined in the case of K45 with the conjunct $\exists{x}.(\neg\mathit{lantern}(x))$ expressing seriality (cf. the proof of Theorem 3.11).

4 Transitive frames: counting successors, accessing predecessors

In this section, we consider the language \Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}, that is the modal language in which we can count the successors, but cannot count the predecessors, having at our disposal only the basic converse modality. Over all classes of frames involving neither transitivity nor Euclideanness local satisfiability is PSpace-complete and global satisfiability is ExpTime-complete, as the tight lower and upper bounds can be transferred from, resp., the one-way non-graded language $\Diamond$ and the full two-way graded language. Over the classes of Euclidean frames K5 and D5, both problems are NExpTime-complete, as proved in Theorem 3.17. Over the classes of transitive Euclidean frames KB45, K45, D45, and S5 the problems are NP-complete, as the lower bound transfers from the language $\Diamond$, and the upper bound from the full two-way graded language (Theorem 3.20). So, over all the above-discussed classes of frames the complexities of \Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}} and \Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq} coincide.

What is left are the classes of transitive frames K4, D4, and S4. Recall that, in contrast to their one-way counterparts, the two-way graded logics of transitive frames \mbox{\rm K4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}), \mbox{\rm D4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}), and \mbox{\rm S4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}_{\geq}) are undecidable [Zolin (2017)]. In [Zolin (2017)] the question is asked if the decidability is regained when the language is restricted to \Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}. Here we answer this question, demonstrating the local and global finite model property for the obtained logics; this implies that their satisfiability problems are indeed decidable.

In Lemma 5.5 from [Zolin (2017)], it is shown that over the class of transitive frames the global satisfiability and local satisfiability problems for the considered language are polynomially equivalent. Moreover, they are polynomially equivalent to the combined satisfiability problem, asking if for a given pair of formulas $\phi,\phi^{\prime}$ there exists a structure in which $\phi$ is true at every world and $\phi^{\prime}$ is true at some world. The remark following the proof of that lemma says that it holds also for reflexive transitive frames. The same can be easily shown also for serial transitive frames. We thus have:

Lemma 4.22**.**

For each of the logics \mbox{\rm K4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), \mbox{\rm D4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), and \mbox{\rm S4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) their global, local and combined satisfiability problems are polynomially equivalent.

Below we explicitly deal with global satisfiability. The above lemma implies, however, that our results apply also to local satisfiability.

Let us concentrate on the class K4 of all transitive frames. The finite model construction we are going to present is the most complicated part of this paper. It begins similarly to the exponential model construction in the case of local satisfiability of $\mbox{\rm K4}(\Diamond_{\geq})$ from [Kazakov and Pratt-Hartmann (2009)]: we introduce a Scott-type normal form (Lemma 4.23), and then generalize two pieces of model surgery used there (Lemma 4.25) to our setting: starting from any model, we first obtain a model with short paths of cliques and then we decrease the size of the cliques. Some modifications of the constructions from [Kazakov and Pratt-Hartmann (2009)] are necessary to properly deal with the converse modality; they are, however, rather straightforward. Having a model with short paths of cliques and small cliques, we develop some new machinery of clique profiles and clique types allowing us to decrease the overall size of the structure; this fragment is our main contribution.

Lemma 4.23**.**

Given a formula $\varphi$ of the language (\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), we can compute in polynomial time a formula $\psi$ of the form

[TABLE]

where the $p_{i}$, $q_{i}$, $p^{\prime}_{i}$, $q^{\prime}_{i}$ are propositional variables, the $C_{i}$, $D_{i}$ are natural numbers, and $\eta$ and the $\pi_{i}$, $\chi_{i}$, $\pi^{\prime}_{i}$, $\chi^{\prime}_{i}$ are propositional formulas, such that $\varphi$ and $\psi$ are globally satisfiable over exactly the same transitive frames.

Proof 4.24**.**

Follows by a routine renaming process, which is similar to the proof of Lemma 4 from [Kazakov and Pratt-Hartmann (2009)]).

Next, let us introduce some helpful terminology, copying it mostly from the above-mentioned paper [Kazakov and Pratt-Hartmann (2009)]. Let ${\mathfrak{A}}=\langle W,R,V\rangle$ be a transitive structure, and $w_{1},w_{2}\in W$. We say that $w_{2}$ is an $R$-successor of $w_{1}$ if $\langle w_{1},w_{2}\rangle\in R$; $w_{2}$ is a strict $R$-successor of $w_{1}$ if $\langle w_{1},w_{2}\rangle\in R$, but $\langle w_{2},w_{1}\rangle\not\in R$; $w_{2}$ is a direct $R$-successor of $w_{1}$ if $w_{2}$ is a strict $R$-successor of $w_{1}$ and, for every $w\in W$ such that $\langle w_{1},w\rangle\in R$ and $\langle w,w_{2}\rangle\in R$ we have either $w\in Q_{\mathfrak{A}}(w_{1})$ or $w\in Q_{\mathfrak{A}}(w_{2})$. Recall that $Q_{\mathfrak{A}}(w)$ denotes the $R$-clique for $w$ in ${\mathfrak{A}}$.

The depth of a structure ${\mathfrak{A}}$ is the maximum over all $k\geq 0$ for which there exist worlds $w_{0},\ldots,w_{k}\in W$ such that $w_{i}$ is a strict $R$-successor of $w_{i-1}$ for every $1\leq i\leq k$, or $\infty$ if no such a maximum exists. The breadth of ${\mathfrak{A}}$ is the maximum over all $k\geq 0$ for which there exist worlds $w,w_{1},\ldots,w_{k}$ such that $w_{i}$ is a direct $R$-successor of $w$ for every $1\leq i\leq k$, and the sets $Q_{{\mathfrak{A}}}(w_{1}),\ldots Q_{{\mathfrak{A}}}(w_{k})$ are disjoint, or $\infty$ if no such a maximum exists. The width of ${\mathfrak{A}}$ is the smallest $k$ such that $k\geq|Q_{\mathfrak{A}}(w)|$ for all $w\in W$, or $\infty$ if no such $k$ exists.

Lemma 4.25**.**

Let $\varphi$ be a normal form formula as in Equation 4.23. If $\varphi$ is globally satisfied in a transitive model ${\mathfrak{A}}$ then it is globally satisfied in a transitive model ${\mathfrak{A}}^{\prime}$ with depth $d^{\prime}\leq(\sum_{i=1}^{m}D_{i})+m+m^{\prime}+1$ and width $c^{\prime}\leq(\sum_{i=1}^{l}C_{i})+l^{\prime}+1$.

Proof 4.26**.**

The proof is a construction being a minor modification of Stages 1 and 4 of the construction from the proof of Lemma 6 in [Kazakov and Pratt-Hartmann (2009)], where the language without backward modalities is considered. We closely follow the lines of Kazakov and Pratt-Hartmann’s construction, just taking additional care of backward witnesses. We remark here that also Stage 2 of the above mentioned construction could be adapted, giving a better bound on the depth of ${\mathfrak{A}}^{\prime}$. We omit it here since such an improvement would not be crucial for our purposes. Stage 3 cannot be directly adapted.

Let us turn to the detailed proof.

Stage 1. Small depth.* Let ${\mathfrak{A}}=\langle W,R,V\rangle$. For $w\in W$ define $d^{i}_{\mathfrak{A}}(w):=\min(D_{i}+1,|\{w^{\prime}:{\mathfrak{A}},w^{\prime}\models\chi_{i},\langle w,w^{\prime}\rangle\in R^{*}\}|)$ where $D_{i}$ and $\chi_{i}$, $1\leq i\leq m$, are as in Equation 4.23 and $R^{*}$ is the reflexive closure of $R$. We also define S_{\mathfrak{A}}(w):=\{\chi^{\prime}_{i}:\text{there is~{}w^{\prime} such that }{\mathfrak{A}},w^{\prime}\models\chi^{\prime}_{i}\text{ and }\langle w^{\prime},w\rangle\in R^{*}\}, where $\chi^{\prime}_{i}$, $1\leq i\leq m^{\prime}$ are also as in Equation 4.23.*

Let R_{\sim}:=\{\langle w_{1},w_{2}\rangle\in R:d^{i}_{\mathfrak{A}}(w_{1})=d^{i}_{\mathfrak{A}}(w_{2})\text{ for all~{}1\leq i\leq m and }S_{\mathfrak{A}}(w_{1})=S_{\mathfrak{A}}(w_{2})\} be the restriction of $R$ to pairs of worlds that have the same values of the $d^{i}_{\mathfrak{A}}$ and $S_{\mathfrak{A}}$. Let $R^{-}_{\sim}$ be the inverse of $R_{\sim}$. Let ${\mathfrak{A}}^{\prime}=\langle W,R^{\prime},V\rangle$ be obtained from ${\mathfrak{A}}=\langle W,R,V\rangle$ by setting $R^{\prime}:=(R\cup R^{-}_{\sim})^{+}$, where the superscript $+$ is the transitive closure operator. Intuitively, if $w_{1}$ is $R$-reachable from $w_{2}$ $w_{1}$ and $w_{2}$ agree on the number (up to the limit of $D_{i}$) of the worlds satisfying $\chi_{i}$ reachable from them, for all $1\leq i\leq m$, and, for all $i$, $w_{1}$ is an $R$-successor of a world satisfying $\chi_{i}^{\prime}$ iff $w_{2}$ is, then we make $w_{1}$ and $w_{2}$ $R^{\prime}$-equivalent. The effect is that some $R$-cliques of ${\mathfrak{A}}$ are joined into bigger $R$-cliques in ${\mathfrak{A}}^{\prime}$. We show that ${\mathfrak{A}}^{\prime}$ satisfies $\varphi$ and has appropriately bounded depth.

For every $w_{1},w_{2}\in W$ such that $w_{2}$ is a strict $R^{\prime}$-successor of $w_{1}$, we have $d^{i}_{\mathfrak{A}}(w_{1})\geq d^{i}_{\mathfrak{A}}(w_{2})$ for all $1\leq i\leq m$, $S_{\mathfrak{A}}(w_{1})\subseteq S_{\mathfrak{A}}(w_{2})$ and either $d^{i}_{\mathfrak{A}}(w_{1})>d^{i}_{\mathfrak{A}}(w_{2})$ for some $i$, and thus $\sum_{i=1}^{m}d^{i}_{\mathfrak{A}}(w_{1})>\sum_{i=1}^{m}d^{i}_{\mathfrak{A}}(w_{2})$ or the inclusion $S_{\mathfrak{A}}(w_{1})\subseteq S_{\mathfrak{A}}(w_{2})$ is strict. Since $d^{i}_{\mathfrak{A}}(w)\leq D_{i}+1$ for every $w\in W$ and every $1\leq i\leq m$, and the size of $S_{\mathfrak{A}}(w)$ is bounded by $m^{\prime}$, the length of every chain $w_{0},\ldots,w_{k}$ such that $w_{i}$ is a strict $R^{\prime}$-successor of $w_{i-1}$ is bounded by $(\sum_{i=1}^{m}D_{j})+m+m^{\prime}+1$.

In order to prove that ${\mathfrak{A}}^{\prime}\models\varphi$, we first prove that $d^{i}_{\mathfrak{A}}(w)=d^{i}_{{\mathfrak{A}}^{\prime}}(w)$ for every $w\in W$ and $1\leq i\leq m$. Assume to the contrary that $d^{i}_{\mathfrak{A}}(w)\not=d^{i}_{{\mathfrak{A}}^{\prime}}(w)$ for some $w\in W$ and some $i$. Since $R\subseteq R^{\prime}$, we have $d^{i}_{\mathfrak{A}}(w)<d^{i}_{{\mathfrak{A}}^{\prime}}(w)\leq D_{i}+1$, which means, in particular, that there exists an element $w^{\prime}\in W$ with ${\mathfrak{A}},w^{\prime}\models\chi_{i}$, such that $\langle w,w^{\prime}\rangle\in R^{\prime}$ but $\langle w,w^{\prime}\rangle\not\in R$.

Since $\langle w,w^{\prime}\rangle\in R^{\prime}$, by definition of $R^{\prime}$, there exists a sequence $w_{0},\ldots,w_{k}$ of different worlds in $W$ such that $w_{0}=w$, $w_{k}=w^{\prime}$ and $\langle w_{j-1},w_{j}\rangle\in R\cup R^{-}_{\sim}$ for every $1\leq j\leq k$. Note that $d^{i}_{\mathfrak{A}}(w_{j-1})\geq d^{i}_{\mathfrak{A}}(w_{j})$ for every $1\leq j\leq k$ and every $1\leq i\leq m$. Take the maximal $j$ such that $\langle w_{j-1},w^{\prime}\rangle\not\in R$. Since $\langle w_{0},w^{\prime}\rangle=\langle w,w^{\prime}\rangle\not\in R$, such a maximal $j$ always exists. Then $\langle w_{j},w^{\prime}\rangle\in R^{*}$, and $\langle w_{j-1},w_{j}\rangle\not\in R$. Since $\langle w_{j-1},w_{j}\rangle\in R\cup R^{-}_{\sim}$, we have $\langle w_{j-1},w_{j}\rangle\in R^{-}_{\sim}$, and so $d^{i}_{\mathfrak{A}}(w_{j-1})=d^{i}_{{\mathfrak{A}}}(w_{j})$ by definition of $R_{\sim}$. Since $d^{i}_{\mathfrak{A}}(w_{j})\leq d^{i}_{\mathfrak{A}}(w_{0})=d^{i}_{\mathfrak{A}}(w)<D_{i}+1$, we obtain a contradiction, due to the fact that $d^{i}_{{\mathfrak{A}}}(w_{j-1})=d^{i}_{\mathfrak{A}}(w_{j})\leq D_{i}$, $\langle w_{j-1},w\ \rangle\not\in R^{*}$, $\langle w_{j},w^{\prime}\rangle\in R^{*}$, $\langle w_{j},w_{j-1}\rangle\in R$, and ${\mathfrak{A}},w^{\prime}\models\chi_{i}$.

The observation that $S_{\mathfrak{A}}(w)=S_{{\mathfrak{A}}^{\prime}}(w)$ for all $w\in W$ is even simpler. Assume to the contrary that this equality does not hold for some $w\in W$. This means that $\chi^{\prime}_{i}\in S_{{\mathfrak{A}}^{\prime}}(w)$ and $\chi^{\prime}_{i}\not\in S_{{\mathfrak{A}}}(w)$ for some $1\leq i\leq m^{\prime}$. In particular, there exists an element $w^{\prime}\in W$ with ${\mathfrak{A}},w^{\prime}\models\chi^{\prime}_{i}$, such that $\langle w^{\prime},w\rangle\in R^{\prime}$ but $\langle w^{\prime},w\rangle\not\in R$. Thus, there is a sequence of different worlds $w^{\prime}=w_{0},\ldots,w_{k}=w$ such that  $\langle w_{j-1},w_{j}\rangle\in R\cup R^{-}_{\sim}$ for every $1\leq j\leq k$. Note that $S_{\mathfrak{A}}(w_{j-1})\subseteq S_{\mathfrak{A}}(w_{j})$ for every $1\leq j\leq k$. Since $\chi_{i}^{\prime}\in S_{\mathfrak{A}}(w_{0})$ it follows that $\chi_{i}^{\prime}\in S_{\mathfrak{A}}(w_{k})$. Contradiction.

To complete the proof that ${\mathfrak{A}}^{\prime}\models\varphi$ we demonstrate that, if $\psi$ is any conjunct of $\varphi$ and $w\in W$, then ${\mathfrak{A}},w\models\psi$ implies ${\mathfrak{A}}^{\prime},w\models\psi$. Indeed, for the propositional formula $\eta$ it is immediate. For subformulas $(p_{i}\rightarrow\Diamond_{\geq C_{i}}\pi_{i})$ and (p^{\prime}_{i}\rightarrow\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}\pi^{\prime}_{i}) this holds since $R\subseteq R^{\prime}$. For subformulas $(q_{i}\rightarrow\Diamond_{\leq D_{i}}\chi_{i})$ this follows from the property $d^{i}_{\mathfrak{A}}(w)=d^{i}_{{\mathfrak{A}}^{\prime}}(w)$. Finally, for subformulas $(q^{\prime}_{i}\rightarrow\boxminus\neg\chi^{\prime}_{i})$ this follows from the property $S_{\mathfrak{A}}(w)=S_{{\mathfrak{A}}^{\prime}}(w)$.

Stage 2. Small width.* By Stage 1 we may assume that ${\mathfrak{A}}$ has depth bounded by $(\sum_{i=1}^{m}D_{j})+m+m^{\prime}+1$. For every element $w\in W$ we define $Q_{\pi_{i}}(w)$ to be the set of elements of $Q_{\mathfrak{A}}(w)$ for which $\pi_{i}$ holds ($1\leq i\leq l$) and $Q_{\pi^{\prime}_{i}}(w)$ to be the set of elements of $Q_{\mathfrak{A}}(w)$ for which $\pi^{\prime}_{i}$ holds ($1\leq i\leq l^{\prime}$). We call the elements of each $Q_{\pi}(w)$ the equivalent $\pi$-witnesses for $w$. Note that for each relevant $\pi$ we have $Q_{\pi}(w_{1})=Q_{\pi}(w_{2})$ when $w_{1}$ and $w_{2}$ are $R$-equivalent. For $1\leq i\leq l$, let $Q^{\prime}_{\pi_{i}}(w)$ be $Q_{\pi_{i}}(w)$ if $|Q_{\pi_{i}}(w)|\leq C_{i}$, or, otherwise, a subset of $Q_{\pi_{i}}(w)$ which contains exactly $C_{i}$ elements. We call $Q^{\prime}_{\pi_{i}}(w)$ the selected equivalent $\pi_{i}$-witnesses for $w$. For $1\leq i\leq l^{\prime}$, let $Q^{\prime}_{\pi^{\prime}_{i}}(w)$ be $Q_{\pi^{\prime}_{i}}(w)$ if $|Q_{\pi_{i}}(w)|\leq 1$, or, otherwise, a singleton subset of $Q_{\pi_{i}}(w)$. We call $Q^{\prime}_{\pi_{i}}(w)$ the selected equivalent $\pi^{\prime}_{i}$-witness for $w$. Additionally, define $Q^{\prime}_{*}(w)$ to be any singleton subset of $Q_{\mathfrak{A}}(w)$. We assume that if $w_{1}$ and $w_{2}$ are $R$-equivalent then $Q^{\prime}_{\pi_{i}}(w_{1})=Q^{\prime}_{\pi_{i}}(w_{2})$ for all $1\leq i\leq l$, $Q^{\prime}_{\pi^{\prime}_{i}}(w_{1})=Q^{\prime}_{\pi^{\prime}_{i}}(w_{2})$ for $1\leq i\leq l^{\prime}$, and $Q^{\prime}_{*}(w_{1})=Q^{\prime}_{*}(w_{2})$. Define the structure ${\mathfrak{A}}^{\prime}=\langle W^{\prime},R^{\prime},V^{\prime}\rangle$ by setting $W^{\prime}=\bigcup_{w\in W,1\leq i\leq l}Q^{\prime}_{\pi_{i}}(w)\cup\bigcup_{w\in W,1\leq i\leq l^{\prime}}Q^{\prime}_{\pi^{\prime}_{i}}(w)\cup Q^{\prime}_{*}(w)$, $R^{\prime}:=R\!\!\restriction\!\!W^{\prime}$, and $V^{\prime}=V\!\!\restriction\!\!W^{\prime}$. Intuitively ${\mathfrak{A}}^{\prime}$ is obtained from ${\mathfrak{A}}$ by removing elements in every $R$-clique, except for those that are selected witnesses for other elements or are members of the singleton set $Q_{*}$, guaranteeing that the clique will remain non-empty. It is not difficult to see that ${\mathfrak{A}}^{\prime}$ has the required properties. In particular our selection process selects at most $(\sum_{i=1}^{l}C_{i})+l^{\prime}+1$ elements in every $R$-clique.*

To describe our next step, we need a few more definitions. Given a world $w$ of a structure ${\mathfrak{A}}$, we define its depth as the maximum over all $k\geq 0$ for which there exist worlds $w=w_{0},\ldots,w_{k}\in W$ such that $w_{i}$ is a strict $R$-successor of $w_{i-1}$ for every $1\leq i\leq k$, or as $\infty$ if no such a maximum exists. For an $R$-clique $Q$ we define its depth as the depth of $w$ for any $w\in Q$; this definition is sound since for all $w_{1}\in Q_{{\mathfrak{A}}}(w)$ the depth of $w$ is equal to the depth of $w_{1}$.

From this point, we will mostly work on the level of cliques rather than individual worlds. We may view any structure ${\mathfrak{A}}$ as a partially ordered set of cliques. We write $\langle Q_{1},Q_{2}\rangle\in R$, and say that a clique $Q_{1}$ sends an edge to a clique $Q_{2}$ (or that $Q_{2}$ receives an edge from $Q_{1}$) if $\langle w_{1},w_{2}\rangle\in R$ for any (equivalently: for all) $w_{1}\in Q_{1}$, $w_{2}\in Q_{2}$.

A $1$-type of a world $w$ in ${\mathfrak{A}}$ is the set of all propositional variables $p$ such that ${\mathfrak{A}}\models p$. We sometimes identify a $1$-type with the conjunction of all its elements and negations of variables it does not contain. Given a natural number $k$, a structure ${\mathfrak{A}}$ and a clique $Q$ in this structure ${\mathfrak{A}}$, we define a $k$-profile of $Q$ (called just a profile if $k$ is clear from the context) in ${\mathfrak{A}}$ as the tuple $prof^{k}_{\mathfrak{A}}(Q)=(\mathcal{H},\mathcal{A},\mathcal{B},\text{\emph{irref}})$, where $\mathcal{H}$ is the multiset of $1$-types in which the number of copies of each $1$-type $\alpha$ equals $\min(k+1,|\{w\in Q:{\mathfrak{A}},w\models\alpha\}|)$, $\mathcal{A}$ is the multiset of $1$-types in which the number of copies of each $1$-type $\alpha$ equals \min(k,|\{w:{\mathfrak{A}},w\models\alpha\text{ and~{}w$is a strict~{}$R-successor of a world from }~{}Q$\}|)$, $\mathcal{B}$ is the set of $1$-types of worlds for which a world from $Q$ is its strict $R$-successor, and irref is a Boolean variable set to $1$ iff the clique consists of a single irreflexive element (note that if the clique contains at least two elements then they all must be reflexive). Intuitively, $\mathcal{H}$ counts (up to $k+1$) realizations of $1$-types (H)ere in Q, $\mathcal{A}$ counts (up to $k$) realizations $1$-types (A)bove $Q$, and $\mathcal{B}$ says which $1$-types appear (B)elow $Q$. Usually, given a normal form $\varphi$ as in Equation 4.23, we will be interested in $M_{\varphi}$-profiles of cliques, where $M_{\varphi}=\max(\{C_{i}\}_{i=1}^{l}\cup\{D_{i}+1\}_{i=1}^{m})$. Note that, given the $M_{\varphi}$-profiles of all cliques in a structure we are able to determine whether this structure is a global model of $\varphi$. Indeed, given the $M_{\varphi}$-profile of a clique we know the $1$-types of elements it contains, for each such element we can count, at least up to $M_{\varphi}$, how many successors of each $1$-type it has (for this we use the values of $\mathcal{H}$, $\mathcal{A}$ and irref), and for each element we know the set of $1$-types of its predecessors (for this we use the values of $\mathcal{H}$, $\mathcal{B}$ and irref). Clearly, this information is sufficient to check if every conjunct of $\varphi$ is satisfied. The following observation is also straightforward.

Lemma 4.27**.**

If ${\mathfrak{A}}\models\varphi$ for a normal form $\varphi$, and if in a structure ${\mathfrak{A}}^{\prime}$ the $M_{\varphi}$-profile of every clique is equal to the $M_{\varphi}$-profile of some clique from ${\mathfrak{A}}$, then ${\mathfrak{A}}^{\prime}\models\varphi$.

We now prove the finite model property.

Lemma 4.28**.**

Let $\varphi$ be a normal form formula. If $\varphi$ is globally satisfied in a transitive model ${\mathfrak{A}}$ then it is globally satisfied in a finite transitive model ${\mathfrak{A}}^{\prime}$.

Proof 4.29**.**

Construction of ${\mathfrak{A}}^{\prime}$.* We assume that $\varphi$ is as in Equation 4.23. By Lemma 4.25, we may assume that ${\mathfrak{A}}=\langle W,R,V\rangle$ has depth $d\leq(\sum_{i=1}^{m}D_{i})+m+m^{\prime}+1$ and width $c\leq(\sum_{i=1}^{l}C_{i})+l^{\prime}+1$. Note that ${\mathfrak{A}}$ may be infinite due to possibly infinite breadth.*

Let us split $W$ into sets $U_{0},\ldots,U_{d}$ with $U_{i}$ consisting of all elements of $W$ of depth $i$ in ${\mathfrak{A}}$ (equivalently speaking: being the union of all cliques of depth $i$ in ${\mathfrak{A}}$). They are called layers. Note that cliques from $U_{i}$ may send $R$-edges only to cliques from $U_{j}$ with $j<i$.

We now inductively define a sequence of models ${\mathfrak{A}}={\mathfrak{A}}_{-1},{\mathfrak{A}}_{0},\ldots,{\mathfrak{A}}_{d}={\mathfrak{A}}^{\prime}$, with ${\mathfrak{A}}_{i}=\langle W_{i},R_{i},V_{i}\rangle$ such that

• •

$W_{i}=U^{\prime}_{0}\cup\ldots\cup U^{\prime}_{i}\cup U_{i+1}\cup\ldots\cup U_{d}$, where each $U^{\prime}_{i}$ is a finite union of some cliques from $U_{i}$,

• •

$V_{i}=V\!\!\restriction\!\!W_{i}$**

• •

${\mathfrak{A}}_{i}\!\!\restriction\!\!(U^{\prime}_{0}\cup\ldots\cup U^{\prime}_{i})={\mathfrak{A}}_{i-1}\!\!\restriction\!\!(U^{\prime}_{0}\cup\ldots\cup U^{\prime}_{i})$,

• •

${\mathfrak{A}}_{i}\!\!\restriction\!\!(U^{\prime}_{0}\cup\ldots\cup U^{\prime}_{i-1}\cup U_{i+1}\cup\ldots\cup U_{d})={\mathfrak{A}}_{i-1}\!\!\restriction\!\!(U^{\prime}_{0}\cup\ldots\cup U^{\prime}_{i-1}\cup U_{i+1}\cup\ldots\cup U_{d})$**

• •

in particular: ${\mathfrak{A}}_{i}\!\!\restriction\!\!(U_{i+1}\cup\ldots\cup U_{d})={\mathfrak{A}}\!\!\restriction\!\!(U_{i+1}\cup\ldots\cup U_{d})$.

We obtain ${\mathfrak{A}}_{i}$ from ${\mathfrak{A}}_{i-1}$ by distinguishing a fragment $U^{\prime}_{i}$ of $U_{i}$, removing $U_{i}\setminus U^{\prime}_{i}$ and adding some edges from $U_{i+1}\cup\ldots\cup U_{d}$ to $U^{\prime}_{i}$; all the other edges remain untouched. We do it carefully, to avoid modifications of the profiles of the surviving cliques. Let us describe the process of constructing ${\mathfrak{A}}_{i}$ in details.

Assume $i\geq 0$. We first distinguish a finite subset $U_{i}^{\prime}$ of $U_{i}$. We define a clique type of every clique $Q$ from $U_{i}$ in ${\mathfrak{A}}_{i-1}$ as a triple $(\mathcal{H},\mathcal{B},S)$,where $\mathcal{H}$, and $\mathcal{B}$ are as in $prof^{M_{\varphi}}_{{\mathfrak{A}}_{i-1}}(Q)$ and $S$ is the subset of cliques from $U_{0}^{\prime}\cup\ldots\cup U^{\prime}_{i-1}$, consisting of those cliques to which $Q$ sends an $R_{i-1}$-edge. We stress that during the construction of ${\mathfrak{A}}_{i}$, the clique types of cliques are always computed in ${\mathfrak{A}}_{i-1}$. In particular $S$ is empty for $i=0$ and, as we will always have that $U_{0}^{\prime}\cup\ldots\cup U^{\prime}_{i-1}$ is finite, $S$ is finite for any $i>0$. Thus for each $i$ there will be only finitely many clique types.

For every clique type $\beta$ realized in $U_{i}$, we mark $M_{\varphi}$ cliques of this type, or all such cliques if there are less than $M_{\varphi}$ of them. Let $U^{\prime}_{i}$ be the union of the marked cliques. We fix some arbitrary numbering of the marked cliques.

Now we define the relation $R_{i}$. As said before, for any pair of cliques $Q_{1},Q_{2}$ both of which are contained in $U^{\prime}_{0}\cup\ldots\cup U^{\prime}_{i-1}\cup U_{i+1}\cup\ldots\cup U_{d}$ or in $U^{\prime}_{0}\cup\ldots\cup U^{\prime}_{i}$, we set $\langle Q_{1},Q_{2}\rangle\in R_{i}$ iff $\langle Q_{1},Q_{2}\rangle\in R_{i-1}$. It remains to define the $R_{i}$-edges from $U_{i+1}\cup\ldots\cup U_{d}$ to $U^{\prime}_{i}$. For every clique $Q$ from $U_{i+1}\cup\ldots\cup U_{d}$ and every clique type $\beta$ realized in $U_{i}^{\prime}$, let $f(\beta)$ be the number of $R_{i-1}$-edges sent by $Q$ to cliques of type $\beta$ in $U_{i}$, if this number is not greater than $M_{\varphi}$, or, otherwise, let $f(\beta)=M_{\varphi}$. Let $f^{\prime}(\beta)$ be the number of $R_{i-1}$-edges sent by $Q$ to cliques of type $\beta$ in $U^{\prime}_{i}$ (recall that this number is not greater than $M_{\varphi}$). We let all the $R_{i-1}$-edges sent by $Q$ to the cliques of type $\beta$ in $U^{\prime}_{i}$ to be also members of $R_{i}$, that is, to be edges in ${\mathfrak{A}}_{i}$. Additionally, we link $Q$ by $R_{i}$ to the first (with respect to the numbering we have fixed) $f(\beta)-f^{\prime}(\beta)$ cliques of type $\beta$ in $U^{\prime}_{i}$ to which $Q$ is not linked by $R_{i-1}$. By the choice of $U^{\prime}_{i}$, we have enough such cliques in $U^{\prime}_{i}$. We finish the construction of ${\mathfrak{A}}_{i}$ by removing all the cliques from $U_{i}\setminus U^{\prime}_{i}$.

That ${\mathfrak{A}}_{i}$ has the desired properties is shown in the following two claims.

Claim 1: Each of the ${\mathfrak{A}}_{i}$ is a transitive structure.**

We show this by induction by $i={-1},0,\ldots,d$. Obviously ${\mathfrak{A}}_{-1}={\mathfrak{A}}$ is transitive. Assume that ${\mathfrak{A}}_{i-1}$ is transitive, and assume to the contrary that ${\mathfrak{A}}_{i}$ is not. This means there are cliques $Q_{1},Q_{2},Q_{3}$ in ${\mathfrak{A}}_{i}$ such that $\langle Q_{1},Q_{2}\rangle\in R_{i}$, $\langle Q_{2},Q_{3}\rangle\in R_{i}$ but $\langle Q_{1},Q_{3}\rangle\not\in R_{i}$. It is easy to see that the cliques $Q_{1},Q_{2},Q_{3}$ must belong to three different layers, and that precisely one of the two cases holds: either $Q_{2}\subseteq U^{\prime}_{i}$, $\langle Q_{1},Q_{2}\rangle\not\in R_{i-1}$, $\langle Q_{2},Q_{3}\rangle\in R_{i-1}$ or $Q_{3}\subseteq U^{\prime}_{i}$, $\langle Q_{1},Q_{2}\rangle\in R_{i-1}$, $\langle Q_{2},Q_{3}\rangle\not\in R_{i-1}$. In the first case, our construction implies that there is a clique $Q^{\prime}\subseteq U_{i}\setminus U^{\prime}_{i}$ such that $\langle Q_{1},Q^{\prime}\rangle\in R_{i-1}$, and the clique-types of $Q_{2}$ and $Q^{\prime}$ are identical. But from the latter it follows that $\langle Q^{\prime},Q_{3}\rangle\in R_{i-1}$ and from transitivity of $R_{i-1}$ we have $\langle Q_{1},Q_{3}\rangle\in R_{i-1}$. Since none of $Q_{1}$, $Q_{3}$ is contained in $U_{i}$, by our construction we have that $\langle Q_{1},Q_{3}\rangle\in R_{i}$. Contradiction. In the second case, let $\beta$ be the clique-type of $Q_{3}$ and let $Q^{\prime}_{1},\ldots,Q^{\prime}_{k_{1}}$ be the cliques of type $\beta$ from $U^{\prime}_{i}$ to which $Q_{2}$ sends $R_{i-1}$-edges,  $Q^{\prime\prime}_{1},\ldots,Q^{\prime\prime}_{k_{2}}$ be the cliques of type $\beta$ from $U_{i}\setminus U^{\prime}_{i}$ to which $Q_{2}$ sends $R_{i-1}$-edges, and let  $Q^{\prime\prime\prime}_{1},\ldots,Q^{\prime\prime\prime}_{k_{3}}$ be the cliques of type $\beta$ from $U^{\prime}_{i}$ to which $Q_{1}$ sends $R_{i-1}$-edges, but $Q_{2}$ does not. Note that, by transitivity of $R_{i-1}$, $Q_{1}$ sends $R_{i-1}$-edges to all of the $Q^{\prime}_{i}$ and all of the $Q^{\prime\prime}_{i}$. If $k_{1}+k_{2}+k_{3}\geq M_{\varphi}$ then $Q_{1}$ must send, by our construction, an $R_{i}$-edge to every clique of type $\beta$ from $U^{\prime}_{i}$, in particular to $Q_{3}$; contradiction. Thus $k_{1}+k_{2}+k_{3}<M_{\varphi}$ and $Q_{1}$ sends at least $k_{2}$ $R_{i}$-edges to cliques of type $\beta$ from $U^{\prime}_{i}$ to which it does not sent $R_{i-1}$-edges. $Q_{2}$ sends precisely $k_{2}$ such edges. Thus, since our strategy of choosing always cliques of type $\beta$ with minimal possible numbers in the numbering we have fixed requires $Q_{2}$ to send an $R_{i}$-edge to $Q_{3}$, the same strategy requires $Q_{1}$ also to to send an $R_{i}$-edge to $Q_{3}$. Contradiction.

Claim 2: The $M_{\varphi}$-profile of every clique in ${\mathfrak{A}}_{i}$ is the same as its $M_{\varphi}$-profile in ${\mathfrak{A}}$.* Again we work by induction. Assume that the $M_{\varphi}$-profiles of the surviving cliques in ${\mathfrak{A}}_{i-1}$ are the same as in ${\mathfrak{A}}$. We show that the $M_{\varphi}$-profiles of cliques surviving in ${\mathfrak{A}}_{i}$ are the same as in ${\mathfrak{A}}_{i-1}$. It is obvious for the $\mathcal{H}$-components and the values of irref, as we do not change the cliques. The $\mathcal{A}$-components for the cliques from $U^{\prime}_{0}\ldots U^{\prime}_{i}$ cannot change since they send $R_{i}$-edges to precisely the same cliques they send $R_{i-1}$-edges. Similarly, the $\mathcal{B}$-components for the cliques from $U_{i+1}\ldots U_{d}$ cannot change since they receive $R_{i}$-edges precisely from the same cliques they receive $R_{i-1}$-edges.*

Consider a clique $Q$ from $U^{\prime}_{0}\ldots U^{\prime}_{i-1}$. Note that $prof^{M_{\varphi}}_{{\mathfrak{A}}_{i}}(Q).\mathcal{B}\subseteq prof^{M_{\varphi}}_{{\mathfrak{A}}_{i-1}}(Q).\mathcal{B}$ since any $R_{i}$-edge received by $Q$ is also an $R_{i-1}$-edge. To see that $\supseteq$ also holds take any 1-type $\alpha\in prof^{M_{\varphi}}_{{\mathfrak{A}}_{i-1}}(Q).\mathcal{B}$. Then there exists a clique $Q^{\prime}$ containing a realization of $\alpha$ such that $Q^{\prime}$ sends an $R_{i-1}$-edge to $Q$. If $Q^{\prime}$ survives in ${\mathfrak{A}}_{i}$ then it sends an $R_{i}$-edge to $Q$. Otherwise $Q^{\prime}\subseteq U_{i}\setminus U^{\prime}_{i}$ and there is a clique $Q^{\prime\prime}$ of the same clique-type as $Q^{\prime}$ in $U^{\prime}_{i}$. This equality of the clique-types implies that $\alpha$ is realized in $Q^{\prime\prime}$ and $Q^{\prime\prime}$ sends an $R_{i}$-edge to $Q$. It follows that $\alpha\in prof^{M_{\varphi}}_{{\mathfrak{A}}_{i}}(Q)$. Thus $prof^{M_{\varphi}}_{{\mathfrak{A}}_{i-1}}(Q)=prof^{M_{\varphi}}_{{\mathfrak{A}}_{i}}(Q)$.

Consider a clique $Q$ from $U^{\prime}_{i}$. Obviously $prof^{M_{\varphi}}_{{\mathfrak{A}}_{i-1}}(Q).\mathcal{B}\subseteq prof^{M_{\varphi}}_{{\mathfrak{A}}_{i}}(Q).\mathcal{B}$ since all the $R_{i-1}$-edges received by $Q$ remain $R_{i}$-edges. To see $\supseteq$ assume $\alpha\in prof^{M_{\varphi}}_{{\mathfrak{A}}_{i}}(Q).\mathcal{B}$ for some $1$-type $\alpha$. Then there exists a clique $Q^{\prime}$ containing a realization of $\alpha$ such that $Q^{\prime}$ sends an $R_{i}$-edge to $Q$. If $Q^{\prime}$ sends also an $R_{i-1}$-edge to $Q$ then $\alpha\in prof^{M_{\varphi}}_{{\mathfrak{A}}_{i-1}}(Q).\mathcal{B}$. Otherwise, by our construction, $Q^{\prime}$ sends an $R_{i-1}$-edge to a clique $Q^{\prime\prime}\subseteq U_{i}\setminus U^{\prime}_{i}$ such that the clique-types of $Q$ and $Q^{\prime\prime}$ are equal. But then $\alpha$ belongs to the $\mathcal{B}$-component of the clique-type of $Q^{\prime\prime}$ and also of $Q$. So, $\alpha\in prof^{M_{\varphi}}_{{\mathfrak{A}}_{i-1}}(Q).\mathcal{B}$. It follows that $prof^{M_{\varphi}}_{{\mathfrak{A}}_{i-1}}(Q).\mathcal{B}=prof^{M_{\varphi}}_{{\mathfrak{A}}_{i}}(Q).\mathcal{B}$.

Finally, consider a clique $Q$ from $U_{i+1}\cup\ldots\cup U_{d}$. It remains to show that $prof^{M_{\varphi}}_{{\mathfrak{A}}_{i-1}}(Q).\mathcal{A}=prof^{M_{\varphi}}_{{\mathfrak{A}}_{i}}(Q).\mathcal{A}$. By our construction, the $R_{i}$-edges sent by $Q$ to $U^{\prime}_{0}\cup\ldots\cup U^{\prime}_{i-1}\cup U_{i+1}\cup\ldots\cup U_{d}$ are the same as $R_{i-1}$-edges sent by $Q$ to this set. The desired equality of the $\mathcal{A}$-components (as multisets) follows now easily from the fact that, for any clique-type $\beta$, whenever $Q$ sends precisely $k$ $R_{i-1}$-edges to cliques of $U_{i}$ of type $\beta$ then it sends precisely $k^{\prime}$-edges to cliques of $U^{\prime}_{i}$ of type $\beta$, where $k^{\prime}=min(k,M_{\varphi})$. This finishes the proof of Claim 2.

The two above claims and Lemma 4.27 imply that ${\mathfrak{A}}^{\prime}={\mathfrak{A}}_{d}$ is indeed a model of $\varphi$. As each of the $U_{i}^{\prime}$ contains a finite number of cliques and each of the cliques is finite, we get that ${\mathfrak{A}}^{\prime}$ is finite. This finishes the proof of Lemma 4.28.

Let us estimate the size of the constructed finite model ${\mathfrak{A}}^{\prime}$. For $U^{\prime}_{0}$ we take at most $M_{\varphi}$ realizations of every clique type from $U_{0}$. $M_{\varphi}$ is bounded exponentially, and the number of possible clique types in $U_{0}$ is bounded doubly exponentially in $|\varphi|$ (note that such cliques do not send any edges). Then, to construct $U^{\prime}_{i}$ we consider clique types distinguished, in particular, by the sets of cliques from $U^{\prime}_{0}\cup\ldots U^{\prime}_{i-1}$ to which a given clique sends edges. Thus, the number of cliques in $U^{\prime}_{i}$ may become exponentially larger than the number of cliques in $U^{\prime}_{i-1}$. Thus, we can only estimate the number of cliques in our eventual finite model by a tower of exponents of height $d$ (recall that our bound on $d$ is exponential in $|\varphi|$, though a polynomial bound would not be difficult to obtain). We leave open the question if a construction building smaller (e.g., doubly exponential in $|\varphi|$) models exist.

A careful inspection shows that all our constructions respect reflexivity and seriality, that is, if we replace the word transitive in the statements of Lemma 4.25 and Lemma 4.28 with the phrases reflexive transitive or serial transitive then they remain correct.

Theorem 4.30**.**

The logics \mbox{\rm K4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), \mbox{\rm D4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), \mbox{\rm S4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) have the finite model property. Their local and global satisfiability problems are decidable.

A natural decision procedure arising from our work is as follows: guess a finite model of the given formula and check that it indeed is a model. However, this procedure does not give a good upper complexity bound, since it needs to take into account very large finite models. The precise complexity can be established using the above-mentioned results from [Gogacz et al. (2019)] concerning the description logic $\mathcal{SIQ}^{-}$.

Theorem 4.31**.**

The local and global satisfiability problems for the logics \mbox{\rm K4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), \mbox{\rm D4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), \mbox{\rm S4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) are 2-ExpTime-complete.

Proof 4.32**.**

In [Gogacz et al. (2019)] it is shown that the knowledge base satisfiability problem for the logic $\mathcal{SIQ}^{-}$, restricted to a single transitive role, is 2-ExpTime-complete. With this single role restriction, the language of $\mathcal{SIQ}^{-}$ becomes a syntactic variant of K4 (\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}). The knowledge base satisfiability in $\mathcal{SIQ}^{-}$ is the question if for a given pair $(\mathcal{T},\mathcal{A})$, where $\mathcal{T}$ is a TBox and $\mathcal{A}$ is an ABox, there exists a structure containing $\mathcal{A}$ and respecting $\mathcal{T}$ at every element. We do not want to define these notions formally here and refer the interested reader to [Gogacz et al. (2019)] or some other articles on description logics. For our purposes it is sufficient to say that $\mathcal{T}$ consists of implications of the form $\phi\rightarrow\psi$ and $\mathcal{A}$ is a collection of assertions of the form $\phi(a)$ or $T(a,b)$ where $a,b$ are names for domain elements (which can be used only in $\mathcal{A}$), $\phi(a)$ means that $\phi$ is satisfied at $a$, and $T(a,b)$ means that there is an edge from $a$ to $b$.

To solve global satisfiability for \mbox{\rm K4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) we just translate the input formula $\phi$ to the knowledge base $(\{\top\rightarrow\phi\},\emptyset)$ and ask for its satisfiability. Regarding the lower bound, we can easily adapt the lower bound proof from [Gogacz et al. (2019)] (Theorem 4) to our scenario. The proof there goes by a reduction from the acceptance problem for alternating Turing machines with exponentially bounded space, and uses both TBoxes and ABoxes. However, ABoxes are always of a simple form $\phi^{\prime}(a)$. What we can do is to take the conjunction $\phi$ of the K4-counterparts of the implications from the given TBox and ask for combined satisfiability of $\phi$ and $\phi^{\prime}$. This gives the $2\textsc{-ExpTime}$-lower bound for the combined complexity of \mbox{\rm K4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}). Due to Lemma 4.22 we infer 2-ExpTime-completeness of local and global satisfiability in \mbox{\rm K4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}).

The upper and lower complexity bounds for \mbox{\rm K4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) and \mbox{\rm S4}(\Diamond_{\geq},\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) can be obtained by an inspection of the proofs from [Gogacz et al. (2019)] and observing that they work for structures with a reflexive or serial transitive relation.

5 Missing lower bounds for logics with converse and without graded modalities

To complete the picture we consider in this section the modal language with converse but without graded modalities. Over most relevant classes of frames tight complexity bounds for local and global satisfiability of this language are known. However, according to Zolin’s survey [Zolin (2017)], the three logics of transitive frames K4 (\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), S4 (\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) and D4 (\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) whose global satisfiability is known to be in ExpTime lack the corresponding lower bound. We provide it here. We were also not able to find a tight lower bound in the literature for the logics of Euclidean frames, K5 (\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), D5 (\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}). We also show it here. Interestingly, the two reductions are identical, i.e., in both cases we produce the same formulas (but the shapes of the intended models differ).

In the conference version of this paper we used a rather heavy reductions from the halting problem for alternating Turing machines working in polynomial space. Following the suggestion of one of the referees we looked for an alternative proof by a reduction from global satisfiability of the logic $\mbox{\rm K}(\Diamond)$. The general idea is essentially the same as in our previous proof but the reduction is arguably simpler.

Theorem 5.33**.**

The global satisfiability problem for \mbox{\rm K4}(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), \mbox{\rm D4}(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) and \mbox{\rm S4}(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) is ExpTime-hard.

Proof 5.34**.**

We recall that global satisfiability problem for $\mbox{\rm K}(\Diamond)$ is ExpTime-hard. We reduce this problem simultaneously to global satisfiability of the three logics we consider.

Take any modal formula $\varphi$ of $\mbox{\rm K}(\Diamond)$. Without loss of generality we assume that $\varphi$ contains no nested occurrences of $\Diamond$ and $\Box$. (Indeed, if $\varphi$ contains a nested occurrence of a modal operator, that is it contains a subformula $\Diamond\psi$ or $\Box\psi$ in the scope of another $\Diamond$ or $\Box$, then we replace that subformula by a fresh variable $p$ and append the conjunct $p\leftrightarrow\Diamond\psi$, resp., $p\leftrightarrow\Diamond\psi$. Successively treating in this way all occurrences of modal operators we eventually end up with a formula equisatisfiable to $\varphi$ in which they are not nested.)

Assuming that $c_{0},c_{1},c_{2}$ and $c_{3}$ are fresh propositional variables not occurring in $\varphi$ we define the translation $\mathbf{tr}(\varphi)$ as follows:

• •

$\mathbf{tr}(p)=p$* for all propositional variables $p$,*

• •

$\mathbf{tr}(\varphi^{\prime}\lor\varphi^{\prime\prime})=\mathbf{tr}(\varphi^{\prime})\lor\mathbf{tr}(\varphi^{\prime\prime})$* and analogously for $\lor,\rightarrow,\leftrightarrow$,*

• •

$\mathbf{tr}(\neg\varphi^{\prime})=\neg\mathbf{tr}(\varphi^{\prime})$,

• •

\mathbf{tr}(\Diamond\varphi^{\prime})=[c_{0}\rightarrow\Diamond(c_{1}\land\mathbf{tr}(\varphi^{\prime}))]\land[c_{1}\rightarrow\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}(c_{2}\land\mathbf{tr}(\varphi^{\prime}))]\land[c_{2}\rightarrow\Diamond(c_{3}\land\mathbf{tr}(\varphi^{\prime}))]\land[c_{3}\rightarrow\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}(c_{0}\land\mathbf{tr}(\varphi^{\prime}))]* and analogously for $\Box\varphi^{\prime}$*

Let $\varphi^{*}=\mathbf{tr}(\varphi)\land(\bigvee_{0\leq i\leq 3}c_{i})\land(\bigwedge_{0\leq i<j\leq 3}(\neg c_{i}\vee\neg c_{j}))$. Note that $\varphi^{*}$ is composed of the translated $\varphi$ and a formula stipulating that for each node exactly one of $c_{i}$ holds true. The size of $\varphi^{*}$ is clearly polynomial in $|\varphi|$ since $\Diamond$ and $\Box$ have no nested occurrences in $\varphi$.

Claim 1

If $\varphi$ is globally satisfiable in $\mbox{\rm K}(\Diamond)$ then $\varphi^{*}$ is globally satisfiable in \mbox{\rm K4}(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), \mbox{\rm D4}(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) and \mbox{\rm S4}(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}).

Proof 5.35**.**

Let ${\mathfrak{A}}=\langle W,R,V\rangle$ be a model of $\varphi$. We assume that ${\mathfrak{A}}$ is tree-shaped (this is done without loss of generality since $\mbox{\rm K}(\Diamond)$ has the tree-shaped model property). Let $w_{r}$ denotes the root of ${\mathfrak{A}}$.

For any world $w$ define its distance from the root, denoted with $d(w)$, as the length of the $R$-path from $w_{r}$, i.e., $d(w_{r})=0$, $d(w)=1$ iff $R(w_{r},w)$ holds, $d(w)=2$ iff there is a world $v$ such that $R(w_{r},v),R(v,w)$ etc. We define the Kripke structure ${\mathfrak{A}}^{\prime}=(W^{\prime},R^{\prime},V^{\prime})$ by inverting every second $R$-edge of ${\mathfrak{A}}$ and labelling the worlds on every path, leading from the root, repetitively $c_{0},c_{1},c_{2},c_{3},c_{0},\ldots$. Formally:

• •

$W=W^{\prime}$,

• •

For every propositional variable $p\not\in\{c_{0},c_{1},c_{2},c_{3}\}$ we set $V^{\prime}(p)=V(p)$ while for the variables $c_{i}$ we set $V^{\prime}(c_{i})=\{w:d(w)\;\mathop{mod}\;4=i\}$ for $i\in\{0,1,2,3\}$,

• •

$R^{\prime}$* is the reflexive closure of $R_{(0,1)}\cup R_{(1,2)}^{-1}\cup R_{(2,3)}\cup R_{(3,0)}^{-1}$, with $R_{(i,j)}=R\cap V^{\prime}(c_{i})\times V^{\prime}(c_{j})$.*

The shape of the obtained model is illustrated in Fig. 4.

Now we show that $\varphi^{*}$ is globally satisfiable in \mbox{\rm K4}(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), \mbox{\rm D4}(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) and \mbox{\rm S4}(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}). First, note that due to the construction $R^{\prime}$ is transitive and reflexive (and thus also serial). Next, note that the second part of the formula $\varphi^{*}$ is globally satisfied in ${\mathfrak{A}}^{\prime}$, since every world belongs to exactly one of $V^{\prime}(c_{i})$ (due to the fact that the satisfaction of $c_{i}$ depends on a distance from the root, which is unique since ${\mathfrak{A}}$ is assumed to be tree-shaped). Finally, we show that ${\mathfrak{A}}^{\prime}\models\mathbf{tr}(\varphi)$. The proof is by induction, where the inductive hypothesis states that for any subformula $\psi$ of $\varphi$ and every world $w$ we have ${\mathfrak{A}},w\models\psi$ if and only if ${\mathfrak{A}}^{\prime},w\models\mathbf{tr}(\psi)$. The case of $\psi$ being a propositional variable follows from the second item of definition of ${\mathfrak{A}}^{\prime}$. The case when $\psi$ is a Boolean combination of formulas is immediate from the inductive hypothesis and the semantics of $\models$. Hence, the only interesting case is when $\psi$ is of the form $\Diamond(\psi^{\prime})$. We prove only one implication; the second one is analogous. Assume that ${\mathfrak{A}},w\models\Diamond(\psi^{\prime})$. Thus there is a world $v$ such that $R(w,v)$ and ${\mathfrak{A}},v\models\psi^{\prime}$. By induction hypothesis we deduce that ${\mathfrak{A}}^{\prime},v\models\mathbf{tr}(\psi^{\prime})$. Moreover, for $i=d(w)\;\mathop{mod}\;4$ and $j=d(v)\;\mathop{mod}\;4=(i+1)\;\mathop{mod}\;4$ we have ${\mathfrak{A}}^{\prime},w\models c_{i}$ and ${\mathfrak{A}}^{\prime},v\models c_{j}$. Moreover, if $i$ is even then $(w,v)\in R^{\prime}$ and $(v,w)\in R^{\prime}$ otherwise. In each of the cases $i\in\{0,1,2,3\}$ these all imply that ${\mathfrak{A}}^{\prime},w\models\mathbf{tr}(\psi)$, which finishes the proof.

Claim 2

If $\varphi^{*}$ is globally satisfiable in \mbox{\rm K4}(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}), \mbox{\rm D4}(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) or \mbox{\rm S4}(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) then $\varphi$ is globally satisfiable in $\mbox{\rm K}(\Diamond)$.

Proof 5.36**.**

Let ${\mathfrak{A}}=\langle W,R,V\rangle$ be a model of $\varphi^{*}$. We will define an increasing chain of structures ${\mathfrak{A}}^{\prime}_{0}$, ${\mathfrak{A}}^{\prime}_{1}$, $\ldots$, in which ${\mathfrak{A}}_{i}^{\prime}=\langle W^{\prime}_{i},R^{\prime}_{i},V^{\prime}_{i}\rangle$, together with a pattern function $f:A_{0}\cup A_{1}\cup\ldots\rightarrow W$. The Kripke structure ${\mathfrak{A}}^{\prime}=\langle W^{\prime},R^{\prime},V^{\prime}\rangle$ defined as the union of the chain will turn out to be a model of $\varphi$. Our chain of structures is defined as follows.

We fix a world $w\in W$, set ${\mathfrak{A}}_{0}^{\prime}=\langle\{w^{\prime}\},\emptyset,V_{0}^{\prime}\rangle$ with $V_{0}^{\prime}(w^{\prime})=V(w)$ and set $f(w^{\prime})=w$. For simplicity let us assume that ${\mathfrak{A}},w\models c_{0}$. In our construction, for every element $w^{\prime}$ freshly added to ${\mathfrak{A}}^{\prime}_{i}$, we will have that $f(w^{\prime})$ satisfy $c_{i\mod 4}$.

Assume now that ${\mathfrak{A}}^{\prime}_{i}$ is defined. To construct ${\mathfrak{A}}^{\prime}_{i+1}$ we repeat for every element $w^{\prime}$ freshly added to ${\mathfrak{A}}^{\prime}_{i}$: if $i$ is even (odd) then for every $R$-successor ($R$-predecessor) $v$ of $f(w^{\prime})$ in ${\mathfrak{A}}$ such that ${\mathfrak{A}},v\models c_{i+1\mod 4}$ add to $W_{i+1}$ a fresh $R$-successor $v^{\prime}$ of $w^{\prime}$ and let $V^{\prime}_{i}(v^{\prime})=V(v)$ and $f(v^{\prime})=v$.

We prove inductively over the shape of $\psi$ that ${\mathfrak{A}}^{\prime},w^{\prime}\models\psi$ iff ${\mathfrak{A}},f(w^{\prime})\models\mathbf{tr}(\psi)$. The case of atomic propositions and Boolean combinations follows immediately from the definition. The only interesting case is of $\psi=\Diamond(\psi^{\prime})$. Here we show only one case of one implication; the other cases are analogous. Assume that ${\mathfrak{A}},f(w^{\prime})\models\mathbf{tr}(\psi)$ holds as well as $f(w^{\prime})\models c_{0}$. Then there is an $R$-successor $v$ of $f(w^{\prime})$ satisfying $\mathbf{tr}(\psi^{\prime})\land c_{1}$. Note that the $R^{\prime}$-successors of $w^{\prime}$ are copies of $R$–successors of $f(w^{\prime})$ satisfying $c_{1}$, thus there is a world $v^{\prime}$ being an $R^{\prime}$-successor of $f(w^{\prime})$ and satisfying $f(v^{\prime})=v$. Hence, from the inductive assumption, we infer ${\mathfrak{A}}^{\prime},v^{\prime}\models\psi^{\prime}$, which implies ${\mathfrak{A}}^{\prime},w^{\prime}\models\psi$. Analyzing analogously the other cases we finish the inductive proof of the claim.

The two proceeding claims show the correctness of the translation, allowing us to conclude Theorem 5.33.

We next handle the case of Euclidean frames.

Theorem 5.37**.**

The global and local satisfiability problem for K5(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) and D5 (\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}) is ExpTime-hard.

Proof 5.38**.**

We explicitly consider the global satisfiability problem, but due to Lemma 3.9 our proof applies also to local satisfiability. The proof goes as the proof of Theorem 5.33. Our current intended models are similar to the intended models there (as on Fig. 4). The difference is that all the worlds satisfying $c_{1}$ or $c_{3}$ are made equivalent to each other, and the worlds satisfying $c_{0}$ or $c_{2}$ are irreflexive. Note that this does not violate the property that each world can identify its children in the tree. Observe also that such intended models are indeed Euclidean and serial (however, they are neither transitive nor reflexive); in particular all worlds satisfying $c_{0}$ or $c_{2}$ are lanterns. Now, for a given K formula we can construct precisely the same formula as in the previous proof. We leave the routine details to the reader. The correctness proof is essentially identical to the correctness proof of Theorem 5.33 so we omit it here.

6 Conclusions

We have filled the gaps remaining in the classification of the complexity of the local and global satisfiability problems for natural modal languages with graded and converse modalities over traditional classes of frames. What we have not systematically studied are the problem of combined satisfiability (given two formulas check if there exists a model in which the first is satisfied locally and the second is satisfied globally) and the problem of finite (local, global, combined) satisfiability (asking about the existence of finite models). We suspect that the classification could be extended to cover these problems using results/techniques from our paper and the referenced articles without major obstacles.

Two other questions we leave open are if the NExpTime-lower bound in Thm. 3.16 remains valid if the numbers in graded modalities are encoded in unary rather than in binary and if our finite model construction from Section 4 can be replaced by a one producing smaller models.

Acknowledgements

We thank Evgeny Zolin for providing us a comprehensive list of gaps in the classification of the complexity of graded modal logics and for sharing with us his tikz files with modal cubes. We thank Emil Jeřábek for his explanations concerning K5(\Diamond,\ensurestackMath{\stackengine{.5pt}{\Diamond}{\scalebox{0.75}[1.0]{-}}{O}{c}{F}{F}{L}}). We also thank Tomasz Gogacz and Filip Murlak for comments concerning Section 4. Finally, we thank the anonymous reviewers for their useful comments and remarks.

Bartosz Bednarczyk is supported by Polish Ministry of Science and Higher Education program ”Diamentowy Grant” no. DI2017 006447.

Emanuel Kieroński and Piotr Witkowski are supported by Polish National Science Centre grant no. 2016/21/B/ST6/01444.