Almost linear Büchi automata
type: Item
instance of: scholarly article
title: Almost linear Büchi automata
zbMATH Open document ID: 1254.68141
DOI: 10.1017/S0960129511000399
author: Tomáš Babiak
author: Vojtěch Řehák
author: Jan Strejček
publication date: 2012-05-11T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 03D05
Mathematics Subject Classification ID: 68Q45
zbMATH DE Number: 6033365
zbMATH Keywords: LTL
zbMATH Keywords: Büchi automata
describes a project that uses: DiVinE
MaRDI profile type: Publication
cites work: Depth-First Search and Linear Graph Algorithms
published in: MSCS. Mathematical Structures in Computer Science
review text: 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 situa…
reviewed by: Viktor Schuppan
description: scientific article; zbMATH DE number 6033365