Detailed Information on Publication Record
2010
Parallel Partial Order Reduction with Topological Sort Proviso
BARNAT, Jiří, Luboš BRIM and Petr ROČKAIBasic information
Original name
Parallel Partial Order Reduction with Topological Sort Proviso
Name in Czech
Paralelní redukce částečného uspořádání s využitím topologického třídění
Authors
BARNAT, Jiří (203 Czech Republic, guarantor, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution) and Petr ROČKAI (703 Slovakia, belonging to the institution)
Edition
Los Alamos, Software Engineering and Formal Methods (SEFM 2010), p. 222-231, 10 pp. 2010
Publisher
IEEE Computer Society Press
Other information
Language
English
Type of outcome
Stať ve sborníku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Italy
Confidentiality degree
není předmětem státního či obchodního tajemství
Publication form
printed version "print"
RIV identification code
RIV/00216224:14330/10:00045912
Organization unit
Faculty of Informatics
ISBN
978-0-7695-4153-2
Keywords (in Czech)
LTL ověřování modelu; Redukce čístečného uspořádání; Paralelní a distribuované výpočty; DiVinE
Keywords in English
LTL Model Checking; Partial Order Reduction; Parallel and Distributed Processing; DiVinE
Tags
International impact, Reviewed
Změněno: 18/2/2013 12:44, RNDr. Petr Ročkai, Ph.D.
V originále
Partial order reduction and distributed-memory processing are the two essential techniques to fight the wellknown state space explosion problem in explicit state model checking. Unfortunately, these two techniques have not been integrated yet to a satisfactory degree. The main source of difficulties is the cycle proviso that requires one fully expanded state on every cycle in the reduced state space graph. In this paper we suggest a new technique that guarantees correct construction of the reduced state space graph w.r.t. the cycle proviso. Our new technique is fully compatible with the parallel graph traversal procedure while at the same time it provides competitive reduction of the state space if compared to the serial case. The new technique has been implemented within the parallel and distributed-memory LTL model checker DIVINE and its performance is reported in this paper.
In Czech
Redukce částečného uspořádání a počítáni v distribuované paměti jsou dvě klíčové techniky pro boj se stavovou explozí v kontextu enumerativní verifikace. Hlavním výsledkem této práce je nový paralelní algoritmus pro výpočet množiny vrcholů pokrývající všechny cykly v grafu, který umožňuje uspokojivou integraci obou klíčových technik. Nová technika byla implementována v rámci nástroje DiVinE.
Links
GA201/09/1389, research and development project |
| ||
GP201/09/P497, research and development project |
| ||
MSM0021622419, plan (intention) |
| ||
MUNI/A/0914/2009, interní kód MU |
| ||
1M0545, research and development project |
|