Distributed Qualitative LTL Model Checking of Markov Decision Processes

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F06%3A00015450" target="_blank" >RIV/00216224:14330/06:00015450 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Distributed Qualitative LTL Model Checking of Markov Decision Processes

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Distributed Qualitative LTL Model Checking of Markov Decision Processes

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2006

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of 5th International Workshop on Parallel and Distributed Methods in verifiCation

ISBN

—

ISSN

1571-0661

e-ISSN

—

Počet stran výsledku

15

Strana od-do

—

Název nakladatele

University of Bonn

Místo vydání

Bonn, Germany

Místo konání akce

Bonn

Datum konání akce

1. 1. 2006

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—