In synthesis, we aim to construct a finite-state reactive system from a given 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. In this talk, I will give a short introduction into the synthesis problem and the underlying game theory, discuss desired properties of assumptions, and present a two-step algorithm to compute useful environment assumptions. Our algorithm operates on the game graph that is used to answer the realizability question. First, it computes a safety assumption that removes a minimal set of environment edges from the graph. Second, it computes a liveness assumption that puts fairness conditions on some of the remaining environment edges. We use probabilistic games to compute the liveness assumptions. This is joint work with Krishnendu Chatterjee and Tom Henzinger.
