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

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