Almost linear Büchi automata

Investor logo
Investor logo
Investor logo
Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BABIAK Tomáš STREJČEK Jan ŘEHÁK Vojtěch

Year of publication 2012
Type Article in Periodical
Magazine / Source Mathematical Structures in Computer Science
MU Faculty or unit

Faculty of Informatics

Citation
Web http://dx.doi.org/10.1017/S0960129511000399
Doi http://dx.doi.org/10.1017/S0960129511000399
Field Informatics
Keywords LTL; linear time logic; model checking
Description We introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Büchi automata (BA) called Almost linear Büchi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. As we expect applications of our results in model checking, we use two standard sources of specification formulae, namely Spec Patterns and BEEM, to study practical relevance of LIO fragment, and to compare our translation of LIO to ALBA with two standard translations of LTL to BA via alternating automata. Finally, we demonstrate that the LIO to ALBA translation can be much faster than the standard translation and the produced automata can be substantially smaller.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.