The Study Of Approximate Safety And Liveness Properties In Branching Time

Formal methods refer to techniques that rely on strict mathematical foundations to formalize,develop,and verify software and hardware systems.Formal specification,as the basis of formal method,strictly describes the model of the developed system and its properties through formal language,including model specification and property specification.The property specifications are divided into linear-time specifications and branching-time specifications.As the basic property of these two property specifications,safety and liveness have been extensively studied.As the system becomes larger and more complex,it will inevitably face the processing of uncertain or inconsistent information.Adding fuzzy theory to the classic formal specification is an effective quantitative method,which can accurately describe the behavior of such systems.The branching-time specification in the property specification plays a very important role in system verification.There is no corresponding formal definition for extending the branching-time property to fuzzy systems.At the same time,the quantitative expansion of safety and liveness will provide a theory for the verification of such systems.In this paper,based on Fuzzy Kripke and fuzzy transition system,we extend safety and liveness,and study some properties of them.The main work is as follows.1.Based on fuzzy Kripke structure,a formal definition of branching-time properties,especially the safety and liveness properties,in the fuzzy setting,is given.At the same time,two types of closure operations are defined,resulting in four types of properties: universal safety,universal liveness,existential safety,and existential liveness.Finally,we show that any branching-time property is the intersection of an existential safety property and an existential liveness property,a universal safety property and a universal liveness property or an existential safety property and a universal liveness property.2.Based on the fuzzy transition system,the classic safety and liveness are quantitatively expanded,?-safety and ?-liveness are defined,and two prefixes and closure operations for ?-safety and ?-liveness are given.The theorem of how to determine whether a property is ?-safety and ?-activity is proved.Finally,the decomposition result of decomposing a property into ?-safety and ?-liveness is given.