Distributed Qualitative LTL Model Checking of Markov Decision Processes

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