Hennessy-Milner Type Theorems for Fuzzy Multimodal Logics Over Heyting Algebras

TL;DR

This paper extends Hennessy-Milner theorems to fuzzy multimodal logics over Heyting algebras, establishing conditions under which various bisimulations coincide with modal equivalence in fuzzy Kripke models.

Contribution

It introduces the concept of weak bisimulation for fuzzy multimodal logics and proves Hennessy-Milner type theorems relating weak bisimulation to existing bisimulation notions.

Findings

Weak bisimulation coincides with forward bisimulation in image-finite models.

Weak bisimulation coincides with backward bisimulation in domain-finite models.

Weak bisimulation coincides with regular bisimulation in degree-finite models.

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 $\Psi $ 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 $\Psi $ 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 $\Psi$. 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.