Environment Assumptions for Synthesis

Details Environment Assumptions for Synthesis Environment Assumptions for Synthesis

2008-05-27

arxiv.org/abs/0805.4167v1

Computer Science

Computer Science and Game Theory

15 pages

Scientific paper

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\to\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.

Affiliated with

Also associated with

No associations

Rating

Environment Assumptions for Synthesis does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Environment Assumptions for Synthesis, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Environment Assumptions for Synthesis will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-274092