On the Modal Definability of Simulability by Finite Transitive Models

Abstract

We show that given a finite, transitive and reflexive Kripke model 〈 W, ≼, ⟦ ⋅ ⟧ 〉 and ${w \in W}$ , the property of being simulated by w (i.e., lying on the image of a literalpreserving relation satisfying the ‘forth’ condition of bisimulation) is modally undefinable within the class of S4 Kripke models. Note the contrast to the fact that lying in the image of w under a bisimulation is definable in the standard modal language even over the class of K4 models, a fairly standard result for which we also provide a proof.

We then propose a minor extension of the language adding a sequent operator ${\natural}$ (‘tangle’) which can be interpreted over Kripke models as well as over topological spaces. Over finite Kripke models it indicates the existence of clusters satisfying a specified set of formulas, very similar to an operator introduced by Dawar and Otto. In the extended language ${{\sf L}^+ = {\sf L}^{\square\natural}}$ , being simulated by a point on a finite transitive Kripke model becomes definable, both over the class of (arbitrary) Kripke models and over the class of topological S4 models.

As a consequence of this we obtain the result that any class of finite, transitive models over finitely many propositional variables which is closed under simulability is also definable in L ⁺, as well as Boolean combinations of these classes. From this it follows that the μ-calculus interpreted over any such class of models is decidable.