线性时间属性中近似安全性和活性的刻画  

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

作　　者：常玉婷 潘海玉 CHANG Yuting;PAN Haiyu(School of Computer and Information Security,Guilin University of Electronic Technology,Guilin 541004,China)

机构地区：[1]桂林电子科技大学计算机与信息安全学院,广西桂林541004

出　　处：《桂林电子科技大学学报》2022年第5期423-430,共8页Journal of Guilin University of Electronic Technology

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

摘　　要：针对线性时间属性中最重要的基础属性安全性和活性,将它们扩展到模糊背景下,有助于定量刻画系统与其属性之间的满足程度。结合度量理论中线性距离的概念,刻画系统与属性之间关系,进而量化一个系统多大程度满足一个属性。首先回顾线性距离的定义以及一些性质。其次,基于模糊迁移系统,研究线性时间属性中安全性和活性的定量扩展形式,并尽可能多地保留传统线性时间属性相关的优良性质,通过给定距离阈值α,定义α-安全性和α-活性,从而将经典的线性时间属性扩展到模糊背景下。通过对所提出的α-安全性和α-活性理论进行扩充,对现有模糊背景下的线性时态逻辑进行适当地补充,从而刻画所定义的α-安全性和α-活性。最后通过一个具体的实例来阐述所得出的结论。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.

关 键 词：线性时间属性 模糊逻辑 安全性 活性 线性时态逻辑 

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