Synthesizing Approximate Implementations for Unrealizable Specifications

TL;DR

This paper introduces algorithms for synthesizing approximate implementations from unrealizable specifications within bounded environments, ensuring partial correctness on finite, ultimately periodic input sequences.

Contribution

It presents novel automata-theoretic and symbolic methods for synthesis in bounded settings and for generating approximate solutions that satisfy specifications on bounded lassos.

Findings

Algorithms successfully synthesize approximate implementations.

Methods guarantee specification satisfaction on bounded lassos.

Evaluation on arbiter specifications demonstrates effectiveness.

Abstract

The unrealizability of a specification is often due to the assumption that the behavior of the environment is unrestricted. In this paper, we present algorithms for synthesis in bounded environments, where the environment can only generate input sequences that are ultimately periodic words (lassos) with finite representations of bounded size. We provide automata-theoretic and symbolic approaches for solving this synthesis problem, and also study the synthesis of approximative implementations from unrealizable specifications. Such implementations may violate the specification in general, but are guaranteed to satisfy the specification on at least a specified portion of the bounded-size lassos. We evaluate the algorithms on different arbiter specifications.