Abstract
Time optimal reachability analysis employs model-checking to compute goal states that can be reached from an initial state with a minimal accumulated time duration. The model-checker may produce a corresponding diagnostic trace which can be interpreted as a feasible schedule for many scheduling and planning problems, response time optimization etc. We propose swarm verification to accelerate time optimal reachability using the real-time model-checker Uppaal. In swarm verification, a large number of model checker instances execute in parallel on a computer cluster using different, typically randomized search strategies. We develop four swarm algorithms and evaluate them with four models in terms scalability, and time- and memory consumption. Three of these cooperate by exchanging costs of intermediate solutions to prune the search using a branch-and-bound approach. Our results show that swarm algorithms work much faster than sequential algorithms, and especially two using combinations of random-depth-first and breadth-first show very promising performance.
Originalsprog | Engelsk |
---|---|
Titel | Proceedings of the 31st Annual ACM Symposium on Applied Computing |
Antal sider | 7 |
Vol/bind | SAC '16 |
Udgivelsessted | New York, NY, USA |
Forlag | Association for Computing Machinery |
Publikationsdato | 3 apr. 2016 |
Sider | 1634-1640 |
ISBN (Elektronisk) | 978-1-4503-3739-7 |
DOI | |
Status | Udgivet - 3 apr. 2016 |
Begivenhed | The 31st Annual ACM Symposium on Applied Computing - Pisa, Italien Varighed: 4 apr. 2016 → 8 apr. 2016 Konferencens nummer: 31 http://www.sigapp.org/sac/sac2016/ |
Konference
Konference | The 31st Annual ACM Symposium on Applied Computing |
---|---|
Nummer | 31 |
Land/Område | Italien |
By | Pisa |
Periode | 04/04/2016 → 08/04/2016 |
Internetadresse |