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.
Type de document :
Rapport
[Intern report] A03-R-503 || merz03c, 2003, 14 p
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00107750
Contributeur : Publications Loria <>
Soumis le : jeudi 19 octobre 2006 - 09:07:56
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 12:24:17

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

231

Téléchargements de fichiers

42