Title :
Minimal Büchi Automata for Certain Classes of LTL Formulas
Author :
Jacek Cichon;Adam Czubak;Andrzej Jasinski
Author_Institution :
Inst. of Math. & Comput. Sci., Wroclaw Univ. of Technol., Wroclaw, Poland
Abstract :
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. 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.
Keywords :
"Automata","Logic","Mathematics","Computer science","Mathematical model","Formal languages","Automatic testing","Stress","Tin"
Conference_Titel :
Dependability of Computer Systems, 2009. DepCos-RELCOMEX ´09. Fourth International Conference on
Print_ISBN :
978-0-7695-3674-3
DOI :
10.1109/DepCoS-RELCOMEX.2009.31
