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

Varování

Publikace nespadá pod Filozofickou 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:	Techniky automatické verifikace a validace softwarových a hardwarových systémů Realistická aplikace formálních metod v komponentových systémech Vysoce paralelní a distribuované výpočetní systémy Verifikace a analýza velmi velkých počítačových systémů Automatizovaná formální verifikace s využitím soudobého hardware Rozsáhlé výpočetní systémy: modely, aplikace a verifikace Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity