Distributed Qualitative LTL Model Checking of Markov Decision Processes

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Název česky	Distribuované kvalitativní LTL ověřování modelu Markovových Rozhodovacích Procesů
Autoři	BARNAT Jiří BRIM Luboš ČERNÁ Ivana ČEŠKA Milan TŮMOVÁ Jana
Rok publikování	2006
Druh	Článek ve sborníku
Konference	Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	distributed; parallel; LTL model checking; probabilistic systems; MDP
Popis	U systémů s pravděpodobnostním chováním je problém stavové exploze ještě citelnější než u běžně používaných nedetermistických systémů. Článek popisuje klastrový paralelní algoritmus pro ověřování LTL vlastností konečně stavových provděpodobnostních systémů, který staví na redukci problému na problém detekce akceptující ergodické komponenty v grafu. AE komponentu lze odhalit opakovaným prováděním prohledávání grafu. Unikátní vlastností algoritmu je, že na rozdíl od detekce obyčejných akceptujících komponent při detekci ergodických akceptujících komponent nenarůstá paralelizací asymtotická složitost.
Související projekty:	Techniky automatické verifikace a validace softwarových a hardwarových systémů Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy Automatizovaná verifikace softwaru