Experimental Comparison of Algorithms Checking Proviso for Partial Order Reduction

MORAVEC, Pavel. Experimental Comparison of Algorithms Checking Proviso for Partial Order Reduction. In 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006). Mikulov, Czech Republic: FI MU Report Series, 2006, p. 129-136.

Basic information

Original name

Experimental Comparison of Algorithms Checking Proviso for Partial Order Reduction

Name in Czech

Experimentální porovnání algoritmů ověřujících proviso pro redukci pomocí reprezentantů

Authors

MORAVEC, Pavel (203 Czech Republic, guarantor)

Edition

Mikulov, Czech Republic, 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), p. 129-136, 2006

Publisher

FI MU Report Series

---

Other information

Language

English

Type of outcome

Proceedings paper

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

is not subject to a state or trade secret

RIV identification code

RIV/00216224:14330/06:00015445

Organization unit

Faculty of Informatics

Keywords in English

model checking; partial order reduction; proviso checking

Tags

Model checking, partial order reduction, proviso checking

---

Abstract

In the original language

In this paper we have summed up all known algorithms checking proviso for partial order reduction in LTL model checking. All mentioned algorithms have been implemented and experimentally evaluated on a large collection of models. Experiments mostly confirmed theoretical expectations of algorithms comparison.

In Czech

Článek shrnuje všechny známé algoritmy pro ověřování provisa u redukce pomocí reprezentantů pro ověřování LTL vlastností modelu. Všechny zmíněné algoritmy byly implementovány a experimentálně vyhodnoceny na rozsáhlé sbírce modelů. Experimenty ve většině případů potvrdily teoretická očekávání z porovnání algoritmů.

---

Links

GA201/06/1338, research and development project	Name: Automatizovaná verifikace softwaru Investor: Czech Science Foundation, Automated software verification
GD102/05/H050, research and development project	Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems
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
1ET408050503, research and development project	Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science