\(\epsilon \) -Approximate Bisimulations for Nondeterministic Fuzzy Kripke Structures

Bisimulation is a famous behavioral equivalence relation for discrete event systems and has developed rapidly in model checking. Inspired by the bisimulations theory of nondeterministic fuzzy Kripke structures(NFKSs) proposed by Deng [26], in this paper, we define the concept of \(\epsilon \) -approximate bisimulations for NFKSs. Next, we introduce the notion of the set of traces. On above basis, we propose a new mapping which is used to compare the behaviors of two NFKSs under \(\epsilon \) -approximate bisimulation. Meanwhile, we investigate the property of finite paths. This property lays the groundwork for exploring the behaviors of two NFKSs under the \(\epsilon \) -approximate bisimulation. Fortunately, we demonstrate that if two NFKSs equipped with an \(\epsilon \) -approximate bisimulation between them, then their behaviors are \(\epsilon \) -approximate each other. Furthermore, we discover that there might not exist the greatest \(\epsilon \) -approximate bisimulation for a given NFKS. At last, in order to complish approximate minimization operation for a given NFKS under \(\epsilon \) -approximate bisimulation, we elaborate three algorithms to generate all maximal \(\epsilon \) -approximate bisimulations. Surprisingly, with help of the maximal \(\epsilon \) -approximate bisimulations, the quotient NFKSs obtained through the Definition 24 not only have minimum number of states, but also the behavior of quotient NFKS differs by \(\epsilon \) from the behavior of initial NFKS.