Mixing Probabilistic and non-Probabilistic Objectives in Markov Decision Processes
This work addresses a theoretical problem in formal verification and control synthesis for systems with probabilistic and non-probabilistic requirements, but it appears incremental as it builds on existing MDP and omega-regular property frameworks.
The paper tackles the problem of deciding the existence of strategies in Markov Decision Processes (MDPs) for Boolean combinations of omega-regular objectives under various probability constraints, and provides algorithms and complexity bounds for solving these cases.
In this paper, we consider algorithms to decide the existence of strategies in MDPs for Boolean combinations of objectives. These objectives are omega-regular properties that need to be enforced either surely, almost surely, existentially, or with non-zero probability. In this setting, relevant strategies are randomized infinite memory strategies: both infinite memory and randomization may be needed to play optimally. We provide algorithms to solve the general case of Boolean combinations and we also investigate relevant subcases. We further report on complexity bounds for these problems.