HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Emptiness of Linear Weak Alternating Automata

Stephan Merz 1 Ali Sezgin
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The automata-theoretic approach to model checking requires two basic ingredients: a translation from logic to automata, and an algorithm for checking language emptiness. LTL model checking has traditionally been based on (generalized) Büchi automata. Weak alternating automata provide an attractive alternative because there is an elegant and linear-time translation from LTL. However, due to their intricate combinatorial structure, no direct algorithm for deciding the emptiness problem for these automata has been known, and implementations have relied on an exponential translation of weak alternating to nondeterministic Büchi automata. In this paper, we fill this gap by proposing an algorithm to decide language emptiness for the subclass of weak alternating automata that result from the translation of LTL formulas. Our approach makes use of two observations: first, runs of weak alternating automata can be represented as dags and second, the transition graphs of linear weak alternating automata are of restricted combinatorial structure. Our algorithm computes strongly connected components of the graph of reachable configurations, the emptiness criterion being expressed in terms of the set of self loops that can be avoided within an SCC.
Document type :
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Thursday, October 19, 2006 - 9:07:56 AM
Last modification on : Friday, February 4, 2022 - 3:34:38 AM
Long-term archiving on: : Friday, November 25, 2016 - 12:24:17 PM


  • HAL Id : inria-00107750, version 1



Stephan Merz, Ali Sezgin. Emptiness of Linear Weak Alternating Automata. [Intern report] A03-R-503 || merz03c, 2003, 14 p. ⟨inria-00107750⟩



Record views


Files downloads