Synthesis of Pareto-optimal Policies for Continuous-Time Markov Decision Processes

Abstract

We present a work-in-progress method for the synthesis of continuous-time Markov decision process (CTMDP) policies–an important problem not handled by current probabilistic model checkers. The policies synthesised by this method correspond to configurations of software systems or software controllers of cyber-physical systems (CPS) that satisfy predefined nonfunctional constraints and are Pareto-optimal with respect to a set of optimisation objectives. We illustrate the effectiveness of our method by using it to synthesise optimal configurations for a client-server system, and optimal controllers for a driver-attention management CPS.