Formal Methods for Control Synthesis: An Optimization Perspective

In control theory, complicated dynamics such as systems of (nonlinear) differential equations are controlled mostly to achieve stability. This fundamental property, which can be with respect to a desired operating point or a prescribed trajectory, is often linked with optimality, which requires minimizing a certain cost along the trajectories of a stable system. In formal verification (model checking), simple systems, such as finite-state transition graphs that model computer programs or digital circuits, are checked against rich specifications given as formulas of temporal logics. The formal synthesis problem, in which the goal is to synthesize or control a finite system from a temporal logic specification, has recently received increased interest. In this article, we review some recent results on the connection between optimal control and formal synthesis. Specifically, we focus on the following problem: Given a cost and a correctness temporal logic specification for a dynamical system, generate an optimal control strategy that satisfies the specification. We first provide a short overview of automata-based methods, in which the dynamics of the system are mapped to a finite abstraction that is then controlled using an automaton corresponding to the specification. We then provide a detailed overview of a class of methods that rely on mapping the specification and the dynamics to constraints of an optimization problem. We discuss advantages and limitations of these two types of approaches and suggest directions for future research.

• Publication year

  2019

• Venue

  Annu. Rev. Control. Robotics Auton. Syst.

• Publication date

  2019-05-03

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1146/ANNUREV-CONTROL-053018-023717
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• No references are available for this paper.

• When Every Transmission Counts: Event-Trigger Threshold Regulation for STL Properties

  2026cites this paper
• Comparison of Linear Systems Across Time Domains: Continuous-time vs. Discrete-time

  2026influential citation
• Causal Online Learning of Safe Regions in Cloud Radio Access Networks

  2026cites this paper
• Motion Planning with Metric Temporal Logic Using Reachability Analysis and Hybrid Zonotopes

  2026influential citation
• Distributed Execution of Signal Temporal Logic Tasks in Open Networked Robotic System via Predefined-Time Control

  2026cites this paper
• Solving the Synthesis Problem Self-Organizing Control System in the Class of Elliptical Accidents Optics for Objects with One Input and One Output

  2026cites this paper
• Formal Methods in Robot Policy Learning and Verification: A Survey on Current Techniques and Future Directions

  2026cites this paper
• Exact Continuous Reformulations of Logic Constraints in Nonlinear Optimization and Optimal Control Problems

  2026cites this paper
• Signal Temporal Logic Verification and Synthesis Using Deep Reachability Analysis and Layered Control Architecture

  2026cites this paper
• Robust Temporal Logic Planning Under Contingency Constraints

  2025cites this paper
• Bridging Perception and Planning: Towards End-to-End Planning for Signal Temporal Logic Tasks

  2025cites this paper
• Control Synthesis for Multiple Reach-Avoid Tasks via Hamilton-Jacobi Reachability Analysis

  2025cites this paper
• AP-observation Automata for Abstraction-based Verification of Continuous-time Systems (Extended Version)

  2025cites this paper
• Receding Horizon Control for Signal Temporal Logic Using Robustness-Conserving Partial Formula Evaluation

  2025cites this paper
• Accelerating Signal-Temporal-Logic-Based Task and Motion Planning of Bipedal Navigation using Benders Decomposition

  2025cites this paper
• Neuro-Symbolic Acceleration of MILP Motion Planning with Temporal Logic and Chance Constraints

  2025cites this paper
• Topology-aware planning under linear temporal logic constraints

  2025cites this paper
• Trajectory Optimization for UAV-Based Medical Delivery with Temporal Logic Constraints and Convex Feasible Set Collision Avoidance

  2025cites this paper
• Optimal On-the-Fly Route Planning With Rich Transportation Requests

  2025cites this paper
• Multi-Fidelity Temporal Reasoning: A Stratified Logic for Cross-Scale System Specifications

  2025cites this paper
• Smooth Logic Constraints in Nonlinear Optimization and Optimal Control Problems

  2025cites this paper
• Average Reward Reinforcement Learning for Omega-Regular and Mean-Payoff Objectives

  2025cites this paper
• Seeing, Saying, Solving: An LLM-to-TL Framework for Cooperative Robots

  2025cites this paper
• Continuous-Time Control Synthesis for Multiple Quadrotors under Signal Temporal Logic Specifications

  2025cites this paper
• Verification of Stochastic Systems Under Signal Temporal Logic Specifications

  2025cites this paper
• No-regret path planning for temporal logic tasks in partially-known environments

  2025cites this paper
• Model predictive control for on-orbit inspection mission with signal temporal logic specifications

  2025cites this paper
• Certified Inductive Synthesis for Online Mixed-Integer Optimization

  2025cites this paper
• Multi-layer Motion Planning with Kinodynamic and Spatio-Temporal Constraints

  2025cites this paper
• Ro-To-Go! Robust Reactive Control with Signal Temporal Logic

  2025cites this paper
• Safety Verification of Stochastic Systems under Signal Temporal Logic Specifications

  2025cites this paper
• Trajectory Planning with Signal Temporal Logic Costs Using Deterministic Path Integral Optimization

  2025cites this paper
• Pretrained Embeddings as a Behavior Specification Mechanism

  2025cites this paper
• Sequential Convex Programming for 6-DoF Powered Descent Guidance with Continuous-Time Compound State-Triggered Constraints

  2025cites this paper
• Challenges and opportunities in the industrial usage controller synthesis tools: A review of LTL-based opensource tools for automated control design

  2025cites this paper
• SMTL: A Stratified Logic for Expressive Multi-Level Temporal Specifications

  2025cites this paper
• Distributionally Robust Control Synthesis for Stochastic Systems with Safety and Reach-Avoid Specifications

  2025cites this paper
• Generalized Mean Robustness for Signal Temporal Logic

  2025cites this paper
• Robust Temporal Logic Task Planning for Multirobot Systems Under Permanent Robot Failures

  2025cites this paper
• Ask, Reason, Assist: Decentralized Robot Collaboration via Language and Logic

  2025cites this paper
• NL2SpaTiaL: Generating Geometric Spatio-Temporal Logic Specifications from Natural Language for Manipulation Tasks

  2025cites this paper
• MaxAuc: A Max-Plus-Based Auction Approach for Multi-Robot Allocations for Time-Ordered Temporal Logic Tasks

  2025cites this paper
• Streamlined Integration of GR(1) Synthesis and Reinforcement Learning for Optimizing Critical Cyber-Physical Systems

  2025cites this paper
• A Hybrid Learning-to-Optimize Framework for Mixed-Integer Quadratic Programming

  2025cites this paper
• Exact Smooth Reformulations for Trajectory Optimization Under Signal Temporal Logic Specifications

  2025cites this paper
• Ask, Reason, Assist: Robot Collaboration via Natural Language and Temporal Logic

  2025cites this paper
• Towards Tighter Convex Relaxation of Mixed-integer Programs: Leveraging Logic Network Flow for Task and Motion Planning

  2025influential citation
• Self-Triggered Model Predictive Control for Signal Temporal Logic Tasks

  2024cites this paper
• Signal temporal logic synthesis under Model Predictive Control: A low complexity approach

  2024influential citation
• Semantic and Logical Communication-Control Codesign for Correlated Dynamical Systems

  2024cites this paper
• Formal Synthesis of Controllers for Safety-Critical Autonomous Systems: Developments and Challenges

  2024cites this paper
• Safe Planning through Incremental Decomposition of Signal Temporal Logic Specifications

  2024cites this paper
• Robust-Locomotion-By-Logic: Perturbation-Resilient Bipedal Locomotion via Signal Temporal Logic Guided Model Predictive Control

  2024influential citation
• A Survey of Optimization-Based Task and Motion Planning: From Classical to Learning Approaches

  2024influential citation
• Flow-Based Synthesis of Reactive Tests for Discrete Decision-Making Systems With Temporal Logic Specifications

  2024cites this paper
• Reactive Temporal Logic-based Planning and Control for Interactive Robotic Tasks

  2024cites this paper
• Optimization with Temporal and Logical Specifications via Generalized Mean-based Smooth Robustness Measures

  2024cites this paper
• Path Planning for Autonomous Vehicle Turning at Intersections with Signal Temporal Logic Specifications

  2024cites this paper
• Decision-Making Based on Signal Temporal Logic for Ramp Merging and Diverging of Autonomous Vehicle

  2024cites this paper
• Task Formalization for Autonomous Driving Turning at Roundabouts with Signal Temporal Logic Specifications

  2024cites this paper
• Scalable Signal Temporal Logic Guided Reinforcement Learning via Value Function Space Optimization

  2024influential citation
• Precision on Demand: Propositional Logic for Event-Trigger Threshold Regulation

  2024cites this paper
• Power management via STL specifications of a DC microgrid integrating renewables and storage devices: a smart railway station case study

  2024cites this paper
• In Search of Trees: Decision-Tree Policy Synthesis for Black-Box Systems via Search

  2024cites this paper
• Strategy templates for almost-sure and positive winning of stochastic parity games towards permissive and resilient control

  2024cites this paper
• Risk-Aware Autonomous Driving with Linear Temporal Logic Specifications

  2024cites this paper
• A Signal Temporal Logic Approach for Task-Based Coordination of Multi-Aerial Systems: a Wind Turbine Inspection Case Study

  2024cites this paper
• Iterative Optimization-based Control of a Class of Mixed Logical Dynamical Systems with STL Specifications: A Case Study on Microgrids

  2024cites this paper
• Signal Temporal Logic Planning With Time-Varying Robustness

  2024influential citation
• Optimization-Based Task and Motion Planning Under Signal Temporal Logic Specifications Using Logic Network Flow

  2024cites this paper
• Interval Signal Temporal Logic for Robust Optimal Control

  2024cites this paper
• Motion Planning for Automata-based Objectives using Efficient Gradient-based Methods

  2024cites this paper
• Model Predictive Control Algorithm Based on Signal Temporal Logic Specifications with Disturbances Guaranteeing Feasibility

  2024cites this paper
• Real-Time Trajectory Generation for Soft Robot Manipulators Using Differential Flatness

  2024cites this paper
• A two-stage distributed receding horizon control for persistent monitoring tasks with monitoring count requirements

  2024cites this paper
• Traffic-Rule-Compliant Trajectory Repair via Satisfiability Modulo Theories and Reachability Analysis

  2024cites this paper
• Safe Merging of Autonomous Vehicles under Temporal Logic Task

  2024cites this paper
• Task-Driven Reinforcement Learning With Action Primitives for Long-Horizon Manipulation Skills

  2023cites this paper
• Interval Signal Temporal Logic From Natural Inclusion Functions

  2023cites this paper
• Walking-by-Logic: Signal Temporal Logic-Guided Model Predictive Control for Bipedal Locomotion Resilient to External Perturbations

  2023cites this paper
• Automaton Model Updating Based on the L* Algorithm

  2023cites this paper
• STLCCP: Efficient Convex Optimization-Based Framework for Signal Temporal Logic Specifications

  2023cites this paper
• Smooth Robustness Measures for Symbolic Control Via Signal Temporal Logic

  2023influential citation
• Context-Triggered Abstraction-Based Control Design

  2023cites this paper
• Signal Temporal Logic-Guided Model Predictive Control for Robust Bipedal Locomotion Resilient to Runtime External Perturbations

  2023cites this paper
• Ensuring Reliable Robot Task Performance through Probabilistic Rare-Event Verification and Synthesis

  2023cites this paper
• Signal Temporal Logic Meets Convex-Concave Programming: A Structure-Exploiting SQP Algorithm for STL Specifications

  2023cites this paper
• Formal methods to comply with rules of the road in autonomous driving: State of the art and grand challenges

  2023cites this paper
• Temporal Logic Motion Planning With Convex Optimization via Graphs of Convex Sets

  2023cites this paper
• Robust Temporal Logic Motion Control via Disturbance Observers

  2023cites this paper
• Multiple Subformulae Cooperative Control for Multiagent Systems Under Conflicting Signal Temporal Logic Tasks

  2023cites this paper
• Temporal logic guided safe model-based reinforcement learning: A hybrid systems approach

  2023cites this paper
• Runtime Assurance from Signal Temporal Logic Safety Specifications

  2023influential citation
• A Novel Framework for the Design of Resilient Cyber-Physical Systems Using Control Theory and Formal Methods

  2023cites this paper
• MAPS 2 : Multi-robot autonomous motion planning under signal temporal logic specifications

  2023cites this paper
• An Interleaved Algorithm for Integration of Robotic Task and Motion Planning

  2023cites this paper
• Neural controller design for a class of nonlinear systems with time-varying delay: A bibliometric analysis-based short literature review

  2023cites this paper
• Lexicographic Mixed-Integer Motion Planning with STL Constraints

  2023cites this paper
• Entropy Rate Maximization of Markov Decision Processes under Linear Temporal Logic Tasks

  2022cites this paper
• Temporal Logic Guided Motion Primitives for Complex Manipulation Tasks with User Preferences

  2022cites this paper