Using Accepting Predecessors in Distributed LTL Model-Checking

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	MORAVEC, Pavel. Using Accepting Predecessors in Distributed LTL Model-Checking. In MOVEP'04: 6th school on MOdeling and VErifying parallel Processes. Bruxelles, Belgium: Universite Libre de Bruxelles, 2004, s. 122-129, 7 s.
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:	Automatizovaná verifikace paralelních a distribuovaných systémů Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů