Optimization-based trajectory generation with linear temporal logic specifications

We present a mathematical programming-based method for optimal control of discrete-time dynamical systems subject to temporal logic task specifications. We use linear temporal logic (LTL) to specify a wide range of properties and tasks, such as safety, progress, response, surveillance, repeated assembly, and environmental monitoring. Our method directly encodes an LTL formula as mixed-integer linear constraints on the continuous system variables, avoiding the computationally expensive processes of creating a finite abstraction of the system and a Büchi automaton for the specification. In numerical experiments, we solve temporal logic motion planning tasks for high-dimensional (10+ continuous state) dynamical systems.

Authors

• Eric M. Wolff
• Ufuk Topcu
• Richard M. Murray

Keywords

• Trajectory
• Encoding
• Planning
• Vehicle dynamics
• Cost function
• Indexes
• Robots
• Temporal Specificity
• Temporal Logic
• Linear Temporal Logic
• Temporal Logic Specifications
• Linear Temporal Logic Specifications
• System Dynamics
• Specific Tasks
• Continuous State
• Continuous System
• Path Planning
• Linear Logic
• System State
• Control Input
• Boolean Operators
• Time Index
• Mixed-integer Programming
• Discrete System
• Sequence Of States
• Solution Approach
• Mixed Integer Linear Programming
• Number Of Binary Variables
• Temporal Operators
• System Constraints
• Trajectory Length
• Set Of Propositions
• Safe Region
• Model Checking
• Input Constraints
• Infinite Sequence