Logical characterizations of simulation and bisimulation for fuzzy transition systems

Simulations and bisimulations are known to be useful for abstracting and comparing formal systems, and they have recently been introduced into fuzzy systems. In this study, we provide sound and complete logical characterizations for simulation and bisimulation, which are defined over fuzzy labeled transition systems via two variants of the Hennessy–Milner Logic. The logic for characterizing fuzzy simulation has neither negation nor disjunction, which is very different from the well-known logical characterizations of probabilistic simulations, although the completeness proofs of our characterization results are inspired by relevant research in probabilistic concurrency theory. The logic for characterizing fuzzy bisimulation also deviates from that for probabilistic bisimulations.