一类线性时段不变式的验证优化与实现
线性时段不变式是一类重要的时段演算公式。文献[1]中提出一种验证算法,能够针对以时间自动机建模的系统,模型检验其是否满足一个扩展的线性时段不变式。在验证一类特定公式时,该算法需要引入O(b)个辅助变量,且需全程保留它们的值,会导致检验这类公式所需的变量数和复杂度急剧增长。该文提出一种基于系统反转的模型检验方法,并为线性时段不变式的模型检验问题提供一种全新的解决思路。
模型检验、时间自动机、线性时段不变式、切变、反向系统
12
TP311(计算技术、计算机技术)
2016-05-04(万方平台首次上网日期,不代表论文的发表时间)
共2页
71-72