Satisfiability Bounds for $\omega$-Regular Properties in Bounded-Parameter Markov Decision Processes

TL;DR

This paper develops methods to compute the bounds on the probability of satisfying complex omega-regular properties in bounded-parameter Markov decision processes, addressing uncertainty in transition probabilities.

Contribution

It introduces a novel approach to analyze omega-regular properties in BMDPs by framing the problem as an omega-regular stochastic game, extending previous results on interval Markov chains.

Findings

Computed extreme satisfaction probabilities for omega-regular properties in BMDPs.

Extended analysis to bounded-parameter stochastic games.

Provided a solution to a problem posed by Dutreix and Coogan in 2018.

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.