论文部分内容阅读
提出了一种基于归纳法思想的验证方法，通过控制周期上特性的描述，发现了基于控制周期特征式的线性混合自动机验证方法，这一方法采用定理证明过程来得出归纳证明的结构；采用模型检查方法来得出归纳证明的奠基和迭代步，这一方法同时兼顾了模型检查和定理证明的特点用此定理证明更高的自动化程度解决了单用模型检查不能解决的问题，得出了对著名案例ＧａｓＢｕｒｎｅｒ问题中的参数３ｎｏｎ＿ｌｅａｋｋｉｎｇ≥７６的最优范围。