-
题名加权迁移系统线性时间属性及其安全性检测
- 1
-
-
作者
林运国
-
机构
福建农林大学计算机与信息学院
-
出处
《计算机应用》
CSCD
北大核心
2014年第5期1413-1417,共5页
-
文摘
针对加权迁移系统,提出了线性时间属性及其安全性检测。首先定义了半环K上的加权迁移系统,提出了加权线性时间属性概念,并根据权重函数确定加权线性时间属性的上确界、下确界和闭包;接着给出了几种常见的加权线性时间属性并且讨论了它们的关系;然后重点研究了加权安全性,通过加权自动机和闭包给出了加权正则安全性;最后基于加权有穷自动机,建立了加权正则安全性的检测方法。检测过程结合半环和形式幂级数,构造了加权迁移系统和加权有穷自动机的乘积系统,将加权安全性检测问题转化为验证乘积系统的不变性,给出了加权正则安全性检测的算法和复杂度。实例结果表明,所提的方法能够对加权迁移系统的安全性进行检测。
-
关键词
迁移系统
线性时间属性
模型检测
安全性
半环
-
Keywords
transition system
linear time property
model checking
safety property
semiring
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名线性时间属性中近似安全性和活性的刻画
- 2
-
-
作者
常玉婷
潘海玉
-
机构
桂林电子科技大学计算机与信息安全学院
-
出处
《桂林电子科技大学学报》
2022年第5期423-430,共8页
-
基金
国家自然科学基金(62162014)
广西自然科学基金(2018GXNSFAA281326)
广西可信软件重点实验室基金(kx201911)。
-
文摘
针对线性时间属性中最重要的基础属性安全性和活性,将它们扩展到模糊背景下,有助于定量刻画系统与其属性之间的满足程度。结合度量理论中线性距离的概念,刻画系统与属性之间关系,进而量化一个系统多大程度满足一个属性。首先回顾线性距离的定义以及一些性质。其次,基于模糊迁移系统,研究线性时间属性中安全性和活性的定量扩展形式,并尽可能多地保留传统线性时间属性相关的优良性质,通过给定距离阈值α,定义α-安全性和α-活性,从而将经典的线性时间属性扩展到模糊背景下。通过对所提出的α-安全性和α-活性理论进行扩充,对现有模糊背景下的线性时态逻辑进行适当地补充,从而刻画所定义的α-安全性和α-活性。最后通过一个具体的实例来阐述所得出的结论。
-
关键词
线性时间属性
模糊逻辑
安全性
活性
线性时态逻辑
-
Keywords
linear-time properties
fuzzy logic
safety
liveness
linear temporal logic
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名基于度量线性时态逻辑的近似安全性
被引量：2
- 3
-
-
作者
蔡泳
钱俊彦
潘海玉
-
机构
桂林电子科技大学广西可信软件重点实验室
-
出处
《计算机科学》
CSCD
北大核心
2020年第10期309-314,共6页
-
基金
国家自然科学基金(61672023)
广西自然科学基金(2018GXNSFAA281326)
广西可信软件重点实验室基金(kx201911)。
-
文摘
近年来,计算机系统的定量验证已经引起了学术界和工业界足够的关注,其中取值于度量空间的系统性质研究为定量验证的发展开辟了一条新途径。在系统验证中常用线性时间属性来刻画系统的性质,而安全性作为线性时间属性中一类至关重要的基础属性,能保证系统在运行过程中不会发生“坏”的事情,其在度量背景下的推广形式也应该得到关注。为此,文中研究伪超度量空间上安全性的扩展问题,首先对已有的度量线性时态逻辑进行适当的补充,使其能充分地刻画度量背景下的线性时间属性;然后引入距离阈值α,提出一种α-安全性的概念,从而将经典的安全性提升到伪超度量空间上;最后讨论度量线性时态逻辑与α-安全性之间的关系。这些结论为取值于度量空间的系统的安全性验证提供了理论依据。
-
关键词
安全性
模型检测
线性时间属性
线性时态逻辑
伪超度量空间
-
Keywords
Safety property
Model checking
Linear-time property
Linear temporal logic
Pseudo-ultrametric space
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
