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

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F12%3A00057076" target="_blank" >RIV/00216224:14330/12:00057076 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1016/j.scico.2011.03.001" target="_blank" >http://dx.doi.org/10.1016/j.scico.2011.03.001</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1016/j.scico.2011.03.001" target="_blank" >10.1016/j.scico.2011.03.001</a>

Result language
angličtina
Original language name
On-the-fly Parallel Model Checking Algorithm that is Optimal for Verification of Weak LTL Properties
Original language 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.
Czech name
—
Czech description
—

Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
IN - Informatics
OECD FORD branch
—

Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Publication year
2012
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)