Simulations and bisimulations for fuzzy multimodal logics over Heyting algebras

In the present paper, we study fuzzy multimodal logics over complete Heyting algebras and Kripke models for these logics. We introduce two types of simulations (forward and backward) and five types of bisimulations (forward, backward, forward-backward, backward-forward and regular) between Kripke models, as well as the corresponding presimulations and prebisimulations, which are simulations and bisim-ulations with relaxed conditions. For each type of simulations and bisimulations an efficient algorithm has been provided that works as follows: it computes the greatest presimulation/prebisimulation of that type, and then checks whether it meets the additional condition: if it does, then it is also the greatest sim-ulation/bisimulation of that type, otherwise, there is not any simulation/bisimulation of that type. The algorithms are inspired by algorithms for checking the existence and computing the greatest simulations and bisimulations between fuzzy automata. We also demonstrate the application of these algorithms in the state reduction of Kripke models. We show that forward bisimulation fuzzy equivalences on the Kripke model provide reduced models equivalent to the original model concerning plus-formulas, backward bisim-ulation fuzzy equivalences provide reduced models equivalent concerning minus-formulas, while regular bisimulation fuzzy equivalences provide reduced models equivalent concerning all modal formulas.