Fair Control of Uncertain Dynamical Systems under LTL Specifications

Uncertainties are inevitable for control of dynamical systems of practical relevance. The conventional robust control methods assume persistent worst-case realisations of uncertainties, which leads to conservative solutions. To relax this assumption, we exploit the fairness notion in formal verification to qualitatively capture realistic epistemic disturbance behaviours. We study the fair control problem, that is, to maximise the probability of satisfying an Linear Temporal Logic subject to an action-based fairness constraint for uncertain dynamical systems. The action-based fairness of epistemic disturbances can be defined flexibly: by their observed behaviour and/or by their interaction with control input, enabling both input-dependent and independent disturbance modelling. We develop a sound and complete methodology to perform correct-by-design synthesis. We show that this optimal control problem is equivalent to a reachability problem in the fairness-realisable sub-product Markov decision process. We validate our results over a case study of room temperature regulation.