Enhancing Approximations for Regular Reachability Analysis
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.
Cite
@article{arxiv.1311.6605,
title = {Enhancing Approximations for Regular Reachability Analysis},
author = {Alois Dreyfus and Pierre-Cyrille Heam and Olga Kouchnarenko},
journal= {arXiv preprint arXiv:1311.6605},
year = {2013}
}