An Efficient Algorithm for Transforming LTL Formula to Büchi Automaton

Author

He, Anping ; Wu, Jinzhao ; Li, Lian

Author_Institution

Sch. of Inf. Sci. & Eng., Lanzhou Univ., Lanzhou

Volume

1

fYear

2008

fDate

20-22 Oct. 2008

Firstpage

1215

Lastpage

1219

Abstract

Model checking is an automatic technique for verifying finite state concurrent systems. A rapid solution for the model checking problem is checking the emptiness of product Buchi automaton (BA) of the automaton for finite system and the one for the linear temporal logic (LTL) formula, so the algorithm for transforming LTL formula to BA is one of the bases of the whole model checking procedure. In this article, we propose a new efficient algorithm for transforming LTL formula to BA basing on analysis of the tableau structures of LTL formulae, which could efficiently reduce the size of the automaton, but not increases the spatiotemporal complexity, potentially the efficiency of the whole procedure of verification can be improved.

Keywords

automata theory; formal verification; temporal logic; Buchi automaton; LTL formula; finite state concurrent systems; linear temporal logic; model checking; spatiotemporal complexity; tableau structures; Automata; Automation; Boolean functions; Concurrent computing; Data structures; Helium; Information science; Information technology; Logic; State-space methods; Buchi automaton; Linear Temporal Logic; Tableau structure;

fLanguage

English

Publisher

ieee

Conference_Titel

Intelligent Computation Technology and Automation (ICICTA), 2008 International Conference on

Conference_Location

Hunan

Print_ISBN

978-0-7695-3357-5

Type

conf

DOI

10.1109/ICICTA.2008.297

Filename

4659686