Certified policy synthesis for general Markov decision processes: An application in building automation systems

In this paper, we present an industrial application of new approximate similarity relations for Markov models, and show that they are key for the synthesis of control strategies. Typically, modern engineering systems are modelled using complex and high-order models which make the correct-by-design controller construction computationally hard. Using the new approximate similarity relations, this complexity is reduced and we provide certificates on the performance of the synthesised policies. The application deals with stochastic models for the thermal dynamics in a “smart building” setup: such building automation system set-up can be described by discrete-time Markov decision processes evolving over an uncountable state space and endowed with an output quantifying the room temperature. The new similarity relations draw a quantitative connection between different levels of model abstraction, and allow to quantitatively refine over complex models control strategies synthesised on simpler ones. 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 develop a software toolbox supporting the application and the computational implementation of these new relations