Authors:
- Tom van Dijk
- Jeroen Meijer
- Jaco van de Pol
Published in: TACAS pp 58–75
DOI: 10.1007/978-3-030-17465-1_4
Abstract:
Saturation is an efficient exploration order for computing the set of reachable states symbolically. Attempts to parallelize saturation have so far resulted in limited speedup. We demonstrate for the first time that on-the-fly symbolic saturation can be successfully parallelized at a large scale. To this end, we implemented saturation in Sylvan’s multi-core decision diagrams used by the LTSmin model checker. We report extensive experiments, measuring the speedup of parallel symbolic saturation on a 48-core machine, and compare it with the speedup of parallel symbolic BFS and chaining. We find that the parallel scalability varies from quite modest to excellent. We also compared the speedup of on-the-fly saturation and saturation for pre-learned transition relations. Finally, we compared our implementation of saturation with the existing sequential implementation based on Meddly. The empirical evaluation uses Petri nets from the model checking contest, but thanks to the architecture of LTSmin, parallel on-the-fly saturation is now available to multiple specification languages.
BibTeX entry:
@inproceedings{DijkMP19,
author = {Tom van Dijk and Jeroen Meijer and Jaco van de Pol},
booktitle = {TACAS},
doi = {10.1007/978-3-030-17465-1_4},
pages = {58--75},
publisher = {Springer},
series = {LNCS},
talk = {2019parsat_talk.pdf},
title = {Multi-core On-The-Fly Saturation},
volume = {11428},
year = {2019}
}