Complexity of modal logic IK5 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.
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)^*&amp;=\Box^-(\Box^-\bot\to\Box^+\phi^*),\\
(A\phi)^*&amp;=\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.