Lazy Reachability Analysis in Distributed Systems
We address the problem of reachability in distributed systems, modelled as networks of finite automata and propose and prove a new algorithm to solve it efficiently in many cases. This algorithm allows to decompose the reachability objective among the components, and proceeds by constructing partial products by lazily adding new components when required. It thus constructs more and more precise over-approximations of the complete product. This permits early termination in many cases, in particular when the objective is not reachable, which often is an unfavorable case in reachability analysis. We have implemented this algorithm in an early prototype and provide some very encouraging experimental results.
Reachability analysis
Compositional verification
Automata
17:1-17:14
Regular Paper
Loïg
Jezequel
Loïg Jezequel
Didier
Lime
Didier Lime
10.4230/LIPIcs.CONCUR.2016.17
H. R. Andersen. Partial model checking. In LICS, pages 398-407, 1995.
F. Bacchus and Q. Yang. Downward refinement and the efficiency of hierarchical problem solving. Artificial Intelligence, 71(1):43-100, 1994.
A. R. Bradley. SAT-based model checking without unrolling. In VMCAI, pages 70-87, 2011.
A. Cimatti and A. Griggio. Software model checking via IC3. In CAV, pages 277-293, 2011.
J. C. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Trans. Software Eng., 22(3):161-180, 1996.
P. Crouzen and F. Lang. Smart reduction. In FASE, pages 111-126, 2011.
C. Flanagan and S. Qadeer. Thread-modular model checking. In SPIN, pages 213-224, 2003.
H. Garavel, F. Lang, R. Mateescu, and W. Serwe. CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT, 15(2):89-107, 2013.
S. Graf and B. Steffen. Compositional minimization of finite state systems. In CAV, pages 186-196, 1990.
O. Grumberg and D. E. Long. Model checking and modular verification. TOPLAS, 16(3):843-871, 1994.
J. Hoffmann, J. Porteous, and L. Sebastia. Ordered landmarks in planning. JAIR, 22(1):215-278, 2004.
G. J. Holzmann and D. Peled. An improvement in formal verification. In FORTE, pages 197-211, 1994.
F. Kordon, H. Garavel, L. M. Hillah, F. Hulin-Hubard, A. Linard, M. Beccuti, A. Hamez, E. Lopez-Bobeda, L. Jezequel, J. Meijer, E. Paviot-Adet, C. Rodriguez, C. Rohr, J. Srba, Y. Thierry-Mieg, and K. Wolf. Complete Results for the 2015 Edition of the Model Checking Contest. http://mcc.lip6.fr results.php, 2015.
F. Lang and R. Mateescu. Partial model checking using networks of labelled transition systems and boolean equation systems. LMCS, 9(4), 2013.
A. Lehmann, N. Lohmann, and K. Wolf. Stubborn sets for simple linear time properties. In ICATPN, pages 228-247, 2012.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode