Informace o publikaci
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 | |
| 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: |