Data-Driven Interval MDP Abstraction for Formal Control of Stochastic Nonlinear Systems
A technique that abstracts a discrete-time nonlinear system with additive stochastic noise into a finite-state interval Markov decision process using only sample access to the dynamics and noise. Backward reachable sets are underapproximated from forward simulations, and transition-probability intervals are Clopper-Pearson confidence intervals, so each interval carries a probably-approximately-correct guarantee. Policies synthesized on the abstraction satisfy a reach-avoid objective on the concrete system with PAC guarantees despite unknown dynamics.
Proceedings of Machine Learning Research vol 283:1–22, 2025 7th Annual Conference on Learning for
A data-driven method for synthesizing provably correct control policies for discrete-time nonlinear systems with additive stochastic noise whose dynamics and noise distribution are only accessible th…