How to Cope with Higher Dependency in Partial Order Reduction for LTL Model Checking

MORAVEC, Pavel. How to Cope with Higher Dependency in Partial Order Reduction for LTL Model Checking. In 1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2005). Znojmo, Czech Republic: FI MU Report Series, 2005, s. 186-192.

Základní údaje

• Originální název: How to Cope with Higher Dependency in Partial Order Reduction for LTL Model Checking
• Název česky: Jak se vypořádat s vyšší závislostí v partial order reduction při ověřování LTL vlastností modelu
• Autoři: MORAVEC, Pavel (203 Česká republika, garant).
• Vydání: Znojmo, Czech Republic, 1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2005), s. 186-192, 2005.
• Nakladatel: FI MU Report Series

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í
• WWW: URL
• Kód RIV: RIV/00216224:14330/05:00012706
• Organizační jednotka: Fakulta informatiky
• Klíčová slova anglicky: model checking; partial order reduction; ample sets
• Štítky: ample sets, Model checking, partial order reduction

Anotace

Partial order reduction tries to combat the state space explosion problem by reducing the size of the state space. It is based on exploring only a subset of all possible interleavings of independent concurrent processes. However, even in cases when the dependency among processes is small, the method often fails. The reason is that the heuristics actually used to compute the dependency relation are too rough. In this paper we propose a new method which often overcomes the described bottleneck of partial order reduction.

Anotace česky

Článek navrhuje novou metodu použití techniky partial order reduction v situacích, kdy standardní postup selže kvůli vyšší závislosti v modelu.

Návaznosti

• 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

• 1M0545, projekt VaV: Název: Institut Teoretické Informatiky

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky