DCSynth: Guided reactive synthesis with soft requirements

Abstract

In this paper, we propose a technique for guided synthesis of a controller from regular requirements which are specified using an interval temporal logic QDDC. We find that QDDC is well suited for guided synthesis due to its superiority in dealing with both qualitative and quantitative specifications. Our framework allows specification consisting of both hard and soft requirements as QDDC formulas. We have developed a method and a tool DCSynth, which computes a controller that invariantly satisfies the hard requirement and it H-optimally meets the soft requirement. Soft requirements can be used to specify quality attributes. The proposed technique is also useful in dealing with conflicting (i.e. unrealizable) requirements by making some of them as soft requirements. Case studies are carried out to demonstrate the effectiveness of the soft requirement guided synthesis in obtaining high quality controllers. The quality of the synthesized controllers is compared by measuring both the guaranteed as well as the expected case behaviour of the controlled system. Tool DCSynth facilitates such comparison.