  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).
