Publication details

<< back
 

Almost linear Büchi automata

Basic information
Original title:Almost linear Büchi automata
Authors:Tomáš Babiak, Jan Strejček, Vojtěch Řehák
Further information
Citation:BABIAK, Tomáš, Jan STREJČEK and Vojtěch ŘEHÁK. Almost linear Büchi automata (Almost linear Büchi automata). Mathematical Structures in Computer Science, Cambridge: Cambridge University Press, 2012, vol. 22, No 2, p. 203-235. ISSN 0960-1295. doi:10.1017/S0960129511000399.Export BibTeX
@article{913326,
author = {Babiak, Tomáš and Strejček, Jan and Řehák, Vojtěch},
article_location = {Cambridge},
article_number = {2},
doi = {http://dx.doi.org/10.1017/S0960129511000399},
keywords = {LTL; linear time logic; model checking},
language = {eng},
issn = {0960-1295},
journal = {Mathematical Structures in Computer Science},
title = {Almost linear Büchi automata},
url = {http://dx.doi.org/10.1017/S0960129511000399},
volume = {22},
year = {2012}
}
Original language:English
Field:Informatics
WWW:link to a new windowhttp://dx.doi.org/10.1017/S0960129511000399
Type:Article in Periodical
Keywords:LTL; linear time logic; model checking

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:

 
 
top