Minimal Büchi Automata for Certain Classes of LTL Formulas
Jacek Cichoń, Adam Czubak, Andrzej Sebastian Jasiński OFM · 2009
In this paper we calculate the minimal number of states of Buchi automata which encode some classes of linear temporal logic (LTL) formulas that are frequently used in model checking. Among others, we show that the minimal size of a Buchi automaton accepting the formula Pi0p1Lambda ... Lambda Pi0pnis n+1, the minimal size of Buchi automaton accepting the formula 0p1Lambda ... Lambda0pnis 2nand the minimal size of a Buchi automaton accepting the formula 0(p1Lambda0p1)Lambda...Lambda(pnLambda0pn) is 3n. Our results may be used for verification of the quality of algorithms which automatically translate LTL formulas into Buchi automata and for improving the quality and speed of such translators. In the last section of this paper we compare our lower bound estimations to Buchi automata generated by two currently used translators: LTL2BA and SPOT. We have checked, among others, that the LTL2BA translator generates a Buchi automaton with 25 states and the SPOT translator generates an automaton with 31 states for the formula 0(p1Lambda0(p2Lambda0p3))Lambda0(q1Lambda0(q2Lambda0q3)), while the minimal required number of states is 16.