Distributed LTL Model Checking with Hash Compaction

BARNAT, Jiří, Jan HAVLÍČEK and Petr ROČKAI. Distributed LTL Model Checking with Hash Compaction. In Electronic Notes in Theoretical Computer Science, Volume 296. Neuveden: Elsevier Science, 2013, p. 79-93. ISSN 1571-0661. Available from: https://dx.doi.org/10.1016/j.entcs.2013.07.006.

Basic information

Original name

Distributed LTL Model Checking with Hash Compaction

Name in Czech

Distribuované ověřování modelů LTL za pomoci hash compaction

Authors

BARNAT, Jiří (203 Czech Republic, guarantor, belonging to the institution), Jan HAVLÍČEK (203 Czech Republic, belonging to the institution) and Petr ROČKAI (703 Slovakia, belonging to the institution)

Edition

Neuveden, Electronic Notes in Theoretical Computer Science, Volume 296, p. 79-93, 15 pp. 2013

Publisher

Elsevier Science

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Netherlands

Confidentiality degree

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

Publication form

printed version "print"

References:

URL

RIV identification code

RIV/00216224:14330/13:00065988

Organization unit

Faculty of Informatics

ISSN

DOI

http://dx.doi.org/10.1016/j.entcs.2013.07.006

UT WoS

000216919300006

Keywords in English

model checking; LTL; hash compaction

Tags

International impact, Reviewed

---

Abstract

V originále

We extend a distributed-memory explicit-state LTL model checking algorithm (OWCTY) with hash compaction. We provide a detailed description of the improved algorithm and a correctness argument in the theoretical part of the paper. Additionally, we deliver an implementation of the algorithm as part of out parallel and distributed-memory model checker DiVinE, and use this implementation for a practical evaluation of the approach, on which we report in the experimental part of the paper.

In Czech

Rozšiřujeme distribuovaný algoritmus OWCTY pro realizaci verifikační metody enumerativní ověřování modelu o možnost uchovávat navštívené stavy pouze jako jejich otisky z hashovací funkce. Podáváme detailní popis algoritmu a důkaz korektnosti. Součástí výsledku je implementace algoritmu v prostředí verifikačního nástroje DIVINE a experimentální vyhodnocení.

---

Links

GAP202/11/0312, research and development project

Name: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems) Investor: Czech Science Foundation