Skip to Main content Skip to Navigation
Conference papers

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 (UMR 6174), 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Pierre-Cyrille Heam Connect in order to contact the contributor
Submitted on : Tuesday, November 26, 2013 - 9:28:56 AM
Last modification on : Friday, January 21, 2022 - 3:09:38 AM
Long-term archiving on: : Thursday, February 27, 2014 - 5:50:08 AM


Publisher files allowed on an open archive



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⟩



Record views


Files downloads