Control synthesis for stochastic systems given automata specifications defined by stochastic sets

The problem of control synthesis to maximize the probability of satisfying automata specifications for systems with uncertainty is addressed. Two types of uncertainty are considered; stochasticity in the dynamical system and in the sets defining the specifications. We model the uncertain dynamical sets as stochastic set processes. We show that the optimal control policy can be computed by solving a reachability problem for a hybrid stochastic system, which evolves on product state spaces of the automaton, stochastic sets, and the dynamical system. We derive an approximation to the stochastic set processes to alleviate the complexity of reachability computation. A case study illustrates the framework and the solution approach.