Abstract
This paper presents CNDFS, a tight integration of two earlier multi-core nested depth-first search (NDFS) algorithms for LTL model checking. CNDFS combines the different strengths and avoids some weaknesses of its predecessors. We compare CNDFS to an earlier ad-hoc combination of those two algorithms and show several benefits: It has shorter and simpler code and a simpler correctness proof. It exhibits more stable performance and scalability, while at the same time reducing memory requirements.
The algorithm has been implemented in the multi-core backend of the LTSmin model checker, which is now benchmarked for the first time on a 48 core machine (previously 16). The experiments demonstrate better scalability than other parallel LTL model checking algorithms, but we also investigate apparent bottlenecks.
Finally, we noticed that the multi-core NDFS algorithms produce shorter counterexamples, surprisingly often shorter than their BFS-based counterparts.
Original language | Undefined |
---|---|
Title of host publication | Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012 |
Editors | S. Ramesh |
Place of Publication | London |
Publisher | Springer |
Pages | 269-283 |
Number of pages | 15 |
ISBN (Print) | 978-3-642-33386-6 |
DOIs | |
Publication status | Published - 3 Oct 2012 |
Event | 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012 - Thiruvananthapuram, India Duration: 3 Oct 2012 → 6 Oct 2012 Conference number: 10 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer Verlag |
Volume | 7561 |
Conference
Conference | 10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012 |
---|---|
Abbreviated title | ATVA |
Country/Territory | India |
City | Thiruvananthapuram |
Period | 3/10/12 → 6/10/12 |
Keywords
- METIS-287890
- CNDFS
- IR-80818
- LTL model checking
- LTSMIN
- Verification
- EWI-21967
- Multi-Core
- liveness properties
- paralll
- nested depth-first search
- FMT-MC: MODEL CHECKING
- NDFS