  This paper studies the synthesis of controllers for discrete-time, continuous
state stochastic systems subject to omega-regular specifications using
finite-state abstractions. We present a synthesis algorithm for minimizing or
maximizing the probability that a discrete-time stochastic system with finite
number of modes satisfies an omega-regular property. Our approach uses a
finite-state abstraction of the underlying dynamics in the form of a
Bounded-parameter Markov Decision Process (BMDP) arising from a finite
partition of the system's domain. Such abstractions allow for a range of
transition probabilities between states for each action. Our method analyzes
the product between the abstraction and a Deterministic Rabin Automaton
encoding the specification. Synthesis is decomposed into a qualitative problem,
where the greatest permanent winning components of the product are created, and
a quantitative problem, which requires maximizing the probability of reaching
this component. We propose a metric for the quality of the controller with
respect to the abstracted states and devise a domain partition refinement
technique to reach a quality target. Next, we present a method for computing
controllers for stochastic systems with a continuous input set. The system is
assumed to be affine in input and disturbance, and we derive a technique for
solving the qualitative and quantitative problems in the abstractions of such
systems called Controlled Interval-valued Markov Chains. The greatest permanent
component of such abstractions are found by partitioning the input space to
generate a BMDP accounting for all possible qualitative transitions between
states. Maximizing the probability of reaching this component is cast as an
optimization problem. Quality of the synthesized controller and a refinement
scheme are described for this framework.
