D 2005

On the Controller Synthesis for Finite-State Markov Decision Processes

KUČERA, Antonín a Oldřich STRAŽOVSKÝ

Základní údaje

Originální název

On the Controller Synthesis for Finite-State Markov Decision Processes

Název česky

O syntéze řídících jednotek pro Markovovy rozhodovací procesy s konečně mnoha stavy

Autoři

KUČERA, Antonín (203 Česká republika, garant) a Oldřich STRAŽOVSKÝ (203 Česká republika)

Vydání

Berlin Heidelberg New York, 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, od s. 541-552, 12 s. 2005

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Kód RIV

RIV/00216224:14330/05:00012780

Organizační jednotka

Fakulta informatiky

ISBN

3-540-30495-9

UT WoS

000234885800044

Klíčová slova anglicky

Controller Synthesis; Markov Decision Processes

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 30. 3. 2010 20:22, prof. RNDr. Antonín Kučera, Ph.D.

Anotace

V originále

We study the problem of effective controller synthesis for finite-state Markov decision processes (MDPs) and the class of properties definable in the logic PCTL extended with long-run average propositions. We show that the existence of such a controller is decidable, and we give an algorithm which computes the controller if it exists. We also address the issue of ``controller robustness'', i.e., the problem whether there is a controller which still guarantees the satisfaction of a given property when the probabilities in the considered MDP slightly deviate from their original values. From a practical point of view, this is an important aspect since the probabilities are often determined empirically and hence they are inherently imprecise. We show that the existence of robust controllers is also decidable, and that such controllers are effectively computable if they exist. .

Česky

V článku je studována problematika efektivní syntézy řídících jednotek pro Markovovy rozhodovací procesy s konečně mnoha stavy a třídu vlastností definovatelných v logice PCTL rozšířené o limitní vlastnosti běhů. Je dokázáno, že problém existence takových řídících jednotek je rozhodnutelný a je podán algoritmus pro jejich konstrukci. Je také podrobněji rozebrána otázka stability řídících jednotek.

Návaznosti

GA201/03/1161, projekt VaV
Název: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM0021622419, záměr
Název: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaV
Název: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky