---
res:
bibo_abstract:
- 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 phi by computing
an environment assumption psi such that the new specification psi -> phi is
realizable. Our aim is to construct an assumption psi 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.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Krishnendu Chatterjee
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Thomas A
foaf_name: Thomas Henzinger
foaf_surname: Henzinger
foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
orcid: 0000−0002−2985−7724
- foaf_Person:
foaf_givenName: Barbara
foaf_name: Jobstmann, Barbara
foaf_surname: Jobstmann
bibo_doi: 10.1007/978-3-540-85361-9_14
bibo_volume: 5201
dct_date: 2008^xs_gYear
dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@
dct_title: Environment assumptions for synthesis@
...