Adapting Behaviors via Reactive Synthesis

TL;DR

This paper introduces a scalable reactive synthesis approach for the Adapter Design Pattern, enabling automatic generation of adapters that ensure behavior equivalence, with a new specification format and an efficient synthesis tool.

Contribution

The work presents Separated GR($k$), a new specification format, and a scalable synthesis algorithm, along with the SGR($k$) tool, to improve adapter synthesis performance.

Findings

SGR($k$) outperforms existing tools on benchmarks.

Separated GR($k$) enables scalable synthesis for complex specifications.

The approach effectively automates adapter generation for different hardware.

Abstract

In the \emph{Adapter Design Pattern}, a programmer implements a \emph{Target} interface by constructing an \emph{Adapter} that accesses an existing \emph{Adaptee} code. In this work, we present a reactive synthesis interpretation to the adapter design pattern, wherein an algorithm takes an \emph{Adaptee} and a \emph{Target} transducers, and the aim is to synthesize an \emph{Adapter} transducer that, when composed with the {\em Adaptee}, generates a behavior that is equivalent to the behavior of the {\em Target}. One use of such an algorithm is to synthesize controllers that achieve similar goals on different hardware platforms. While this problem can be solved with existing synthesis algorithms, current state-of-the-art tools fail to scale. To cope with the computational complexity of the problem, we introduce a special form of specification format, called {\em Separated GR($k$)}, which can be solved with a scalable synthesis algorithm but still allows for a large set of realistic specifications. We solve the realizability and the synthesis problems for Separated GR($k$), and show how to exploit the separated nature of our specification to construct better algorithms, in terms of time complexity, than known algorithms for GR($k$) synthesis. We then describe a tool, called SGR($k$), that we have implemented based on the above approach and show, by experimental evaluation, how our tool outperforms current state-of-the-art tools on various benchmarks and test-cases.