ČERNÁ, Ivana and Radek PELÁNEK. Distributed Explicit Fair Cycle Detection. In SPIN Workshop 2003. Portland (Oregon, USA): Springer-Verlag, 2003, p. 49-74, 25 pp. ISBN 3-540-40117-2.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Distributed Explicit Fair Cycle Detection
Authors ČERNÁ, Ivana (203 Czech Republic, guarantor) and Radek PELÁNEK (203 Czech Republic).
Edition Portland (Oregon, USA), SPIN Workshop 2003, p. 49-74, 25 pp. 2003.
Publisher Springer-Verlag
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/03:00008589
Organization unit Faculty of Informatics
ISBN 3-540-40117-2
UT WoS 000183490400004
Keywords in English distributed model checking; cycle detection
Tags cycle detection, distributed model checking
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Ivana Černá, CSc., učo 1419. Changed: 8/6/2009 16:11.
Abstract
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-first search based algorithms. Experimental results confirm that our approach outperforms that based on a direct implementation of the best sequential algorithm.
Links
GA201/03/0509, research and development projectName: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed Systems
MSM 143300001, plan (intention)Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing
PrintDisplayed: 25/4/2024 03:37