Distributed LTL Model Checking with Hash Compaction

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BARNAT Jiří HAVLÍČEK Jan ROČKAI Petr

Year of publication 2013
Type Article in Proceedings
Conference Electronic Notes in Theoretical Computer Science, Volume 296
MU Faculty or unit

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.