Using Accepting Predecessors in Distributed LTL Model-Checking

• 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
• 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ů