基于度量线性时态逻辑的近似安全性  

Approximate Safety Properties in Metric Linear Temporal Logic

作　　者：蔡泳 钱俊彦[1] 潘海玉 CAI Yong;QIAN Jun-yan;PAN Hai-yu(Guangxi Key Laboratory of Trusted Software,Guilin University of Electronic Technology,Guilin,Guangxi 541004,China)

机构地区：[1]桂林电子科技大学广西可信软件重点实验室,广西桂林541004

出　　处：《计算机科学》2020年第10期309-314,共6页Computer Science

基　　金：国家自然科学基金(61672023);广西自然科学基金(2018GXNSFAA281326);广西可信软件重点实验室基金(kx201911)。

摘　　要：近年来,计算机系统的定量验证已经引起了学术界和工业界足够的关注,其中取值于度量空间的系统性质研究为定量验证的发展开辟了一条新途径。在系统验证中常用线性时间属性来刻画系统的性质,而安全性作为线性时间属性中一类至关重要的基础属性,能保证系统在运行过程中不会发生“坏”的事情,其在度量背景下的推广形式也应该得到关注。为此,文中研究伪超度量空间上安全性的扩展问题,首先对已有的度量线性时态逻辑进行适当的补充,使其能充分地刻画度量背景下的线性时间属性;然后引入距离阈值α,提出一种α-安全性的概念,从而将经典的安全性提升到伪超度量空间上;最后讨论度量线性时态逻辑与α-安全性之间的关系。这些结论为取值于度量空间的系统的安全性验证提供了理论依据。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.

关 键 词：安全性 模型检测 线性时间属性 线性时态逻辑 伪超度量空间 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]