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

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
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áš FOREJT Vojtěch KUČERA Antonín

Rok publikování 2008
Druh Článek ve sborníku
Konference Automata, Languages and Programming. 35th International Colloquium, ICALP 2008. Reykjavik, Iceland, July 2008. Proceedings, Part II.
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Obor Informatika
Klíčová slova Markov decision processes; Probabilistic Temporal Logics
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.