| BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties. Online. Science of Computer Programming. Elsevier, 2012, roč. 77, č. 12, s. 1272-1288. ISSN 0167-6423. Dostupné z: https://dx.doi.org/10.1016/j.scico.2011.03.001. [citováno 2024-04-24] |
Další formáty:
BibTeX
LaTeX
RIS
@article{955939,
author = {Barnat, Jiří and Brim, Luboš and Ročkai, Petr},
article_number = {12},
doi = {http://dx.doi.org/10.1016/j.scico.2011.03.001},
keywords = {Explicit Model Checking; Parallel; On-the-fly; Partial Order Reduction},
language = {eng},
issn = {0167-6423},
journal = {Science of Computer Programming},
title = {On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties},
url = {http://dx.doi.org/10.1016/j.scico.2011.03.001},
volume = {77},
year = {2012}
}
TY - JOUR
ID - 955939
AU - Barnat, Jiří - Brim, Luboš - Ročkai, Petr
PY - 2012
TI - On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties
JF - Science of Computer Programming
VL - 77
IS - 12
SP - 1272-1288
EP - 1272-1288
PB - Elsevier
SN - 01676423
KW - Explicit Model Checking
KW - Parallel
KW - On-the-fly
KW - Partial Order Reduction
UR - http://dx.doi.org/10.1016/j.scico.2011.03.001
N2 - 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.
ER -
BARNAT, Jiří, Luboš BRIM a Petr ROČKAI. On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties. Online. \textit{Science of Computer Programming}. Elsevier, 2012, roč.~77, č.~12, s.~1272-1288. ISSN~0167-6423. Dostupné z: https://dx.doi.org/10.1016/j.scico.2011.03.001. [citováno 2024-04-24]
|
