Distributed Qualitative LTL Model Checking of Markov Decision Processes

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.

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

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

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

---

Anotace

V originále

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.

Č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 VaV	Název: Automatizovaná verifikace softwaru Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET408050503, projekt VaV	Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky