Approximate Safety Properties in Metric Transition Systems

Metric transition systems (MTSs) are proposed for quantitative verification of reactive systems. There are already a number of papers on quantitatively analyzing behaviors of systems based on MTSs. In this article, we make further progress along this research line by lifting safety properties, which assert that nothing "bad" happens during execution of systems, to MTSs. First, we introduce a distance threshold $\alpha \ \text{taken from [0,1],}$ which is used to analyze to what extent a system satisfies its specification. Then, we present a quantitative extension of safety properties, called $\alpha$-safety properties. Furthermore, we give an alternative characterization of $\alpha$-safety properties by means of their closure. In addition, an algorithm for verifying whether a system satisfies a subclass of $\alpha$-safety properties is developed, assuming that the method to convert a regular $\alpha$-safety property to an equivalent metric finite automaton has been given. Finally, we present an example to illustrate our approaches.