Correct-by-construction reach-avoid control of partially observable linear stochastic systems

TL;DR

This paper presents a correct-by-construction control synthesis method for partially observable stochastic linear systems, ensuring reach-avoid objectives with probabilistic guarantees using finite-state abstractions and Kalman filters.

Contribution

It introduces a novel abstraction-based approach that combines Kalman filtering with interval MDPs for robust probabilistic control synthesis in partially observable stochastic systems.

Findings

Successfully handles systems with up to 6D state spaces.

Outperforms RRBT in systems with control input constraints.

Provides probabilistic guarantees for reach-avoid objectives.

Abstract

We study feedback controller synthesis for reach-avoid control of discrete-time, linear time-invariant (LTI) systems with Gaussian process and measurement noise. The problem is to compute a controller such that, with at least some required probability, the system reaches a desired goal state in finite time while avoiding unsafe states. Due to stochasticity and nonconvexity, this problem does not admit exact algorithmic or closed-form solutions in general. Our key contribution is a correct-by-construction controller synthesis scheme based on a finite-state abstraction of a Gaussian belief over the unmeasured state, obtained using a Kalman filter. We formalize this abstraction as a Markov decision process (MDP). To be robust against numerical imprecision in approximating transition probabilities, we use MDPs with intervals of transition probabilities. By construction, any policy on the abstraction can be refined into a piecewise linear feedback controller for the LTI system. We prove that the closed-loop LTI system under this controller satisfies the reach-avoid problem with at least the required probability. The numerical experiments show that our method is able to solve reach-avoid problems for systems with up to 6D state spaces, and with control input constraints that cannot be handled by methods such as the rapidly-exploring random belief trees (RRBT).