DCSYNTH: A Tool for Guided Reactive Synthesis with Soft Requirements.

This paper proposes a technique for the synthesis of high quality controllers from logical specification in an interval temporal logic Quantified Discrete Duration Calculus (QDDC). The specification consists of hard and soft requirements. We compute the controller which guarantees that hard requirements hold invariantly. Moreover, it intermittently but {em maximally} meets the soft requirement as much as possible. We show that this soft requirement guided synthesis provides a useful ability to specify and efficiently synthesize high quality controllers. The technique is also useful in dealing with conflicting requirements. The proposed technique is implemented in a tool DCSYNTH. We illustrate our approach using a case study of a synchronous bus arbiter specification and we experimentally show the effect of soft requirements on the quality (worst case and expected case behaviour) of the synthesized controller.