Adapting behaviors via reactive synthesis

DOI10.1007/978-3-030-81685-8_41zbMATH Open1493.68201arXiv2105.13837OpenAlexW3184451432MaRDI QIDQ832238FDOQ832238

Authors: Gal Amram, Suguman Bansal, Dror Fried, Lucas Martinelli Tabajara, Moshe Y. Vardi, Gera Weiss 

Publication date: 25 March 2022

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.

Full work available at URL: https://arxiv.org/abs/2105.13837

Recommendations

• Synthesis of Reactive(1) designs
• Verification and synthesis of reactive programs
• scientific article; zbMATH DE number 2000429
• Synthesizing reactive programs
• Compositional synthesis with parametric reactive controllers

Mathematics Subject Classification ID

Applications of game theory (91A80) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Graph-Based Algorithms for Boolean Function Manipulation
• Automatic sequences and zip-specifications
• Title not available (Why is that?)
• Automata, logics, and infinite games. A guide to current research
• Title not available (Why is that?)
• Synthesis of Reactive(1) designs
• Title not available (Why is that?)
• Shield synthesis
• Sequential relational decomposition
• Synthesis of asynchronous reactive programs from temporal specifications

Cited In (2)

• Mimicking behaviors in separated domains
• Explainable Reactive Synthesis

Uses Software

• CUDD
• Strix

This page was built for publication: Adapting behaviors via reactive synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832238)