Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2016.17
URN: urn:nbn:de:0030-drops-61545
URL: https://drops.dagstuhl.de/opus/volltexte/2016/6154/
Jezequel, Loïg ; Lime, Didier
Lazy Reachability Analysis in Distributed Systems
| pdf-format: |
|
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.
BibTeX - Entry
@InProceedings{jezequel_et_al:LIPIcs:2016:6154,
author = {Loig Jezequel and Didier Lime},
title = {{Lazy Reachability Analysis in Distributed Systems}},
booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)},
pages = {17:1--17:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-017-0},
ISSN = {1868-8969},
year = {2016},
volume = {59},
editor = {Jos{\'e}e Desharnais and Radha Jagadeesan},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6154},
URN = {urn:nbn:de:0030-drops-61545},
doi = {10.4230/LIPIcs.CONCUR.2016.17},
annote = {Keywords: Reachability analysis, Compositional verification, Automata}
}
| Keywords: | Reachability analysis, Compositional verification, Automata | |
| Seminar: | 27th International Conference on Concurrency Theory (CONCUR 2016) | |
| Issue date: | 2016 | |
| Date of publication: | 24.08.2016 |
