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áš; 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
• 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

• Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
• Institut Teoretické Informatiky
• Vysoce paralelní a distribuované výpočetní systémy