Almost Linear B¨uchi Automata

The growing number of concurrent software and/or hardware systems puts more emphasis on development of automatic verification methods applicable in practice. One of the most promising methods is LTL model checking. The main problem of this verification method is the state explosion problem and consequent high computational complexity. While symbolic approaches to model checking partly solve the problem for hardware systems, there is still no satisfactory solution for model checking of software systems. The most promising approach seems to be a combination of abstraction methods, reduction methods, and optimized model checking algorithms. Reduction methods and optimizations of the algorithms are often based on some specific properties of the specification formula or the model. For example, one of the most effective reduction methods called partial order reduction employs the fact that specification formulae usually do not use the modality next and thus they describe stutter-invariant properties [6],We have realized that all formulae of the restricted temporal logic [10] (i.e. formulae using only temporal operators eventually and always) can be translated to Biichi automata that are linear (1-weak), possibly with an exception of terminal strongly connected components. These terminal components have also a specific property: they accept only infinite words over a set of letters, where some selected letters appear infinitely often. We call such automata Almost linear Biichi automata (ALBA). In this paper we study mainly the expressive power of these automata.Searching for the precise class of LTL formulae corresponding to ALBA automata results in the definition of an LTL fragment named LIO (the abbreviation for linear and infinitely often). The fragment is strictly more expressive than the restricted temporal logic. To prove that LIO corresponds to ALBA, we present translations between LIO and ALBA. While standard translations of LTL formulae into BA use