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 | |
| 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 | |
| Citace | 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. |
| 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: |