Synthesis for Stochastic Systems with Temporal Objectives

Max Dutreix, Georgia Tech

Abstract This talk addresses the problem of synthesizing controllers for discrete-time stochastic systems with  complex temporal objectives using finite-state abstractions. Such objectives include, for example, linear temporal logic specifications. First, we describe a procedure for minimizing or maximizing the probability of occurrence of temporal logic behaviors in discrete-time switched stochastic systems with a finite number of modes. Our approach relies on a finite-state abstraction of the underlying dynamics in the form of a Bounded-parameter Markov Decision Process arising from a finite partition of the system’s domain. Additionally, we propose an iterative partition refinement technique so as to reach a user-defined optimality threshold for the designed controller in a more tractable manner than existing techniques. Finally, numerical examples are presented.