Almost Linear B\"uchi Automata

TL;DR

This paper introduces Almost Linear B"uchi Automata (ALBA) and a new fragment of LTL called LIO, providing direct translation methods and exploring their applications in model checking.

Contribution

It presents a novel class of B"uchi automata (ALBA) and a new LTL fragment (LIO), with effective translation techniques demonstrating their expressive equivalence.

Findings

LIO and ALBA are expressively equivalent.

Direct translation from LIO to ALBA is possible.

ALBA has potential applications in model checking.

Abstract

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.