Synthesis of Reactive(1) designs

2011/08/19 by Roderick Bloem, Barbara Jobstmann, Nir Piterman +2 · 471 citations
Computer Science · Mathematics · #Arbiter #Computer science #Data mining #Formal Methods in Verification #Generality #Mathematics #Measure (data warehouse) #Parallel computing #Process (computing) #Program synthesis #Programming language #Rank (graph theory) #Software Testing and Debugging Techniques #Theoretical computer science #VLSI and Analog Circuit Testing

paper · pdf · doi:10.1016/j.jcss.2011.08.007

published in Journal of Computer and System Sciences 78(3), 911-938 (Elsevier BV)

openalex publication_date 2011/08/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/02

Cited by

• Physically-Feasible Reactive Synthesis for Terrain-Adaptive Locomotion
• Controller Synthesis with Inductive Proofs for Piecewise Linear Systems: an SMT-based Algorithm
• Learning Formulas in Finite Variable Logics
• Shielded Controller Units for RL with Operational Constraints Applied to Remote Microgrids
• Temporal Logic Planning for Minimum-Time Positioning of Multiple Threat-Seduction Decoys
• Nonuniform abstractions, refinement and controller synthesis with novel\n BDD encodings
• Synthesis of coordination programs from linear temporal logic
• Adaptive GR(1) Specification Repair for Liveness-Preserving Shielding in Reinforcement Learning
• Logic programming for deliberative robotic task planning
• Towards Tighter Convex Relaxation of Mixed-integer Programs: Leveraging Logic Network Flow for Task and Motion Planning
• Reactive synthesis specification review for validity and quality
• A Symbolic Approach to Safety LTL Synthesis
• Neural Circuit Synthesis from Specification Patterns
• Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision
• Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis
• Shield Synthesis: Runtime Enforcement for Reactive Systems
• Parameterized Infinite-State Reactive Synthesis
• Dynamics-Based Reactive Synthesis and Automated Revisions for High-Level Robot Control
• Energy mu-Calculus: Symbolic Fixed-Point Algorithms for omega-Regular Energy Games
• Compositional Formal Analysis Based on Conventional Engineering Models
• LTLf Synthesis with Fairness and Stability Assumptions
• Engineering an LTLf Synthesis Tool
• Scaling GR(1) Synthesis via a Compositional Framework for LTL Discrete Event Control
• Interpolation-Based GR(1) Assumptions Refinement
• Software Engineering for Self-Adaptive Robotics: A Research Agenda
• Learning Linear Temporal Properties
• Combined Top-Down and Bottom-Up Approaches to Performance-guaranteed Integrated Task and Motion Planning of Cooperative Multi-agent Systems
• Alternating-Time Temporal Logic with Mean-Payoff Guarantees
• Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications
• Fast Obligation Translation and Synthesis
• Minimal Assumptions Refinement for GR(1) Specifications
• On the Expressive Power of Sub-Propositional Fragments of Modal Logic
• Shield synthesis. [europepmc]
• Performance heuristics for GR(1) synthesis and related algorithms. [europepmc]
• A learning-based synthesis approach of reward asynchronous probabilistic games against the linear temporal logic winning condition. [europepmc]
• A synthesis method for zero-sum mean-payoff asynchronous probabilistic games. [europepmc]
• Decidable Synthesis of Programs with Uninterpreted Functions [europepmc]