Almost linear Büchi automata (Q2883118)

The paper introduces almost linear Büchi automata (ALBA), a proper subclass of Büchi automata, and LIO (abbreviating linear and infinitely often), a proper fragment of LTL. In an ALBA every non-terminal SCC consists of one state; terminal SCCs may contain more than one state but are also subject to certain constraints. ALBA turn out to be more powerful than 1-weak Büchi automata, less powerful than Büchi automata, and incomparable to \(k\)-weak Büchi automata for \(k > 1\) as well as terminal Büchi automata. LIO restricts LTL w.r.t.~where negation can be applied and what formulas can be left operands of the until operator. LIO is strictly more expressive than LTL with temporal operators restricted to sometime and globally. ALBA and LIO are shown to be expressively equivalent by providing effective translations between each other. The provided translation from LIO to ALBA is proved to be double exponential in the worst case; the problem of either finding an improved translation or extending that complexity bound to any translation is left open. The translation from LIO to ALBA was implemented and is compared to the translation from LTL to Büchi automata by \textit{P. Gastin} and \textit{D. Oddoux} [Lect. Notes Comput. Sci. 2102, 53--65 (2001; Zbl 0991.68044)]. To simulate a model checking situation negations of LTL formulas from two suites of specifications patterns are investigated. The implementation is able to automatically fit more than half of these formulas into LIO. On those formulas both the resource consumption during the translation and the size of the resulting automata is acceptable.NEWLINENEWLINEIn terms of motivation/benefits of ALBA and LIO the paper does not go far beyond the fact that ALBA and LIO are new fragments and raises hope for improved algorithms. The introduction states that non-emptiness of ALBA can be determined by reachability rather than cycle detection, with the former being more easily parallelizable. However, in a model checking situation the product with the system is what is relevant; that aspect is not covered in the experimental evaluation. In a specification validation situation typically several of the formulas from the benchmark suites would have to be combined into a single query, with only some of the formulas negated. While results for non-negated instances of the specification patterns can be found in one of the authors M.Sc. thesis, neither the effect of combining formulas nor of the resulting formulas being longer on the translation is investigated.