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

• 作者: 胡棐禹
• 来源期刊: 电脑知识与技术：学术交流
• 学科: 工学
• 关键词: 模型检验 时间自动机 线性时段不变式 切变 反向系统
• 年，卷（期）: dnzsyjsxsb_2016,（1X）
• 页码范围: 71-72
• 页数: 2页
• 分类号: TP301.1

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	胡棐禹	同济大学软件学院	2	1	1.0	1.0