On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties

Investor logo
Investor logo

Warning

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

BARNAT Jiří BRIM Luboš ROČKAI Petr

Year of publication 2012
Type Article in Periodical
Magazine / Source Science of Computer Programming
MU Faculty or unit

Faculty of Informatics

Citation
Web http://dx.doi.org/10.1016/j.scico.2011.03.001
Doi http://dx.doi.org/10.1016/j.scico.2011.03.001
Field Informatics
Keywords Explicit Model Checking; Parallel; On-the-fly; Partial Order Reduction
Description One of the most important open problems of parallel LTL model checking is to design an on-the-fly scalable parallel algorithm with linear time complexity. Such an algorithm would provide the same optimality we have in sequential LTL model checking. In this paper we give a partial solution to the problem: we propose an algorithm that has the required properties for a very rich subset of LTL properties, namely those expressible by weak Buchi automata. In addition to the previous version of the paper, we demonstrate how our new algorithm can be efficiently combined with a particular parallel technique for Partial Order Reduction and report on additional experiments.
Related projects:

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