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

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í

Odkazy

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

V originále

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.

Č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