Robust dynamic programming for temporal logic control of stochastic systems
Robust dynamic programming for temporal logic control of stochastic systems , Sofie Haesaert, Sadegh Soudjani
Abstract: Discrete-time stochastic systems are an essential modelling tool for many engineering systems. We consider stochastic control systems that are evolving over continuous spaces. For this class of models, methods for the formal verification and synthesis of control strategies are computationally hard and generally rely on the use of approximate abstractions. Building on approximate abstractions, we compute control strategies with lower- and upper-bounds for satisfying unbounded temporal logic specifications. Firstly, robust dynamic programming mappings over the abstract system are introduced to solve the control synthesis and verification problem. These mappings yield a control strategy and a unique lower bound on the satisfaction probability for temporal logic specifications that is robust to the incurred approximation errors. Secondly, upper-bounds on the satisfaction probability are quantified, and properties of the mappings are analysed and discussed. Finally, we show the implications of these results to continuous state space of linear stochastic dynamic systems. This abstraction-based synthesis framework is shown to be able to handle infinite-horizon properties.
The abstraction based approach is summarised in the following picture:
The right picture here is a painting of Roy Lichtenstein and illustrates intuitively what it means to abstract continuous states to finite states.