# DCSYNTH: Guided Reactive Synthesis with Soft Requirements

## TL;DR

This paper introduces DCSYNTH, a framework and tool for guided reactive controller synthesis using soft and hard requirements expressed in QDDC logic, enabling the creation of high-quality controllers that satisfy complex specifications.

## Contribution

It presents a novel method for synthesizing controllers guided by soft requirements in QDDC logic, handling conflicting specifications and optimizing controller quality.

## Key findings

- Effective synthesis of controllers satisfying hard and soft requirements.
- Ability to handle conflicting and unrealizable specifications.
- Demonstrated high-quality controllers through case studies.

## Abstract

In reactive controller synthesis, a number of implementations (controllers) are possible for a given specification because of the incomplete nature of specification. To choose the most desirable one from the various options, we need to specify additional properties which can guide the synthesis. In this paper, We propose a technique for guided controller synthesis 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 also developed a method and a tool DCSynth, which computes a controller that invariantly satisfies the hard requirement and it optimally meets the soft requirement. 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 using metrics measuring both the guaranteed and the expected case behaviour of the controlled system. Tool DCSynth facilitates such comparison.