6533b857fe1ef96bd12b432c

RESEARCH PRODUCT

Minimal Büchi Automata for Certain Classes of LTL Formulas

Andrzej JasińskiAdam CzubakJacek Cichoń

subject

Model checkingTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESTheoretical computer scienceLinear temporal logicComputer scienceComputer Science::Logic in Computer ScienceBüchi automatonAutomata theoryTemporal logicComputer Science::Formal Languages and Automata Theory

description

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.

yearjournalcountryeditionlanguage
2009-01-012009 Fourth International Conference on Dependability of Computer Systems
https://doi.org/10.1109/depcos-relcomex.2009.31