@inproceedings{2a9d1889472544bfb86f9aaf38713f19,
title = "Multi-core On-The-Fly Saturation",
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{\textquoteright}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. Data or code related to this paper is available at: [34].",
author = "{van Dijk}, Tom and Jeroen Meijer and {van de Pol}, Jaco",
year = "2019",
month = jan,
day = "1",
doi = "10.1007/978-3-030-17465-1_4",
language = "English",
isbn = "978-3-030-17464-4",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "58--75",
editor = "Lijun Zhang and Tom{\'a}{\v s} Vojnar",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
address = "Germany",
note = "25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 , TACAS 2019 ; Conference date: 06-04-2019 Through 11-04-2019",
}