Paper Info
Title
Satisfiability Bounds for ω-Regular Properties in Bounded-Parameter Markov Decision Processes.
Abstract
We consider the problem of computing minimum and maximum probabilities of satisfying an $\omega$-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. $\omega$-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 $\omega$-regular stochastic game, where a solution is provided. This method extends smoothly further to bounded-parameter stochastic games.
Year
DOI
Venue
2019
10.1109/CDC40024.2019.9029460
CDC
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
0
3
Name
Order
Citations
PageRank
Maximilian Weininger102.70
Tobias Meggendorfer2153.90
Jan Kretínský315916.02