Hennessy-Milner Type Theorems for Fuzzy Multimodal Logics Over Heyting Algebras
Marko Stanković, Miroslav Ćirić and Jelena Ignjatović
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 𝑤 and 𝑤’, that is, to express the degree of modal equivalence between worlds 𝑤 and 𝑤’ 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.
Keywords: Fuzzy bisimulation, fuzzy Kripke model, fuzzy multimodal logic, Hennessy-Milner property, weak bisimulation, weak simulation