Verification of general Markov decision processes by approximate similarity relations and policy refinement

TL;DR

This paper introduces new approximate similarity relations for general Markov decision processes with uncountably-infinite states, enabling effective verification and control refinement through metric-based comparisons.

Contribution

It develops novel probabilistic similarity relations based on metrics, facilitating policy synthesis and control refinement for complex MDPs with infinite states.

Findings

New similarity relations enable verification of complex MDPs.

Relations allow trade-offs between probability deviations and output distances.

Effective policy refinement from abstract models demonstrated.

Abstract

In this work we introduce new approximate similarity relations that are shown to be key for policy (or control) synthesis over general Markov decision processes. The models of interest are discrete-time Markov decision processes, endowed with uncountably-infinite state spaces and metric output (or observation) spaces. The new relations, underpinned by the use of metrics, allow in particular for a useful trade-off between deviations over probability distributions on states, and distances between model outputs. We show that the new probabilistic similarity relations, inspired by a notion of simulation developed for finite-state models, can be effectively employed over general Markov decision processes for verification purposes, and specifically for control refinement from abstract models.