Temporal logic control of general Markov decision processes by approximate policy refinement

TL;DR

This paper presents a method for controlling general Markov decision processes to satisfy temporal logic specifications by using approximate relations and robust satisfaction, enabling effective verification on abstract models.

Contribution

It introduces a robust satisfaction framework for approximate control of gMDPs, allowing properties verified on abstractions to hold on original models.

Findings

Robust satisfaction ensures control strategies are valid despite model deviations.

Verification on abstract models guarantees property satisfaction on original models.

The approach reduces computational complexity for uncountable state spaces.

Abstract

The formal verification and controller synthesis for Markov decision processes that evolve over uncountable state spaces are computationally hard and thus generally rely on the use of approximations. In this work, we consider the correct-by-design control of general Markov decision processes (gMDPs) with respect to temporal logic properties by leveraging approximate probabilistic relations between the original model and its abstraction. We newly work with a robust satisfaction for the construction and verification of control strategies, which allows for both deviations in the outputs of the gMDPs and in the probabilistic transitions. The computation is done over the reduced or abstracted models, such that when a property is robustly satisfied on the abstract model, it is also satisfied on the original model with respect to a refined control strategy.