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

摘要

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