Environment Assumptions for Synthesis
| dc.creator | Chatterjee, Krishnendu | |
| dc.creator | Henzinger, Thomas A. | |
| dc.creator | Jobstmann, Barbara | |
| dc.date | 2008-05-27 | |
| dc.date.accessioned | 2026-07-07T12:19:16Z | |
| dc.date.available | 2026-07-07T12:19:16Z | |
| dc.description | The synthesis problem asks to construct a reactive finite-state system from an $ω$-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 $ϕ$ by computing an environment assumption $ψ$ such that the new specification $ψ\toϕ$ is realizable. Our aim is to construct an assumption $ψ$ 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. | |
| dc.description | 15 pages | |
| dc.identifier | https://arxiv.org/abs/0805.4167 | |
| dc.identifier | http://arxiv.org/abs/0805.4167 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/212694 | |
| dc.subject | Computer Science and Game Theory | |
| dc.subject | Logic in Computer Science | |
| dc.title | Environment Assumptions for Synthesis | |
| dc.type | text |