The Study Of Fuzzy Linear-Time Properties

The formal method is a method,which is strictly based on mathematics,to specify,model,verify and analyze the software and hardware of computer systems.As one of the main content of formal methods,formal specification can specify the system and the properties that the system satisfies.As the basic properties that need to be met for a class of systems,safety and liveness property are very important to ensure system safety and reliability.As software and hardware systems become increasingly large,many quantitative behavior characteristics are designed into the systems during development,so it is not enough to accurately evaluate the behavior of system by using only qualitative techniques.By combining classical formal specification with fuzzy logic,the uncertain or inconsistent information can be effectively quantified and the fuzzy system can be characterized.In the fuzzy background,distance is used to describe linear time properties,and describe the degree of approximation(satisfaction)between the system and the properties,which can accurately reflect the level of error between behavior and given specification of system.However,there is no relevant research on this type of works.Therefore,this paper will carry out relevant work to provide solid theoretical support for the development of fuzzy model checking.The main work is as follows:1.Based on the fuzzy transition system,the safety and liveness property in linear time property are quantitatively expanded,and the good properties of traditional linear time property are retained as much as possible.Firstly,the safety property which suitable for fuzzy transition system is defined from the perspective of good prefix,which is called approximate safety property.Secondly,based on the concept of classical liveness,the definition of approximate liveness has been generalized.2.Based on Büchi automaton,the proposed approximate safety and liveness property are characterized.In addition,it is proved that the fuzzy linear time property characterized by Büchi automaton is the intersection of the languages accepted by approximate safety automaton and approximate liveness automaton.Next,the proposed theory of approximate safety and liveness property and the existing linear temporal logic under fuzzy background is extended.Then,the approximate safety and liveness property are characterized with fuzzy linear temporal logic.