Abstractions and sensor design in partial-information, reactive controller synthesis

Automated synthesis of reactive control protocols from temporal logic specifications has recently attracted considerable attention in various applications, for example, robotic motion planning, network management, etc. An implicit and often unrealistic assumption in this past work is the availability of complete and precise sensing information during the execution of the controllers. In this paper, we use an abstraction procedure for systems with partial observation and propose a formalism to investigate the effects of limitations in sensing. The abstraction procedure enables the existing synthesis methods with partial observation to be applicable and efficient for systems with infinite (or finite but large number of) states. This formalism enables us to systematically discover necessary sensing modalities for rendering the underlying synthesis problems realizable. We use counterexamples, which witness unrealizability potentially due to the limitations in sensing and the coarseness of the abstraction, and interpolation-based techniques to refine the model and the sensing modalities, i.e., to identify new sensors to be included, for the control objective. We demonstrate the method on robot motion planning examples.