Volume 10, Number 2
Converting A Subset of LTL Formula to Buchi Automata
Authors
Bilal Kanso and Ali Kansou, Lebanese University, Beirut
Abstract
The translation of LTL formula into equivalent Büchi automata plays an important role in many algorithms
for LTL model checking, which consist in obtaining a Büchi automaton that is equivalent to the software
system specification and another one that is equivalent to the negation of the property. The intersection of
the two Büchi automata is empty if the model satisfies the property.
Generating the Büchi automaton corresponding to an LTL formula may, in the worst case, be exponential
in the size of the formula, making the model checking effort exponential in the size of the original formula.
There is no polynomial solution for checking emptiness of the intersection. That comes from the translation
step of LTL formula into finite state models. This makes verification methods hard or even impossible to be
implemented in practice. In this paper, we propose a subset of LTL formula which can be converted to
Büchi automata whose the size is polynomial.
Keywords
Linear Temporal Logic, Büchi automata, Model checking, Compositional modelling