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

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

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

Rok uplatnění

2012

Kód důvěrnosti údajů

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

Název periodika

Science of Computer Programming

ISSN

0167-6423

e-ISSN

—

Svazek periodika

77

Číslo periodika v rámci svazku

12

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

17

Strana od-do

1272-1288

Kód UT WoS článku

000308732800004

EID výsledku v databázi Scopus

—