Algorithmic and logical characterizations of bisimulations for non-deterministic fuzzy transition systems

Bisimulation is a well-known behavioral equivalence for discrete event systems and has been developed in fuzzy systems quickly. In this paper, we adopt an approach of the relational lifting that is one of the most used methods in the field of bisimulation research, to define it for a non-deterministic fuzzy transition system. An O(|S|4|→|2) algorithm is given for testing bisimulation where |S| is the number of states and |→| the number of transitions in the underlying transition systems. Two different modal logics are presented. One is two-valued and indicates whether a state satisfies a formula, which is an extension of Hennessy-Milner logic. The other is real-valued and shows to what extent a state satisfies a formula. They both characterize bisimilarity soundly and completely. Interestingly, the second characterization holds under a class of fuzzy logics. In addition, this real-valued logic allows us to conveniently define a logical metric that captures the similarity between states or systems. That is, the smaller distance, the more states alike. Although the work is inspired by the corresponding work in probabilistic systems, it is obviously different. In particular, the real-valued logic in this paper remains unexplored in fuzzy systems, even in probabilistic systems.