Enhancing Approximations for Regular Reachability Analysis - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Enhancing Approximations for Regular Reachability Analysis

Résumé

This paper introduces two mechanisms for computing over-approximations of sets of reachable states, with the aim of ensuring termination of state-space exploration. The first mechanism consists in over-approximating the automata representing reachable sets by merging some of their states with respect to simple syntactic criteria, or a combination of such criteria. The second approximation mechanism consists in manipulating an auxiliary automaton when applying a transducer representing the transition relation to an automaton encoding the initial states. In addition, for the second mechanism we propose a new approach to refine the approximations depending on a property of interest. The proposals are evaluated on examples of mutual exclusion protocols.
Fichier principal
Vignette du fichier
document.pdf (243.83 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Loading...

Dates et versions

hal-00909204 , version 1 (26-11-2013)

Identifiants

Citer

Alois Dreyfus, Pierre-Cyrille Heam, Olga Kouchnarenko. Enhancing Approximations for Regular Reachability Analysis. CIAA 2013 - 18th International Conference on Implementation and Application of Automata - 2013, Jul 2013, Halifax, Canada. pp.331-339, ⟨10.1007/978-3-642-39274-0_29⟩. ⟨hal-00909204⟩
277 Consultations
128 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More