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

A Verification Method For Finite States Systems Based on Temporal Logic

作　　者：杜慧敏 杨红丽[2] 高德远[1] 韩俊刚[2] 

机构地区：[1]西北工业大学计算机科学系,陕西西安710072 [2]西安邮电学院计算机系,陕西西安710061

出　　处：《西北工业大学学报》2000年第1期111-115,共5页Journal of Northwestern Polytechnical University

基　　金：国家自然科学基金!694 73 0 17

摘　　要：LPTL ( Linear Proposition Temporal Logic)与自动机之间有着紧密的联系 ,结合 LPTL语义和语法 ,提出一种从 LPTL公式导出 Büchi自动机的方法。导出的 Büchi自动机所接受的语言准确地表达了 LPTL公式所描述的特性。从而把由 LPTL公式描述的系统设计规范的验证问题转换成检验 Büchi自动机的包含问题。Büchi automata is one form of finite automata on infinite sequences. It can model concurrent system or reactive system, and describe specification of such systems. Linear proposition temporal logic(LPTL) is interpreted on infinite sequences and can be used to express specifications of the systems. There is close relation between infinite automata and LPTL. J.E.Hopcroft and J.D.Ullman proposed a method for demonstrating the equivalence between regular and finite automata. Based on this method, we propose a method to derive a Büchi automata from LPTL by integrating the syntax and semantics of LPTL. The derived automata can be treated as a specification automata. Language received by the Büchi automata exactly describe the properties expressed by LPTL. If the implementation of system is modeled by Büchi automaton and the specification is described by LPTL, the problem of formal verification of systems can be converted into a problem of checking containment of language received by implementation automaton and specification automata. Our method has beenimplemented with VB in Windows 95.

关 键 词：命题时态逻辑 形式化验证 有限状态系统 自动机 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构]