Symbolic models for stochastic control systems without stability assumptions

Symbolic approaches provide a mechanism to construct discrete and possibly finite abstractions of continuous control systems. Discrete abstractions are in turn amenable to automata-theoretic techniques targeted at the construction of controllers satisfying complex specifications that would be difficult to enforce over continuous models with conventional control design methods. Although the construction of discrete abstractions has been extensively studied for non-probabilistic continuous-time control systems, it has received scant attention on their stochastic counterparts. In this paper, we propose an abstraction technique that is applicable to any stochastic continuous-time control system, as long as we are only interested in its behavior over a compact set. The effectiveness of the proposed results is illustrated with the synthesis of a controller for a jet engine model, which is not stable, is affected by noise, and is subject to a schedulability constraint expressed by a finite automaton.