Satisfiability Bounds for ω-Regular Properties in
Bounded-Parameter Markov Decision Processes

D 2019

Satisfiability Bounds for ω-Regular Properties in Bounded-Parameter Markov Decision Processes

WEININGER, Maximilian; Tobias MEGGENDORFER a Jan KŘETÍNSKÝ

Základní údaje

Originální název

Satisfiability Bounds for ω-Regular Properties in Bounded-Parameter Markov Decision Processes

Autoři

WEININGER, Maximilian; Tobias MEGGENDORFER a Jan KŘETÍNSKÝ

Vydání

58th IEEE Conference on Decision and Control, CDC 2019, Nice, France, December 11-13, 2019, od s. 2284-2291, 8 s. 2019

Nakladatel

IEEE

Další údaje

Typ výsledku

Stať ve sborníku

Označené pro přenos do RIV

Organizační jednotka

Fakulta informatiky

ISBN

9781728113982

ISSN

DOI

https://doi.org/10.1109/CDC40024.2019.9029460

Změněno: 17. 3. 2025 14:43, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We consider the problem of computing minimum and maximum probabilities of satisfying an ω-regular property in a bounded-parameter Markov decision process (BMDP). BMDP arise from Markov decision processes (MDP) by allowing for uncertainty on the transition probabilities in the form of intervals where the actual probabilities are unknown. ω-regular languages form a large class of properties, expressible as, e.g., Rabin or parity automata, encompassing rich specifications such as linear temporal logic. In a BMDP the probability to satisfy the property depends on the unknown transitions probabilities as well as on the policy. In this paper, we compute the extreme values. This solves the problem specifically suggested by Dutreix and Coogan in CDC 2018, extending their results on interval Markov chains with no adversary. The main idea is to reinterpret their work as analysis of interval MDP and accordingly the BMDP problem as analysis of an ω-regular stochastic game, where a solution is provided. This method extends smoothly further to bounded-parameter stochastic games.

Citovat

WEININGER, Maximilian; Tobias MEGGENDORFER a Jan KŘETÍNSKÝ. Satisfiability Bounds for ω-Regular Properties in Bounded-Parameter Markov Decision Processes. In 58th IEEE Conference on Decision and Control, CDC 2019, Nice, France, December 11-13, 2019. IEEE, 2019, s. 2284-2291. ISBN 9781728113982. Dostupné z: https://doi.org/10.1109/CDC40024.2019.9029460.

@inproceedings{2484801,
   author = {Weininger, Maximilian and Meggendorfer, Tobias and Křetínský, Jan},
   booktitle = {58th IEEE Conference on Decision and Control, CDC 2019, Nice, France, December 11-13, 2019},
   doi = {https://doi.org/10.1109/CDC40024.2019.9029460},
   isbn = {9781728113982},
   pages = {2284-2291},
   publisher = {IEEE},
   title = {Satisfiability Bounds for ω-Regular Properties in Bounded-Parameter Markov Decision Processes},
   year = {2019}
}

TY  - CONF
ID  - 2484801
AU  - Weininger, Maximilian - Meggendorfer, Tobias - Křetínský, Jan
PY  - 2019
TI  - Satisfiability Bounds for ω-Regular Properties in Bounded-Parameter Markov Decision Processes
PB  - IEEE
SN  - 9781728113982
N2  - We consider the problem of computing minimum and maximum probabilities of satisfying an ω-regular property in a bounded-parameter Markov decision process (BMDP). BMDP arise from Markov decision processes (MDP) by allowing for uncertainty on the transition probabilities in the form of intervals where the actual probabilities are unknown. ω-regular languages form a large class of properties, expressible as, e.g., Rabin or parity automata, encompassing rich specifications such as linear temporal logic. In a BMDP the probability to satisfy the property depends on the unknown transitions probabilities as well as on the policy. In this paper, we compute the extreme values. This solves the problem specifically suggested by Dutreix and Coogan in CDC 2018, extending their results on interval Markov chains with no adversary. The main idea is to reinterpret their work as analysis of interval MDP and accordingly the BMDP problem as analysis of an ω-regular stochastic game, where a solution is provided. This method extends smoothly further to bounded-parameter stochastic games.
ER  -

WEININGER, Maximilian; Tobias MEGGENDORFER a Jan KŘETÍNSKÝ. Satisfiability Bounds for ω-Regular Properties in Bounded-Parameter Markov Decision Processes. In \textit{58th IEEE Conference on Decision and Control, CDC 2019, Nice, France, December 11-13, 2019}. IEEE, 2019, s.~2284-2291. ISBN~9781728113982. Dostupné z: https://doi.org/10.1109/CDC40024.2019.9029460.

Přehled o publikaci