  In this work, we propose an abstraction and refinement methodology for the
controller synthesis of discrete-time stochastic systems to enforce complex
logical properties expressed by deterministic finite automata (a.k.a. DFA). Our
proposed scheme is based on a notion of so-called
$(\epsilon,\delta)$-approximate probabilistic relations, allowing one to
quantify the similarity between stochastic systems modeled by discrete-time
stochastic games and their corresponding finite abstractions. Leveraging this
type of relations, the lower bound for the probability of satisfying the
desired specifications can be well ensured by refining controllers synthesized
over abstract systems to the original games. Moreover, we propose an
algorithmic procedure to construct such a relation for a particular class of
nonlinear stochastic systems with slope restrictions on the nonlinearity. The
proposed methods are demonstrated on a quadrotor example, and the results
indicate that the desired lower bound for the probability of satisfaction is
guaranteed.
