Formal abstractions enable autonomous decision-making of dynamical systems to achieve complex tasks and compute a holistic reference on controllable regions of initial conditions (winning sets) with quantifiable errors. We develop abstraction analysis and computation tools for stochastic formal verification and control synthesis.
