Abstract
The objective of reactive synthesis is to automatically construct an implementation of a reactive system from a high-level specification. While this idea holds a great promise, applying synthesis often faces significant challenges. One of the main hurdles is that the system designer has to provide the right formal specification, which is often a difficult task. In particular, since the system being synthesized is required to satisfy its requirements against all possible environments allowed by the specification, accurately capturing the designer’s knowledge about the environment in which the system will execute is crucial for being able to successfully synthesize an implementation. Missing assumptions about the environment lead quickly to unrealizable specifications, i.e., specifications for which there is no implementation that satisfies them.
In this talk, 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 approximate 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.