Environment Assumptions for Synthesis

DOI10.1007/978-3-540-85361-9_14MaRDI QIDQ3541016zbMATH OpenOpenAlexFDO

Authors Krishnendu Chatterjee, Barbara Jobstmann, Thomas A. Henzinger

Publication date 25 November 2008

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

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

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)

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.

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

Cited in

(26)

• Safraless LTL synthesis considering maximal realizability
• Synthesizing robust systems
• Iterated Boolean games
• Compositional construction of most general controllers
• Resilience to intermittent assumption violations in reactive synthesis
• Synthesis with rational environments
• Graph Games and Reactive Synthesis
• Compositional Control Synthesis for Partially Observable Systems
• Interpolation-based GR(1) assumptions refinement
• Cooperative reactive synthesis
• Synthesis of Reactive(1) designs
• Optimal assumptions for synthesis
• Fully observable non-deterministic planning as assumption-based reactive synthesis
• Assume-admissible synthesis
• Diagnostic Information for Realizability
• On high-quality synthesis
• Register-bounded synthesis
• A weakness measure for GR(1) formulae
• A weakness measure for GR(1) formulae
• Specifiable robustness in reactive synthesis
• Synthesizing approximate implementations for unrealizable specifications
• The complexity of LTL rational synthesis
• ACoRe: automated goal-conflict resolution
• The complexity of LTL rational synthesis
• Computing adequately permissive assumptions for synthesis
• Contract-based multi-agent logical controller synthesis under uncertainty

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)