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

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Germany
• Confidentiality degree: is not subject to a state or trade secret
• 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

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.

Abstract (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