D 2010

Parallel Partial Order Reduction with Topological Sort Proviso

BARNAT, Jiří, Luboš BRIM and Petr ROČKAI

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

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.

Abstract

ORIG CZ

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
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
Displayed: 18/10/2024 15:30