Adapting behaviors via reactive synthesis

DOI10.1007/978-3-030-81685-8_41MaRDI QIDQ832238zbMATH OpenOpenAlexFDO

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

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

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

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.

Recommendations

• Synthesis of Reactive(1) designs
• Verification and synthesis of reactive programs
• Publication:4433972
• Synthesizing reactive programs
• Compositional synthesis with parametric reactive controllers

Cites work

• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• scientific article; zbMATH DE number 1759492 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Automata, logics, and infinite games. A guide to current research
• Automatic sequences and zip-specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• Shield synthesis
• Synthesis of Reactive(1) designs
• Synthesis of asynchronous reactive programs from temporal specifications

Cited in

(2)

• Mimicking behaviors in separated domains
• Explainable Reactive Synthesis

Describes a project that uses

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)