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

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F08%3A00024825" target="_blank" >RIV/00216224:14330/08:00024825 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

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

Original language description

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.

Czech name

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

Czech description

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.

Type

D - Article in proceedings

CEP classification

IN - Informatics

OECD FORD branch

—

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

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

Publication year

2008

Confidentiality

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

Article name in the collection

Automata, Languages and Programming. 35th International Colloquium, ICALP 2008. Reykjavik, Iceland, July 2008. Proceedings, Part II.

ISBN

3-540-70582-1

ISSN

—

e-ISSN

—

Number of pages

12

Pages from-to

—

Publisher name

Springer

Place of publication

Berlin, Heidelberg, New York

Event location

Reykjavik, Iceland

Event date

Jul 7, 2008

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

00025766310