Parallel Partial Order Reduction with Topological Sort Proviso

BARNAT, Jiří, Luboš BRIM a 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, s. 222-231. ISBN 978-0-7695-4153-2.

Základní údaje

Originální název

Parallel Partial Order Reduction with Topological Sort Proviso

Název česky

Paralelní redukce částečného uspořádání s využitím topologického třídění

Autoři

BARNAT, Jiří (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí) a Petr ROČKAI (703 Slovensko, domácí)

Vydání

Los Alamos, Software Engineering and Formal Methods (SEFM 2010), od s. 222-231, 10 s. 2010

Nakladatel

IEEE Computer Society Press

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Itálie

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Kód RIV

RIV/00216224:14330/10:00045912

Organizační jednotka

Fakulta informatiky

ISBN

978-0-7695-4153-2

Klíčová slova česky

LTL ověřování modelu; Redukce čístečného uspořádání; Paralelní a distribuované výpočty; DiVinE

Klíčová slova anglicky

LTL Model Checking; Partial Order Reduction; Parallel and Distributed Processing; DiVinE

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

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.

Česky

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.

---

Návaznosti

GA201/09/1389, projekt VaV	Název: Verifikace a analýza velmi velkých počítačových systémů Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačových systémů
GP201/09/P497, projekt VaV	Název: Automatizovaná formální verifikace s využitím soudobého hardware Investor: Grantová agentura ČR, Automatizovaná formální verifikace s využitím soudobého hardware
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
MUNI/A/0914/2009, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV) Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky