Distributed Qualitative LTL Model Checking of Markov Decision Processes

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, 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:

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