Environment Assumptions for Synthesis

DOI10.1007/978-3-540-85361-9_14zbMATH Open1160.68437arXiv0805.4167OpenAlexW1499127572MaRDI QIDQ3541016FDOQ3541016

Authors: Krishnendu Chatterjee, Barbara Jobstmann, Thomas A. Henzinger 

Publication date: 25 November 2008

Published in: CONCUR 2008 - Concurrency Theory (Search for Journal in Brave)

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 $psiophi$ 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.

Full work available at URL: https://arxiv.org/abs/0805.4167

Recommendations

• Optimal assumptions for synthesis
• Synthesis with rational environments
• scientific article; zbMATH DE number 958151
• Synthesis for Probabilistic Environments
• A unified approach to environmental systems modeling
• scientific article; zbMATH DE number 3876885
• Modelling and architecture of a generic framework for integrative environmental simulations
• Publication:4203891
• Environmental impact assessment in an uncertain environment
• Reaction systems with influence on environment

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (23)

• Compositional Control Synthesis for Partially Observable Systems
• Fully observable non-deterministic planning as assumption-based reactive synthesis
• Iterated Boolean games
• Diagnostic Information for Realizability
• Resilience to intermittent assumption violations in reactive synthesis
• Optimal assumptions for synthesis
• Compositional construction of most general controllers
• On high-quality synthesis
• Synthesis with rational environments
• Synthesis of Reactive(1) designs
• Title not available (Why is that?)
• Graph Games and Reactive Synthesis
• A weakness measure for GR(1) formulae
• A weakness measure for GR(1) formulae
• Safraless LTL synthesis considering maximal realizability
• The complexity of LTL rational synthesis
• Synthesizing robust systems
• Cooperative reactive synthesis
• The complexity of LTL rational synthesis
• ACoRe: automated goal-conflict resolution
• Computing adequately permissive assumptions for synthesis
• Assume-admissible synthesis
• Interpolation-based GR(1) assumptions refinement

This page was built for publication: Environment Assumptions for Synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3541016)