Temporal logic control of nonlinear stochastic systems using a piecewise-affine abstraction

Automatically synthesizing controllers for continuous-state nonlinear stochastic systems, while giving guarantees on the probability of satisfying (infinite-horizon) temporal logic specifications crucially depends on abstractions with a quantified accuracy. For this similarity quantification, approximate stochastic simulation relations are often used. To handle the nonlinearity of the system effectively, we use finite-state abstractions based on piecewise-affine approximations together with tailored simulation relations that leverage the local affine structure. In the end, we synthesize a robust controller for a nonlinear stochastic Van der Pol oscillator