Simulations and bisimulations for fuzzy multimodal logics over Heyting algebras

Abstract

In the present paper we study fuzzy multimodal logics over a complete Heyting algebra 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 bisimulations 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 simulation/bisimulation of that type, otherwise there is no 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 reducing the size of Kripke models. We show that forward bisimulation fuzzy equivalences on the Kripke model provide reduced models equivalent to the original model with respect to plus-formulas, backward bisimulation fuzzy equivalences provide reduced models equivalent w.r.t minus-formulas, while regular bisimulation fuzzy equivalences provide reduced models equivalent w.r.t all modal formulas.