## Environment Assumptions for Synthesis

*Krishnendu Chatterjee,
Thomas A. Henzinger,
and Barbara Jobstmann*

The synthesis problem asks to construct a reactive finite-state system
from an omega-regular specification. Initial specifications are often
unrealizable, which means that there is no system that implements the
specification. A common reason for unrealizability is that
assumptions on the environment of the system are incomplete. We study
the problem of correcting an unrealizable specification *g* by
computing an environment assumption *a* such that the new
specification *a ⇒ g* is realizable. Our aim is to
construct an assumption *a* that constrains only the environment
and is as weak as possible. We present a two-step algorithm for
computing assumptions. The algorithm operates on the game graph that
is used to answer the realizability question. First, we compute a
safety assumption that removes a minimal set of environment edges from
the graph. Second, we compute a liveness assumption that puts
fairness conditions on some of the remaining environment edges. We
show that the problem of finding a minimal set of fair edges is
computationally hard, and we use probabilistic games to compute a
locally minimal fairness assumption.

*Proceedings of the
19th International Conference on Concurrency Theory*
(CONCUR),
Lecture Notes in Computer Science 5201,
Springer,
2008,
pp. 147-161.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2008 Springer.