Discrete abstraction of stochastic nonlinear systems: a bisimulation function approach.