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

https://hal.inria.fr/hal-00909204
Contributor : Pierre-Cyrille Heam <>
Submitted on : Tuesday, November 26, 2013 - 9:28:56 AM
Last modification on : Thursday, November 12, 2020 - 9:42:03 AM
Long-term archiving on: : Thursday, February 27, 2014 - 5:50:08 AM

Files

document.pdf
Publisher files allowed on an open archive

Identifiers

Citation

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⟩

Share

Metrics

Record views

592

Files downloads

447