Home > Research > Publications & Outputs > Satisfiability Bounds for ω-Regular Properties ...

Links

Text available via DOI:

View graph of relations

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

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published
Close
Publication date11/12/2019
Host publication2019 IEEE 58th Conference on Decision and Control, CDC 2019
Pages2284-2291
Number of pages8
ISBN (electronic)9781728113982
<mark>Original language</mark>English

Publication series

NameProceedings of the IEEE Conference on Decision and Control
Volume2019-December
ISSN (Print)0743-1546
ISSN (electronic)2576-2370

Abstract

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.