Synthesis of Reactive(1) designs
From MaRDI portal
Publication:439954
DOI10.1016/j.jcss.2011.08.007zbMath1247.68050OpenAlexW2041701185MaRDI QIDQ439954
Yaniv Sa'ar, Amir Pnueli, Roderick Bloem, Barbara Jobstmann, Nir Piterman
Publication date: 17 August 2012
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jcss.2011.08.007
Applications of game theory (91A80) Logic in computer science (03B70) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Compositional construction of abstractions for infinite networks of discrete-time switched systems, Adapting behaviors via reactive synthesis, Causality-based game solving, Symbolic Model Checking in Non-Boolean Domains, Finite abstractions with robustness margins for temporal logic-based control synthesis, Unnamed Item, Compositional and symbolic synthesis of reactive controllers for multi-agent systems, Linear temporal logic -- from infinite to finite horizon, Qualitative Approximate Behavior Composition, On the relation between reactive synthesis and supervisory control of non-terminating processes, Mean-payoff games with \(\omega\)-regular specifications, Flexible FOND Planning with Explicit Fairness Assumptions, Fairness, assumptions, and guarantees for extended bounded response \textsf{LTL+P} synthesis, Specifiable robustness in reactive synthesis, Dynamic hierarchical reactive controller synthesis, Augmented finite transition systems as abstractions for control synthesis, Automated generation of dynamics-based runtime certificates for high-level control, On the complexity of rational verification, Agent planning programs, Finite-trace and generalized-reactivity specifications in temporal synthesis, Shield synthesis, Alternating good-for-MDPs automata, Unnamed Item, Tableaux for realizability of safety specifications, Reactive synthesis for relay-explorer consensus with intermittent communication, On tolerance of discrete systems with respect to transition perturbations, Unnamed Item, Optimal multirate sampling in symbolic models for incrementally stable switched systems, Approximate Automata for Omega-Regular Languages, Interpolation-Based GR(1) Assumptions Refinement, GR(1)*: GR(1) specifications extended with existential guarantees, Code aware resource management, Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\), Most General Property-Preserving Updates, Refutation-based synthesis in SMT, A weakness measure for GR(1) formulae, A weakness measure for GR(1) formulae, Unnamed Item, Static and dynamic property-preserving updates, Unnamed Item, Synthesizing Optimally Resilient Controllers, Performance heuristics for GR(1) synthesis and related algorithms, Synthesizing optimally resilient controllers, \(\mathsf{GR}(1)\) is equivalent to \(\mathsf{R}(1)\), On-the-fly informed search of non-blocking directed controllers, Compositional construction of most general controllers
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Results on the propositional \(\mu\)-calculus
- The existence of refinement mappings
- Safety and liveness from a methodological point of view
- Verification by augmented finitary abstraction
- Synthesizing robust systems
- Bridging the gap between fair simulation and trace inclusion
- An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
- Receding horizon control for temporal logic specifications
- Bounded Synthesis
- On the Merits of Temporal Testers
- Environment Assumptions for Synthesis
- Symbolic Synthesis of Finite-State Controllers for Request-Response Specifications
- Solving Games Without Determinization
- Better Quality in Synthesis through Quantitative Objectives
- An Antichain Algorithm for LTL Realizability
- Synthesis of Communicating Processes from Temporal Logic Specifications
- Deterministic generators and games for Ltl fragments
- Diagnostic Information for Realizability
- A Hybrid Algorithm for LTL Games
- Solving Sequential Conditions by Finite-State Strategies
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Safraless Compositional Synthesis
- Minimizing Generalized Büchi Automata
- Symbolic Implementation of Alternating Automata
- Verification, Model Checking, and Abstract Interpretation
