Enhancing Approximations for Regular Reachability Analysis

Alois Dreyfus 1, 2 Pierre-Cyrille Heam 2, 1 Olga Kouchnarenko 1, 2
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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.
Type de document :
Communication dans un congrès
Stavros Konstantinidis. CIAA 2013 - 18th International Conference on Implementation and Application of Automata - 2013, Jul 2013, Halifax, Canada. Springer, 7982, pp.331-339, 2013, Lecture Notes in Computer Science. 〈http://link.springer.com/chapter/10.1007%2F978-3-642-39274-0_29〉. 〈10.1007/978-3-642-39274-0_29〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00909204
Contributeur : Pierre-Cyrille Heam <>
Soumis le : mardi 26 novembre 2013 - 09:28:56
Dernière modification le : jeudi 15 février 2018 - 08:48:14
Document(s) archivé(s) le : jeudi 27 février 2014 - 05:50:08

Fichiers

document.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Citation

Alois Dreyfus, Pierre-Cyrille Heam, Olga Kouchnarenko. Enhancing Approximations for Regular Reachability Analysis. Stavros Konstantinidis. CIAA 2013 - 18th International Conference on Implementation and Application of Automata - 2013, Jul 2013, Halifax, Canada. Springer, 7982, pp.331-339, 2013, Lecture Notes in Computer Science. 〈http://link.springer.com/chapter/10.1007%2F978-3-642-39274-0_29〉. 〈10.1007/978-3-642-39274-0_29〉. 〈hal-00909204〉

Partager

Métriques

Consultations de la notice

367

Téléchargements de fichiers

153