一种基于时态逻辑的有限状态系统验证方法1

摘要：

线性命题时态逻辑（LPTL）可定性地描述系统的时间特性，自动机可用于计算机系统的建模。LPTL与自动机之间有着紧密的联系。结合LPTL语义和语法，本文提出一种从LPTL公式导出Buchi自动机的方法。导出的Bucbi自动机所接收的语言准确地表达了LPTL公式所描述的特性。从而把由LPTL公式描述的系统设计规范的系统验证转换成检验Buchi自动机的包含问题。

关键词： 命题时态逻辑 Buchi自动机 形式化验证 积自动机

作者: 杜慧敏 袁立行 韩俊刚

作者单位: 邮电学院计算机系

会议类型: 国内会议

会议名称: 中国电子学会第四届青年学术年会

会议地点: 北京

会议语种:中文

页码: 317～322

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