Distributed Explicit Fair Cycle Detection

Result code in IS VaVaI

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

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Distributed Explicit Fair Cycle Detection

Original language description

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.

Czech name

Distributed Explicit Fair Cycle Detection

Czech description

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.

Type

D - Article in proceedings

CEP classification

IN - Informatics

OECD FORD branch

—

Project

<a href="/en/project/GA201%2F03%2F0509" target="_blank" >GA201/03/0509: Automated Verification of Parallel and Distributed Systems</a><br>

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2003

Confidentiality

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

Article name in the collection

SPIN Workshop 2003

ISBN

3-540-40117-2

ISSN

—

e-ISSN

—

Number of pages

25

Pages from-to

—

Publisher name

Springer-Verlag

Place of publication

Portland (Oregon, USA)

Event location

Portland

Event date

Jan 1, 2003

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000183490400004