×

Lazy reachability analysis in distributed systems. (English) Zbl 1392.68305

Desharnais, Josée (ed.) et al., 27th international conference on concurrency theory, CONCUR 2016, Québec City, Canada, August 23–26, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-017-0). LIPIcs – Leibniz International Proceedings in Informatics 59, Article 17, 14 p. (2016).
Summary: 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.
For the entire collection see [Zbl 1351.68014].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68M14 Distributed systems
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI