加权迁移系统线性时间属性及其安全性检测

Linear time properties of weighted transition system and checking of safety property

针对加权迁移系统,提出了线性时间属性及其安全性检测。首先定义了半环K上的加权迁移系统,提出了加权线性时间属性概念,并根据权重函数确定加权线性时间属性的上确界、下确界和闭包;接着给出了几种常见的加权线性时间属性并且讨论了它们的关系;然后重点研究了加权安全性,通过加权自动机和闭包给出了加权正则安全性;最后基于加权有穷自动机,建立了加权正则安全性的检测方法。检测过程结合半环和形式幂级数,构造了加权迁移系统和加权有穷自动机的乘积系统,将加权安全性检测问题转化为验证乘积系统的不变性,给出了加权正则安全性检测的算法和复杂度。实例结果表明,所提的方法能够对加权迁移系统的安全性进行检测。

With regard to the weighted transition system, the linear time properties were proposed. Firstly, the weighted transition system above semiring K was defined, the concepts of the weighted linear time properties were given, the upper, the lower and the closure of weighted linear time properties were determined by the weighted function; secondly some familiar weighted linear time properties and their relationships were discussed; thirdly the weighted safety property was mainly studied, the weighted regular safety property was defined through weighted automaton and closure of weighted regular safety property; finally, the checking method of the weighted regular safety was built based on weighted finite automaton. The checking was follows. Together with semiring and formal series, the product system was built over weighted transition and weighted finite automaton, the model checking about weighted safety property of weighted transition was transferred to verify the invariance of the product system, the algorithm and complexity were given. Finally, an example shows the model checking of weighted regular safety property is reasonable and efficient. The example result shows the proposed method can verify the safety of the weighted system.