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

Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

BARNAT Jiří BRIM Luboš ROČKAI Petr

Rok publikování 2012
Druh Článek v odborném periodiku
Časopis / Zdroj Science of Computer Programming
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://dx.doi.org/10.1016/j.scico.2011.03.001
Doi http://dx.doi.org/10.1016/j.scico.2011.03.001
Obor Informatika
Klíčová slova Explicit Model Checking; Parallel; On-the-fly; Partial Order Reduction
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.