Parallel Partial Order Reduction with Topological Sort Proviso
BARNAT, Jiří, Luboš BRIM and Petr ROČKAI. Parallel Partial Order Reduction with Topological Sort Proviso. In Software Engineering and Formal Methods (SEFM 2010). Los Alamos: IEEE Computer Society Press, 2010, p. 222-231. ISBN 978-0-7695-4153-2. |
Other formats:
BibTeX
LaTeX
RIS
|
Basic 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 | |
---|---|
Original language | English |
Type of outcome | Proceedings paper |
Field of Study | 10201 Computer sciences, information science, bioinformatics |
Country of publisher | Italy |
Confidentiality degree | is not subject to a state or trade secret |
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 |
Changed by | Changed by: RNDr. Petr Ročkai, Ph.D., učo 139761. Changed: 18/2/2013 12:44. |
Abstract |
---|
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. |
Abstract (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 | Name: Verifikace a analýza velmi velkých počítačových systémů |
Investor: Czech Science Foundation, Verification and Analysis of Large-Scale Computer Systems | |
GP201/09/P497, research and development project | Name: Automatizovaná formální verifikace s využitím soudobého hardware |
Investor: Czech Science Foundation, Automated formal verification using modern hardware | |
MSM0021622419, plan (intention) | Name: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems | |
MUNI/A/0914/2009, interní kód MU | Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV) |
Investor: Masaryk University, Category A | |
1M0545, research and development project | Name: Institut Teoretické Informatiky |
Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science |
PrintDisplayed: 15/8/2024 02:25