Synthesis of Reactive(1) designs

2011/08/19 by Roderick Bloem, Barbara Jobstmann, Nir Piterman +2 · 27 citations
Computer Science · #Formal Methods in Verification #Software Testing and Debugging Techniques #VLSI and Analog Circuit Testing

paper · doi:10.1016/j.jcss.2011.08.007

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\n 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
• 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
• 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]