会议专题

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

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

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

杜慧敏 袁立行 韩俊刚

邮电学院计算机系

国内会议

中国电子学会第四届青年学术年会

北京

中文

317~322

1998-09-01(万方平台首次上网日期,不代表论文的发表时间)