一类线性时段不变式的验证优化与实现

摘要：

线性时段不变式是一类重要的时段演算公式。文献[1]中提出一种验证算法，能够针对以时间自动机建模的系统，模型检验其是否满足一个扩展的线性时段不变式。在验证一类特定公式时，该算法需要引入O(b)个辅助变量，且需全程保留它们的值，会导致检验这类公式所需的变量数和复杂度急剧增长。该文提出一种基于系统反转的模型检验方法，并为线性时段不变式的模型检验问题提供一种全新的解决思路。

关键词：模型检验、时间自动机、线性时段不变式、切变、反向系统

所属期刊栏目：12

分类号：TP311(计算技术、计算机技术)

在线出版日期：2016-05-04（万方平台首次上网日期，不代表论文的发表时间）

页数：共2页

页码：71-72