Distributed Explicit Fair Cycle Detection

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F03%3A00009022" target="_blank" >RIV/00216224:14330/03:00009022 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/00216224:14330/03:00008589

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Distributed Explicit Fair Cycle Detection

Popis výsledku v původním jazyce

The fair cycle detection problem is at the heart of both LTL and fair CTL model checking. This paper presents a new distributed scalable algorithm for explicit fair cycle detection. Our method combines the simplicity of the distribution of explicitly presented data structure and the features of symbolic algorithm allowing for an efficient parallelisation. If a fair cycle (i.e. counterexample) is detected, then the algorithm produces a cycle, which is in general shorter than that produced by depth-firstsearch based algorithms. Experimental results confirm that our approach outperforms that based on a direct implementation of the best sequential algorithm.

Název v anglickém jazyce

Distributed Explicit Fair Cycle Detection

Popis výsledku anglicky

The fair cycle detection problem is at the heart of both LTL and fair CTL model checking. This paper presents a new distributed scalable algorithm for explicit fair cycle detection. Our method combines the simplicity of the distribution of explicitly presented data structure and the features of symbolic algorithm allowing for an efficient parallelisation. If a fair cycle (i.e. counterexample) is detected, then the algorithm produces a cycle, which is in general shorter than that produced by depth-firstsearch based algorithms. Experimental results confirm that our approach outperforms that based on a direct implementation of the best sequential algorithm.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GA201%2F03%2F0509" target="_blank" >GA201/03/0509: Automatizovaná verifikace paralelních a distribuovaných systémů</a><br>

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2003

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 statě ve sborníku

SPIN Workshop 2003

ISBN

0302-9743

ISSN

—

e-ISSN

—

Počet stran výsledku

25

Strana od-do

49-74

Název nakladatele

Springer-Verlag

Místo vydání

Portland (Oregon, USA)

Místo konání akce

Portland

Datum konání akce

1. 1. 2003

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—