  We consider the problem of computing the maximal probability of satisfying an
$\omega$-regular specification for stochastic, continuous-state, nonlinear
systems evolving in discrete time. The problem reduces, after
automata-theoretic constructions, to finding the maximal probability of
satisfying a parity condition on a (possibly hybrid) state space. While
characterizing the exact satisfaction probability is open, we show that a lower
bound on this probability can be obtained by (I) computing an
under-approximation of the qualitative winning region, i.e., states from which
the parity condition can be enforced almost surely, and (II) computing the
maximal probability of reaching this qualitative winning region. The heart of
our approach is a technique to symbolically compute the under-approximation of
the qualitative winning region in step (I) via a finite-state abstraction of
the original system as a $2\frac{1}{2}$-player parity game. Our abstraction
procedure uses only the support of the probabilistic evolution; it does not use
precise numerical transition probabilities. We prove that the winning set in
the abstract $2\frac{1}{2}$-player game induces an under-approximation of the
qualitative winning region in the original synthesis problem, along with a
policy to solve it. By combining these contributions with (a) existing symbolic
fixpoint algorithms to solve $2\frac{1}{2}$-player games and (b) existing
techniques for reachability policy synthesis in stochastic nonlinear systems,
we get an abstraction-based symbolic algorithm for finding a lower bound on the
maximal satisfaction probability. We have implemented our approach and
evaluated it on the nonlinear model of the perturbed Dubins vehicle.
