On Combining Partial Order Reduction with Fairness Assumptions

BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a 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, s. 1-16. ISBN 978-3-540-70951-0.

Základní údaje

Originální název

On Combining Partial Order Reduction with Fairness Assumptions

Název česky

Kombinace redukce pomocí reprezentantů s fairness předpoklady

Autoři

BRIM, Luboš (203 Česká republika, garant), Ivana ČERNÁ (203 Česká republika), Pavel MORAVEC (203 Česká republika) a Jiří ŠIMŠA (203 Česká republika)

Vydání

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

Nakladatel

University Bonn

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Kód RIV

RIV/00216224:14330/06:00015442

Organizační jednotka

Fakulta informatiky

ISBN

978-3-540-70951-0

UT WoS

000245773800006

Klíčová slova anglicky

partial order reduction; fairness; LTL model checking

Štítky

Fairness, LTL model checking, partial order reduction

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

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.

Česky

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.

---

Návaznosti

GA201/06/1338, projekt VaV	Název: Automatizovaná verifikace softwaru Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
GD102/05/H050, projekt VaV	Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET408050503, projekt VaV	Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky