Title :
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
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;
Conference_Titel :
Intelligent Computation Technology and Automation (ICICTA), 2008 International Conference on
Conference_Location :
Hunan
Print_ISBN :
978-0-7695-3357-5
DOI :
10.1109/ICICTA.2008.297
