Abstract

We synthesize controllers for discrete-time stochastic hybrid systems such that the probability of satisfying a given specification on the system is maximized. The specifications are defined with finite state automata. It is shown that automata satisfaction is equivalent to a reachability problem in an extended state space consisting of the system and the automaton state spaces. The control policy is defined as a map from this extended state space to the input space. Using existing results on maximizing reachability probability, the control policy is designed to maximize probability of satisfying the specification. Copyright © 2013 ACM.

Details