【摘要】 LPTL ( Linear Proposition Temporal Logic)与自动机之间有着紧密的联系 ,结合 LPTL语义和语法 ,提出一种从 LPTL公式导出 Büchi自动机的方法。导出的 Büchi自动机所接受的语言准确地表达了 LPTL公式所描述的特性。从而把由 LPTL公式描述的系统设计规范的验证问题转换成检验 Büchi自动机的包含问题。更多还原

【Abstract】 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.更多还原