Complexity of modal logic IK5

Question

What is the complexity of local satisfiability problem for modal logic $\mathit{IK5}$? Herein we denote by $IK5$ the modal logic over euclidean frames extended with inverse modality. Could you provide any references? Is it in $NP$?

What I know about the topic?

It's easy to see that $IK5$ is in $ExpTime$, since there is a reduction from it to $GF^2$ (the two-variable guarded fragment of first-order logic) - see Deciding Regular Grammar Logics with Converse Through First-Order Logic.

On the other hand, the ordinary $K5$ is $NP$-complete.

We can write an equisatisfiable formula in $FO^1$ (the one-variable fragment of first-order logic), because the models can be devided into three parts: (1) starting world $w$, (2) sucessors of $w$ (3) sucessors of sucessors of $w$. The example reduction for even harder logic ($K5$ with graded modalities) is described in A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics. However in the presence of inverse modality we cannot do the same trick - the brief idea is that inverse worlds could require the different number of successors.

Answer 1

The logic is EXP-complete. One way to prove the lower bound is to note that the logic KTB augmented with universal modality, or even just the global consequence relation of KTB, is EXP-complete (Chen and Lin [1]; note that they denote KTB as B).

Note that a connected IK5-frame $(W,R,R^{-1})$ is either a single irreflexive point, or it consists of a reflexive cluster $C$ together with a (possibly empty) set $I$ of irreflexive points, each of which sees (in $R$) a nonempty subset of $C$. Thus, $$R_s:=\{(x,y)\in C^2:\exists z\in I\,(R(z,x)\land R(z,y))\}$$ is a symmetric relation on $C$; if every element of $C$ is seen by an element of $I$, $R_s$ is also reflexive. Conversely, it is easy to see that every reflexive symmetric frame can be obtained in this way. It follows that

$${}\vdash_{\mathrm{KTB}^U}\phi\iff{}\vdash_{\mathrm{IK5}}\Diamond^-\top\land\Box^+\Diamond^-\Box^-\bot\to\phi^*,$$

where the translation $\phi^*$ commutes with propositional connectives, and is defined for modal operators by

\begin{align*} (\Box\phi)^*&=\Box^-(\Box^-\bot\to\Box^+\phi^*),\\ (A\phi)^*&=\Box^+\phi^*. \end{align*}

Here, $A$ denotes the universal modality of $\mathrm{KTB}^U$, and $\Box^+$ and $\Box^-$ respectively denote the forward and backward modalities of IK5.

Reference:

[1] Cheng-Chia Chen and I-Peng Lin, The complexity of propositional modal theories and the complexity of consistency of propositional modal theories, in: Proc. LFCS 1994 (Anil Nerode and Yu. V. Matiyasevich, eds.), LNCS 813, Springer, pp. 69–80, doi 10.1007/3-540-58140-5_8.