Hennessy-Milner Type Theorems for Fuzzy Multimodal Logics Over Heyting Algebras
Marko Stanković, Miroslav Ćirić, Jelena Ignjatović
TL;DR
This work develops Hennessy–Milner type theorems for fuzzy multimodal logics over linearly ordered Heyting algebras by introducing weak bisimulations for a chosen set of formulae and linking them to forward, backward, and regular bisimulations under image-, domain-, and degree-finiteness constraints. It shows that modal equivalence with respect to plus-, minus-, or all formulae can be captured by computing the greatest forward, backward, or regular bisimulations, respectively, thereby enabling more efficient modal-equivalence checks in fuzzy Kripke models. The framework unifies fuzzy Kripke semantics with weak simulations and duality principles, offers reformulations for propositional modal logics, and discusses practical applications to fuzzy description logics and social-network analysis, supported by computational examples. Collectively, the results provide a principled, computable bridge between modal equivalence on fuzzy structures and standard bisimulation notions, with broad implications for reasoning in fuzzy DLs and related systems.
Abstract
In a recent paper, we have introduced two types of fuzzy simulations (forward and backward) and five types of fuzzy bisimulations (forward, backward, forward-backward, backward-forward and regular) between Kripke models for the fuzzy multimodal logics over a complete linearly ordered Heyting algebra. In this paper, for a given non-empty set $Ψ$ of modal formulae, we introduce the concept of a weak bisimulation between Kripke models. This concept can be used to express the degree of equality of fuzzy sets of formulae from $Ψ$ that are valid in two worlds $w$ and $w'$, that is, to express the degree of modal equivalence between worlds $w$ and $w'$ with respect to the formulae from $Ψ$. We prove several Hennessy-Milner type theorems. The first theorem determines that the greatest weak bisimulation for the set of plus-formulae between image-finite Kripke models coincides with the greatest forward bisimulation. The second theorem determines that the greatest weak bisimulation for the set of minus-formulae between domain-finite Kripke models coincides with the greatest backward bisimulation. Finally, the third theorem determines that the greatest weak bisimulation for the set of all modal formulae between the degree-finite Kripke models coincides with the greatest regular bisimulation.