Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/inria-00107750
Contributor : Publications Loria <>
Submitted on : Thursday, October 19, 2006 - 9:07:56 AM
Last modification on : Friday, February 26, 2021 - 3:28:04 PM
Long-term archiving on: : Friday, November 25, 2016 - 12:24:17 PM

Identifiers

  • HAL Id : inria-00107750, version 1

Collections

Citation

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

Share

Metrics

Record views

323

Files downloads

119