A Comparative Study of Algorithms for Linear Temporal Logic to Buchi Automata Translation

• Main Authors: Wen-Chin Chan, 詹文欽
• Other Authors: 蔡益坤
• Format: Others
• Language: en_US
• Published: 2007
• Online Access: http://ndltd.ncl.edu.tw/handle/72400654554970813585

碩士 === 臺灣大學 === 資訊管理學研究所 === 95 === Buchi automata and linear temporal logic are fundamental components of the automata-theoretic approach to model checking, where Buchi automata are used to represent systems, while Propositional Linear Temporal Logic (PTL) is used to specify properties of a system. The approach involves translation of a negated specification PTL formula into a Buchi automaton, which is then intersected with the system automaton and checked for emptiness. In principle, the smaller the translated Buchi automaton, the faster the model checking process. Over the years, numerous algorithms for PTL to Buchi automata translation have been developed. These algorithms construct automata using different intermediate structures and, for a given PTL formula, generate automata of different sizes. Although there have been works comparing some of these algorithms, they are not quite complete in the number of algorithms or in the types of PTL formulae. The goal of this thesis is to provide a more complete comparison and to explain some of the differences between these algorithms. In this thesis, we compare six well-known translation algorithms. Comparisons are made with various combinations of optimization techniques being applied to the translated Buchi automaton. Some of the translation algorithms considered, in particular several on-the-fly algorithms, do not apply for formulae containing past operators. To make the comparisons complete and fair, we extend these on-the-fly algorithms to support past operators, while maintaining the advantages of incremental temporal tableau construction. The extension seems to be new. We hope that such a comparative study would help other researchers in choosing the appropriate translation algorithm and obtaining the smallest possible translated Buchi automaton. As a by-product of this research, we extend the GOAL tool, a graphical tool for manipulating omega-automata and temporal formulae, with five of the six translation algorithms. The previous version of GOAL had only one of the six translation algorithms using tableau construction. The GOAL tool now not only serves educational purposes but also provides a platform for comparative studies of PTL to Buchi automata translation algorithms.