Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives

BRÁZDIL, Tomáš, Vojtěch FOREJT a Antonín KUČERA. Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives. In Automata, Languages and Programming. 35th International Colloquium, ICALP 2008. Reykjavik, Iceland, July 2008. Proceedings, Part II. Berlin, Heidelberg, New York: Springer, 2008, s. 148-159. ISBN 3-540-70582-1.

Základní údaje

Originální název

Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives

Název česky

Verifikace a syntéza řídících jednotek pro Markovovy rozhodovací procesy s kvalitativními vlastnostmi větvícího se času

Autoři

BRÁZDIL, Tomáš (203 Česká republika), Vojtěch FOREJT (203 Česká republika) a Antonín KUČERA (203 Česká republika, garant)

Vydání

Berlin, Heidelberg, New York, Automata, Languages and Programming. 35th International Colloquium, ICALP 2008. Reykjavik, Iceland, July 2008. Proceedings, Part II. od s. 148-159, 12 s. 2008

Nakladatel

Springer

---

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/08:00024825

Organizační jednotka

Fakulta informatiky

ISBN

3-540-70582-1

UT WoS

000257663100013

Klíčová slova anglicky

Markov decision processes; Probabilistic Temporal Logics

Štítky

Markov decision processes, probabilistic temporal logics

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

We show that the controller synthesis and verification problems for Markov decision processes with qualitative PECTL* objectives are 2-EXPTIME complete. More precisely, the algorithms are polynomial in the size of a given Markov decision process and doubly exponential in the size of a given qualitative PECTL* formula. Moreover, we show that if a given qualitative PECTL* objective is achievable by some strategy, then it is also achievable by an effectively constructible one-counter strategy, where the associated complexity bounds are essentially the same as above. For the fragment of qualitative PCTL objectives, we obtain EXPTIME completeness and the algorithms are only singly exponential in the size of the formula.

Česky

V článku je dokázáno, že problém verifikace i problém efektivní syntézy řídící jednotky pro Markovovy rozhodovací procesy s kvalitativními PCTL* vlastnostmi je 2-EXPTIME úplný. Příslušné algoritmy jsou polynomiální ve velikosti daného Markovova rozhodovacího procesu a exponenciální ve velikosti dané PCTL* formule. Dále je ukázáno, že lze-li danou PCTL* vlastnost vynutit pomocí nějaké řídící jednotky, pak ji lze vynutit také pomocí řídící jednotky popsatelné automatem s jedním čítačem, který lze navíc algoritmicky sestrojit.

---

Návaznosti

GD102/05/H050, projekt VaV	Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
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
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky