Specification Format for Reactive Synthesis Problems

TL;DR

This paper introduces a user-friendly specification format for reactive synthesis problems, simplifying the process of defining partial implementations and enabling compatibility with existing synthesizer tools.

Contribution

The paper proposes a new specification format that makes defining partial implementations easier and provides conversion scripts for integration with SYNTCOMP synthesizers.

Findings

The new format reduces complexity in specifying reactive systems.

Conversion scripts enable seamless use with existing synthesis tools.

Facilitates easier adoption of reactive synthesis methods.

Abstract

Automatic synthesis from a given specification automatically constructs correct implementation. This frees the user from the mundane implementation work, but still requires the specification. But is specifying easier than implementing? In this paper, we propose a user-friendly format to ease the specification work, in particularly, that of specifying partial implementations. Also, we provide scripts to convert specifications in the new format into the SYNTCOMP format, thus benefiting from state of the art synthesizers.