Distributed LTL Model Checking with Hash Compaction
| Authors | |
|---|---|
| Year of publication | 2013 |
| Type | Article in Proceedings |
| Conference | Electronic Notes in Theoretical Computer Science, Volume 296 |
| MU Faculty or unit | |
| Citation | |
| Web | http://dx.doi.org/10.1016/j.entcs.2013.07.006 |
| Doi | http://dx.doi.org/10.1016/j.entcs.2013.07.006 |
| Field | Informatics |
| Keywords | model checking; LTL; hash compaction |
| Description | We extend a distributed-memory explicit-state LTL model checking algorithm (OWCTY) with hash compaction. We provide a detailed description of the improved algorithm and a correctness argument in the theoretical part of the paper. Additionally, we deliver an implementation of the algorithm as part of out parallel and distributed-memory model checker DiVinE, and use this implementation for a practical evaluation of the approach, on which we report in the experimental part of the paper. |
| Related projects: |