Research On Approximate Bisimulations For Fuzzy Transition Systems

Modal logics and behavioral equivalences play an important role in the specification and verification of concurrent systems.The former can be used for model checking,particularly for specifying the properties to be verified.The latter can be used for state-aggregation algorithms that compress model by merging bisimilar states but guarantee that the required properties are preserved.Bisimulation is a well-known behavioral equivalence for discrete event systems and have been widely used in many areas of computer science,in particular,in verification where they are crucial to reduce the state space of the system under consideration.Recently,bisimulations have been investigated in fuzzy systems and have been developed quickly.A central question regarding any notion of bisimulation is its distinguishing power.In order to compare the behavior of systems better,researchers proposed approximate bisimulations.However,these bisimulations and approximate bisimulations are invalid in some cases,for example,they are invalid in comparing the behavior of two states of quantitative fuzzy transition systems or some nondeterministic fuzzy transiton systems.To introduce approximate bisimulations to quantitative fuzzy transition systems and nondeterministic fuzzy transiton systems,this dissertation proposes limited approximate bisimulations for labeled fuzzy transition systems,approximate bisimulations and limited bisimulations for nondeterministic fuzzy transition systems,to measure the similarity of states or systems.We provide the fixed-point,algorithmic and logical characterization of approximate bisimulations and limited bisimulations.We investigate the relationships between rough approximations based on cirsp binary relation induced by underlying labeled fuzzy relation and rough approxmations based on limited approximate bisimilarity.The main innovative work of the dissertation includes the following three aspects:(1)Limited approximate bisimulations for quantitative fuzzy transition systems and the corresponding rough approximations.The notion of quantitative fuzzy transition systems is proposed,whose labels are equipped with a residuated lattice-valued equality relation and is an extension of labeled transition systems.In a quantitative fuzzy transition system,we define a new notion of limited approximate similarity,to quantify to what extent one state is simulated by another in the neighboring subgraphs,and provide its properties.Based on the new notion,we give a definition of limited approximate simulation and discuss its properties.Then we introduce an ordered pair of relations,one on the state(vertex)set(limited approximate simulation)and one on the edge(transition)set induced by the relation on state set,called VE limited approximate simulation in the dissertation.We also present a new notion of limited approximate bisimilarity in a quantitative fuzzy transition system,to quantify to what extent two states are similar in the neighbouring subgraphs,and give its properties.One main contribution of the dissertation is to give a condition for two states to be limited approximate bisimilar and investigate the degree of similarity between two states.We discuss the relationships between the rough approximations based on the underlying crisp relation induced by underlying labeled fuzzy relation and the rough approximations based on limited approximate bisimilarity.(2)Approximate bisimulations for nondeterministic fuzzy transition systems.We first realize the relational lifting through a function S induced by residuums(implications)in complete residuated lattices rather than weight functions the previous researchers used,which relaxes the conditions of lifting relation by using weight functions.Some properties of the lifting operation are presented.Based on the lifting operation,we define a notion of ?-bisimulation under (?) for nondeterministic fuzzy transition systems,where ??[0,1].It is much more natural and robust than some behavioral measures,and can measure the degree of similarity between the two states which are deemed to be equivalent intuitively but simply distinguished by other bisimulations.Then we provide some properties of ?-bisimulation underS.We also address the parallel composition operator of nondeterministic fuzzy transition systems and show that ?-bisimilarity under (?) is nonexpansive with respect to the operator,which makes compositional verification possible.In addition,we give a fixedpoint characterization of ?-bisimulation under (?) and compute ?-bisimilarity under (?).Then real-valued logic is introduced to characterize ?-bisimilarity under (?).(3)Limited bisimulations for nondeterministic fuzzy transition systems.We extend the notion of limited approximate bisimilarity to nondeterministic fuzzy transition systems.We define the notion of k-limited ?-bisimilarity by using an approach of relational lifting,where k is a natural number and ??[0,1].It can measure the degree of similarity between two states in the neighbouring subgraphs.Then we provide some properties of it.The relationships between k-limited ?-bisimilarity and ?-bisimilarity under lifting function S are also presented.Based on k-limited ?-bisimilarity,k-limited ?-bisimulation is defined,and then we give a fixed point characterization of k-limited ?-bisimilarity.We also provide some necessary and sufficient conditions for two states in an nondeterministic fuzzy transition systems to be k-limited ?-bisimilar,and an algorithm for computing the greatest ? such that the two given states are k-limited?-bisimilar.Based on the relationships between k-limited ?-bisimilarity and?-bisimilarity under (?),a logical characterization of k-limited ?-bisimilarity is provided.