Distributed Qualitative LTL Model Checking of Markov Decision Processes

BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA and Jana TŮMOVÁ. Distributed Qualitative LTL Model Checking of Markov Decision Processes. Online. In Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation. Bonn, Germany: University of Bonn, 2006. p. 1-15. ISSN 1571-0661. [citováno 2024-04-23]

Basic information

• Original name: Distributed Qualitative LTL Model Checking of Markov Decision Processes
• Name in Czech: Distribuované kvalitativní LTL ověřování modelu Markovových Rozhodovacích Procesů
• Authors: BARNAT, Jiří (203 Czech Republic, guarantor), Luboš BRIM (203 Czech Republic), Ivana ČERNÁ (203 Czech Republic), Milan ČEŠKA (203 Czech Republic) and Jana TŮMOVÁ (203 Czech Republic)
• Edition: Bonn, Germany, Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation, p. 1-15, 2006.
• Publisher: University of Bonn

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Germany
• Confidentiality degree: is not subject to a state or trade secret
• RIV identification code: RIV/00216224:14330/06:00015450
• Organization unit: Faculty of Informatics
• ISSN: 1571-0661
• Keywords in English: distributed; parallel; LTL model checking; probabilistic systems; MDP
• Tags: distributed, LTL model checking, MDP, parallel, probabilistic systems
• Tags: International impact, Reviewed

Abstract

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.

Abstract (in Czech)

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.

Links

• GA201/06/1338, research and development project: Name: Automatizovaná verifikace softwaru

Investor: Czech Science Foundation, Automated software verification

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• 1ET408050503, research and development project: Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů

Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems

• 1M0545, research and development project: Name: Institut Teoretické Informatiky

Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science