Document Open Access Logo

Lazy Reachability Analysis in Distributed Systems

Authors Loïg Jezequel, Didier Lime

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.17.pdf
  • Filesize: 0.58 MB
  • 14 pages

Document Identifiers

Author Details

Loïg Jezequel
Didier Lime

Cite AsGet BibTex

Loïg Jezequel and Didier Lime. Lazy Reachability Analysis in Distributed Systems. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 17:1-17:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CONCUR.2016.17

Abstract

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.
Keywords
  • Reachability analysis
  • Compositional verification
  • Automata

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. H. R. Andersen. Partial model checking. In LICS, pages 398-407, 1995. Google Scholar
  2. F. Bacchus and Q. Yang. Downward refinement and the efficiency of hierarchical problem solving. Artificial Intelligence, 71(1):43-100, 1994. Google Scholar
  3. A. R. Bradley. SAT-based model checking without unrolling. In VMCAI, pages 70-87, 2011. Google Scholar
  4. A. Cimatti and A. Griggio. Software model checking via IC3. In CAV, pages 277-293, 2011. Google Scholar
  5. J. C. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Trans. Software Eng., 22(3):161-180, 1996. Google Scholar
  6. P. Crouzen and F. Lang. Smart reduction. In FASE, pages 111-126, 2011. Google Scholar
  7. C. Flanagan and S. Qadeer. Thread-modular model checking. In SPIN, pages 213-224, 2003. Google Scholar
  8. 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. Google Scholar
  9. S. Graf and B. Steffen. Compositional minimization of finite state systems. In CAV, pages 186-196, 1990. Google Scholar
  10. O. Grumberg and D. E. Long. Model checking and modular verification. TOPLAS, 16(3):843-871, 1994. Google Scholar
  11. J. Hoffmann, J. Porteous, and L. Sebastia. Ordered landmarks in planning. JAIR, 22(1):215-278, 2004. Google Scholar
  12. G. J. Holzmann and D. Peled. An improvement in formal verification. In FORTE, pages 197-211, 1994. Google Scholar
  13. 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. Google Scholar
  14. F. Lang and R. Mateescu. Partial model checking using networks of labelled transition systems and boolean equation systems. LMCS, 9(4), 2013. Google Scholar
  15. A. Lehmann, N. Lohmann, and K. Wolf. Stubborn sets for simple linear time properties. In ICATPN, pages 228-247, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact