Using Accepting Predecessors in Distributed LTL Model-Checking

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky Použití akceptujících předchůdců u distribuovaného ověřování LTL vlastností modelu
Autoři

MORAVEC Pavel

Rok publikování 2004
Druh Článek ve sborníku
Konference MOVEP'04: 6th school on MOdeling and VErifying parallel Processes
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Informatika
Klíčová slova LTL model checking; distributed algorithm
Popis Prezentujeme nový algoritmus s distribuovanou pamětí pro ověřování LTL vlastností modelu, který je navržen pro síť počítačů komunikujících pomocí MPI. Detekce akceptujících cyklů je založena na počítání největších akceptujících předchůdců a na následném rozkladu grafu na nezávislé předchůdcovské podgrafy indukované největšími akceptujícími předchůdci. Vliv uspořádání vrcholů na chování algoritmu je otevřena jako budoucí práce.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.