Almost Linear Büchi Automata

Tomáš Babiak
Vojtěch Řehák
Jan Strejček

We introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Buechi automata (BA) called Almost linear Buechi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. While standard translations of LTL into BA use some intermediate formalisms, the presented translation of LIO into ALBA is direct. As we expect applications of ALBA in model checking, we compare the expressiveness of ALBA with other classes of Buechi automata studied in this context and we indicate possible applications.

In Sibylle Fröschle and Daniele Gorla: Proceedings 16th International Workshop on Expressiveness in Concurrency (EXPRESS 2009), Bologna, Italy, 5th September 2009, Electronic Proceedings in Theoretical Computer Science 8, pp. 16–25.
Published: 17th November 2009.

ArXived at: http://dx.doi.org/10.4204/EPTCS.8.2 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org