Mathematical Structures in Computer Science

Table of Contents - April 2012 - Volume 22, Special Issue 02 (Express '09, Ice '09 and Sos '09)  

Paper

Almost linear Büchi automata

TOMÁŠ BABIAKa1†, VOJTĚCH ŘEHÁKa1‡ and JAN STREJČEKa1§

a1 Faculty of Informatics, Masaryk University, Brno, Czech Republic Email: xbabiak@fi.muni.cz, rehak@fi.muni.cz, strejcek@fi.muni.cz

Abstract

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 there to be applications of our results in model checking, we use two standard sources of specification formulae, namely Spec Patterns and BEEM, to study the practical relevance of the LIO fragment, and to compare our translation of LIO to ALBA with two standard translations of LTL to BA using alternating automata. Finally, we demonstrate that the LIO to ALBA translation can be much faster than the standard translation, and the resulting automata can be substantially smaller.

(Received January 25 2010)

(Revised September 13 2010)

Footnotes

† Tomáš Babiak has been supported by the Czech Science Foundation, grants No. 201/09/1389 and No. 102/09/H042.

‡ Vojtěch Řehák has been supported by the research centre ‘Institute for Theoretical Computer Science (ITI)’, project No. 1M0545, and by the Czech Science Foundation, grants No. 201/08/P459 and No. P202/10/1469.

§ Jan Strejček has been supported by the Ministry of Education of the Czech Republic, project No. MSM0021622419, and by the Czech Science Foundation, grants No. 201/08/P375 and No. P202/10/1469.