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

摘要

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

关键词

线性时间属性 / 模糊逻辑 / 安全性 / 活性 / 线性时态逻辑