Dealing with non-determinism in symbolic control

Abstract. Abstractions (also called symbolic models) are simple descriptions of continuous and hybrid systems that can be used in analysis and control. They are usually constructed in the form of transition systems with finitely many states. Such abstractions offer a very attractive approach to deal with complexity, while at the same time allowing for rich specification languages. Recent results show that, through the abstraction process, the resulting transition systems can be non-deterministic (i.e., if an input is applied in a state, several next states are possible). However, the problem of controlling a nondeterministic transition system from a rich specification such as a temporal logic formula is not well understood. In this paper, we develop a control strategy for a nondeterministic transition system from a specification given as a Linear Temporal Logic formula with a determin-istic Büchi generator. Our algorithm is inspired from (infinite) LTL games on graphs, is complete, and scales polynomially with the size of the Büchi automa-ton. An example of controlling a linear system from a specification given as a temporal logic formula over the regions of its triangulated state space is included for illustration.