A Comparative Study of Algorithms for Linear Temporal Logic to Buchi Automata Translation
Date Issued
2007
Date
2007
Author(s)
Chan, Wen-Chin
DOI
en-US
Abstract
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.
Subjects
Buchi 自動機
模型檢驗
Omega 自動機
On-the-fly 模型檢驗
命題線性時間邏輯
時間邏輯
驗證
Buchi Automata
Model Checking
Omega-Automata
On-the-fly Model Checking
PTL
Temporal Logic
Verification
Type
other
File(s)![Thumbnail Image]()
Loading...
Name
ntu-96-R94725043-1.pdf
Size
23.31 KB
Format
Adobe PDF
Checksum
(MD5):0f7df229c2719d49370f655c9ab4d38c