On Combining Partial Order Reduction with Fairness Assumptions

BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC and Jiří ŠIMŠA. On Combining Partial Order Reduction with Fairness Assumptions. In Proceedings of the 11th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2006). Bonn, Germany: University Bonn, 2006, p. 1-16. ISBN 978-3-540-70951-0.

Basic information

Original name

On Combining Partial Order Reduction with Fairness Assumptions

Name in Czech

Kombinace redukce pomocí reprezentantů s fairness předpoklady

Authors

BRIM, Luboš (203 Czech Republic, guarantor), Ivana ČERNÁ (203 Czech Republic), Pavel MORAVEC (203 Czech Republic) and Jiří ŠIMŠA (203 Czech Republic)

Edition

Bonn, Germany, Proceedings of the 11th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2006), p. 1-16, 2006

Publisher

University Bonn

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

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

RIV identification code

RIV/00216224:14330/06:00015442

Organization unit

Faculty of Informatics

ISBN

978-3-540-70951-0

UT WoS

000245773800006

Keywords in English

partial order reduction; fairness; LTL model checking

Tags

Fairness, LTL model checking, partial order reduction

Tags

International impact, Reviewed

---

Abstract

V originále

We present a new approach to combine partial order reduction with fairness in the context of LTL model checking. For this purpose, we define several behaviour classes representing typical fairness assumptions and examine how various reduction techniques affect these classes. In particular, we consider both reductions preserving all behaviours and reductions preserving only some behaviours.

In Czech

Je prezentován nový přístup kombinace redukce pomocí reprezentantů a fairness podmínek v kontextu ověřování LTL vlastností modelu. Je zadefinováno několik tříd chování popisující typické fairness přepoklady a dokázáno, jak jednotlivé redukční techniky zachovávají tyto třídy. Zejména je uvažován případ, kdy redukce zachovávají všechna chování a redukce zachovávající jen některá z nich.

---

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