Feedback refinement relations for symbolic controller synthesis

A common issue with existing approaches to symbolic controller synthesis lies in the huge complexity of the resulting controllers. In particular, the controllers usually need full plant state information and contain an abstraction of the plant as a building block. In this note, we present an extension which helps reduce that complexity. Our technique is based on the novel concept of feedback refinement relations to compare plants with their finite-state approximations. As an additional feature, our approach builds on infinitary completed trace semantics and allows for the synthesis of controllers for arbitrary, not necessarily prefix-closed specifications. We also reveal if and how existing symbolic controller synthesis procedures should be extended to benefit from the advantages of our technique.