ABSTRACT
For a dynamical system that evolves over a continuous space under continuous inputs, the computation of controllers is highly nontrivial. In fact, even the reachability problem for low-dimensional dynamical systems without controls is undecidable. On the other hand, for discrete transition systems with omega-regular objectives, one can solve the discrete controller synthesis problem effectively (albeit with high computational complexity). Discrete abstractions serve as a bridge between continuous control and discrete control synthesis problems. This introduces a notion of such abstractions and investigate theoretical guarantees of abstraction-based controller synthesis.
