  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.
