Relaxed Cycle Condition Improves Partial Order Reduction

MORAVEC, Pavel a Jiří ŠIMŠA. Relaxed Cycle Condition Improves Partial Order Reduction. In 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007). Znojmo, Czech Republic: FI MU, FIT VUT. s. 140-147. ISBN 978-80-7355-077-6. 2007.

Základní údaje

• Originální název: Relaxed Cycle Condition Improves Partial Order Reduction
• Název česky: Oslabení podmínky na cykly zlepšující redukci pomocí reprezentantů
• Autoři: MORAVEC, Pavel (203 Česká republika, garant) a Jiří ŠIMŠA (203 Česká republika).
• Vydání: Znojmo, Czech Republic, 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007), s. 140-147, 2007.
• Nakladatel: FI MU, FIT VUT

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Česká republika
• Utajení: není předmětem státního či obchodního tajemství
• Kód RIV: RIV/00216224:14330/07:00019497
• Organizační jednotka: Fakulta informatiky
• ISBN: 978-80-7355-077-6
• Klíčová slova anglicky: model checking; partial order reduction; proviso checking
• Štítky: Model checking, partial order reduction, proviso checking

Anotace

Partial order reduction is a method widely used for tackling the state space explosion problem. In this paper we focus on a theoretical refinement of a particular instance of the partial order reduction which is nowadays an inherent part of most tools for explicit state model checking of Linear Temporal Logic. This particular instance is represented as a set of conditions C0 through C3 which describe valid reductions of a state space. We propose a hierarchy of alternatives to the cycle condition C3. In this hierarchy we point out which alternatives guarantee a valid reduction with respect to LTL_X properties.

Anotace česky

Redukce pomocí reprezentantů je metoda široce používaná na boj se stavovou explozí. V článku se zaměřujeme na teoretické zjemnění konkrétní instance této redukce pro logiku LTL. Tato instance je representována množinou podmínek C0 až C3 které popisují platné redukce stavového prostoru. Navrhujeme hierarchii alternativ k podmínce C3. V této hierarchii ukážeme které alternativy k C3 garantují platnou redukci vzhledem k LTL vlastnostem.

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