Optimal control of non-deterministic systems for a computationally efficient fragment of temporal logic

We develop a framework for optimal control policy synthesis for non-deterministic transition systems subject to temporal logic specifications. We use a fragment of temporal logic to specify tasks such as safe navigation, response to the environment, persistence, and surveillance. By restricting specifications to this fragment, we avoid a potentially doubly-exponential automaton construction. We compute feasible control policies for non-deterministic transition systems in time polynomial in the size of the system and specification. We also compute optimal control policies for average, minimax (bottleneck), and average cost-per-task-cycle cost functions. We highlight several interesting cases when optimal policies can be computed in time polynomial in the size of the system and specification. Additionally, we make connections between computing optimal control policies for an average cost-per-task-cycle cost function and the generalized traveling salesman problem. We give simulation results for motion planning problems.