Incremental Verification for On-the-Fly Controller Synthesis

The CIRCA system automatically synthesizes hard real-time discrete event controllers from plant and environment descriptions. CIRCA's automatically-synthesized controllers provide guaranteed real-time performance and safety preservation in adversarial, non-closed-world domains. By separating controller construction from formal controller verification, CIRCA makes controller synthesis decisions in a time-abstract state space that is quite compact. However, controller verification requires a more complete consideration of time, to make real-time performance guarantees. By retaining information between verifications of partial controllers during the controller synthesis process, the incremental verification methods that we present here dramatically reduce the complexity of controller synthesis. We provide formal characterizations of our incremental verification technique and performance results demonstrating up to a 97% reduction in controller synthesis time using these methods.