The characterization of approximate safety and liveness properties in linear-time properties

For the safety and liveness properties of the most important basic properties in linear-time properties, they are extended to the fuzzy background, which is helpful to quantitatively describe the level of satisfaction between the system and its properties. Combining with the concept of linear distance in metric theory, this paper quantifies how extent a system satisfies its property by describing the relationship between the system and its property with distance. First, the definitions and some properties of linear distance are reviewed. Next, based on the fuzzy transition system, the safety and liveness properties in linear time property are quantitatively expanded, and the good properties of traditional linear time properties are retained as much as possible. In addition, the definitions of α-safety properties and α-liveness properties are defined by introducing the distance threshold α, thus extending the classical linear temporal properties to the fuzzy setting. Then, the proposed theory of α-safety properties and α-liveness properties are extended, and the existing linear temporal logic under fuzzy background is appropriately supplemented in order to characterized α-safety properties and α-liveness properties. Finally, a concrete example is given to illustrate the conclusions of this paper.