BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA a Jana TŮMOVÁ. Distributed Qualitative LTL Model Checking of Markov Decision Processes. In Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation. Bonn, Germany: University of Bonn, 2006. s. 1-15. ISSN 1571-0661.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název 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ří (203 Česká republika, garant), Luboš BRIM (203 Česká republika), Ivana ČERNÁ (203 Česká republika), Milan ČEŠKA (203 Česká republika) a Jana TŮMOVÁ (203 Česká republika).
Vydání Bonn, Germany, Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation, s. 1-15, 2006.
Nakladatel University of Bonn
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/06:00015450
Organizační jednotka Fakulta informatiky
ISSN 1571-0661
Klíčová slova anglicky distributed; parallel; LTL model checking; probabilistic systems; MDP
Štítky distributed, LTL model checking, MDP, parallel, probabilistic systems
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnila: prof. RNDr. Ivana Černá, CSc., učo 1419. Změněno: 31. 3. 2010 15:39.
Anotace
Markov decision processes are used to model concurrent programs that exhibit uncertainty. The state explosion problem for probabilistic systems is more critical than in the non-probabilistic case. In the paper we propose a cluster-based algorithm for qualitative LTL model checking of finite state Markov decision processes. We use the automata approach which reduces the model checking problem to the question of existence of an accepting end component. The algorithm uses repeated reachability which systematically eliminates states that cannot belong to any accepting end component. A distinguished feature of the distributed algorithm is that its complexity meets the complexity of the best known sequential algorithm.
Anotace česky
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.
Návaznosti
GA201/06/1338, projekt VaVNázev: Automatizovaná verifikace softwaru
Investor: Grantová agentura ČR, Standardní projekty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 25. 9. 2020 02:24