关于交替式下推系统可达性证明的研究与实现

摘要：

演绎推理是形式化验证中一种重要的方法,具有可以处理无穷状态系统的优点.本文研究与实现关于交替式下推系统中可达性的证明,该系统可以将无穷证明树转换为有穷树.文中首先利用迭代收敛思想实现了饱和算法,并通过全排列算法实现了系统完备化;然后采用余归纳方式对搜索证明进行了优化;最后利用可视化技术对证明树在三维空间进行展示.

关键词：推理验证、形式化验证、交替式下推系统、无穷状态系统、可视化

所属期刊栏目：25

分类号：TP3;X70

资助基金：中法NSFC-ANR共同资助合作研究项目LOCALI61161130530

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

页数：共8页

页码：69-76