Developing safe controllers for autonomous systems under uncertainty

We then define abstract actions that correspond to control inputs that cause transitions between these regions. Due to the noise, every action has multiple possible outcomes that all occur with a certain probability. We compute lower and upper bounds (intervals) on these probabilities based on a finite number of observations of the noise. Our abstraction procedure ensures that we obtain a faithful, yet abstract representation of the autonomous system. In fact, this abstraction constitutes a type of Markov decision process, which is the standard type of model in sequential decision making under uncertainty. To analyze our abstract models in a rigorous manner, we use state-of-art tools from an area called formal verification.