计算树逻辑的一个高效模型检验算法

摘要：

该文给出了分支时序逻辑ＣＴＬ的一个基于自动机理论的模型检验算法。作者将模型检验问题规约为树自动机的成员问题，即判定给定树是否为自动机所接收。通过模拟自动机在树上所有可能的运行得到的一个简单的算法。该算法自然地以“需求驱动”方式逐步生成全局状态空间，在大多数情况下，算法都无须生成整个状态空间。此外，算法很好地体现了时间与空间的折衷，在实际应用中具有较好的性能。

关键词： 计算树逻辑 树自动机 模型检验

作者: 胡成军 王戟 陈火旺

作者单位: 科技大学计算机学院

会议类型: 国内会议

会议名称: 1999年全国理论计算机科学学术年会

会议地点: 浙江金华

会议语种:中文

页码: 5～10

在线出版日期: 1999-10-01（万方平台首次上网日期，不代表论文的发表时间）