Abstract: In recent years,quantitative verification of computer systems has attracted much attention from the academic and industrial communities,where the study of system specifications over metric spaces has offered a new research line for the development of quantitative verification.In system verification,linear time attribute is often used to describe the properties of the system,and security,as one of the most important basic attributes of linear time attribute,can assert that nothing “bad” happens during execution of systems.Hence the extension of safety properties should also be concerned in the context of metrics.This paper investigates safety properties over pseudo-ultrametric spaces.First,metric linear temporal logic (MLTL) is used to characterize linear-time properties in the context of metrics metrics.Then,this paper lifts the notion of safety properties to pseudo-ultrametric spaces,called α-safety properties,by introducing the distance threshold α.Finally,the relationship between MLTL and α-safety properties is discussed.These results provide a theoretical basis for the verification of safety properties in the context of metrics.

Key words: Linear temporal logic, Linear-time property, Model checking, Pseudo-ultrametric space, Safety property