Correct, Reactive, High-Level Robot Control

In this article, we presented an overview of how temporal logic synthesis, coupled with abstractions and continuous bisimilar controllers, can be used to generate high-level, reactive robot control. We illustrated the ideas using the DUC mission, and we presented two approaches to deal with the inherent state explosion problem.