摘要

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(vertical bar S vertical bar(4)vertical bar ->vertical bar(2)) algorithm is given for testing bisimulation where vertical bar S vertical bar is the number of states and vertical bar ->vertical bar 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.