Controller Synthesis for Markov Decision Processes with Branching-Time Objectives
| Autoři | |
|---|---|
| Rok publikování | 2009 |
| Druh | Účelové publikace |
| Fakulta / Pracoviště MU | |
| Citace | |
| Popis | Tato práce obsahuje výsledky z oblasti syntézy plánovačů pro konečněstavové Markovovy rozhodovací procesy a logiky větvícího se času. Markovovův rozhodovací proces je pravděpodobnostní systém často využívaný při modelování skutečných systémů, ve kterých se vyskytuje jak nedeterministické, tak pravděpodobnostní chování. Logiky větvícího se času umožňují vyjádřit požadované vlastnosti těchto systémů. Problém syntézy plánovačů je definován následovně: Je dán Markovův rozhodovací proces a formule logiky větvícího se času; existuje plánovač, který zajistí splnění formule? V této práci se zabýváme i problémem verifikace, který je definován duálně, t.j. cílem je zjistit, zda je formule splněna pro všechny plánovače. Omezením množství paměti anebo použití náhodnosti u plánovačů, případně použitím různých logik lze obdržet různé varianty problému. Hlavním cílem této disertace je poskytnout přehled o aktuálních výsledcích z oblasti. Uvážíme logiky PCTL, PCTL* a PECTL*. První dvě logiky jsou varianty nepravděpodobnostních a široce využívaných logik CTL a CTL*, třetí z logik využívá Büchiho automaty místo běžných temporálních operátorů. Ukážeme, že problém syntézy plánovačů je nerozhodnutelný i v případě, že formule, která má být splněna, je formule logiky PCTL, a plánovače nesmí využívat náhodnost a mají k disposici jen konečně mnoho paměti. Zároveň ale najdeme několik rozhodnutelných a prakticky motivovaných podproblémů. Klasifikujeme známé výsledky v oblasti bezpaměťových plánovačů pro PCTL formule a rozšíříme tyto výsledky i na ostatní logiky. Dále se zaměříme na kvalitativní fragmenty logik a ukážeme, že plánovače mohou vyžadovat "nekonečnou" pamět v podobě potenciálně neomezeného čítače. Ukážeme, že paměť poskytovaná konečným automatem rozšířeným o čítač je ve skutečnosti dostačující a že problém syntézy plánovačů je pro kvalitativní logiky rozhodnutelný. |
| Související projekty: |