-
Temporal Logic Motion Planning with Convex Optimization via Graphs of Convex Sets
Authors:
Vince Kurtz,
Hai Lin
Abstract:
Temporal logic is a concise way of specifying complex tasks. But motion planning to achieve temporal logic specifications is difficult, and existing methods struggle to scale to complex specifications and high-dimensional system dynamics. In this paper, we cast Linear Temporal Logic (LTL) motion planning as a shortest path problem in a Graph of Convex Sets (GCS) and solve it with convex optimizati…
▽ More
Temporal logic is a concise way of specifying complex tasks. But motion planning to achieve temporal logic specifications is difficult, and existing methods struggle to scale to complex specifications and high-dimensional system dynamics. In this paper, we cast Linear Temporal Logic (LTL) motion planning as a shortest path problem in a Graph of Convex Sets (GCS) and solve it with convex optimization. This approach brings together the best of modern optimization-based temporal logic planners and older automata-theoretic methods, addressing the limitations of each: we avoid clip** and passthrough by representing paths with continuous Bezier curves; computational complexity is polynomial (not exponential) in the number of sample points; global optimality can be certified (though it is not guaranteed); soundness and probabilistic completeness are guaranteed under mild assumptions; and most importantly, the method scales to complex specifications and high-dimensional systems, including a 30-DoF humanoid. Open-source code is available at https://github.com/vincekurtz/ltl_gcs.
△ Less
Submitted 1 June, 2023; v1 submitted 18 January, 2023;
originally announced January 2023.
-
Mixed-Integer Programming for Signal Temporal Logic with Fewer Binary Variables
Authors:
Vince Kurtz,
Hai Lin
Abstract:
Signal Temporal Logic (STL) provides a convenient way of encoding complex control objectives for robotic and cyber-physical systems. The state-of-the-art in trajectory synthesis for STL is based on Mixed-Integer Convex Programming (MICP). The MICP approach is sound and complete, but has limited scalability due to exponential complexity in the number of binary variables. In this letter, we propose…
▽ More
Signal Temporal Logic (STL) provides a convenient way of encoding complex control objectives for robotic and cyber-physical systems. The state-of-the-art in trajectory synthesis for STL is based on Mixed-Integer Convex Programming (MICP). The MICP approach is sound and complete, but has limited scalability due to exponential complexity in the number of binary variables. In this letter, we propose a more efficient MICP encoding for STL. Our new encoding is based on the insight that disjunction can be encoded using a logarithmic number of binary variables and conjunction can be encoded without binary variables. We demonstrate in simulation examples that our proposed approach significantly outperforms the state-of-the-art for long and complex specifications. Open-source software is available at https://stlpy.readthedocs.io.
△ Less
Submitted 3 May, 2022; v1 submitted 13 April, 2022;
originally announced April 2022.
-
Robust Approximate Simulation for Hierarchical Control of Piecewise Affine Systems under Bounded Disturbances
Authors:
Zihao Song,
Vince Kurtz,
Shirantha Welikala,
Panos J. Antsaklis,
Hai Lin
Abstract:
Piecewise affine (PWA) systems are widely applied in many practical cases such as the control of nonlinear systems and hybrid dynamics. However, most of the existing PWA control methods have poor scalability with respect to the number of modes and system dimensions and may not be robust to the disturbances in performance. In this paper, we present a robust approximate simulation based control meth…
▽ More
Piecewise affine (PWA) systems are widely applied in many practical cases such as the control of nonlinear systems and hybrid dynamics. However, most of the existing PWA control methods have poor scalability with respect to the number of modes and system dimensions and may not be robust to the disturbances in performance. In this paper, we present a robust approximate simulation based control method for PWA systems under bounded external disturbances. First, a lower-dimensional linear system (abstraction) and an associated interface are designed to enable the output of the PWA system (concrete system) to track the output of the abstraction. Then, a Lyapunov-like simulation function is designed to show the boundedness of the output errors between the two systems. Furthermore, the results obtained for linear abstraction are extended to the case that a simpler PWA system is the abstraction. To illustrate the effectiveness of the proposed approach, simulation results are provided for two design examples.
△ Less
Submitted 3 March, 2022;
originally announced March 2022.
-
A More Scalable Mixed-Integer Encoding for Metric Temporal Logic
Authors:
Vince Kurtz,
Hai Lin
Abstract:
The state-of-the-art in optimal control from timed temporal logic specifications, including Metric Temporal Logic (MTL) and Signal Temporal Logic (STL), is based on Mixed-Integer Convex Programming (MICP). The standard MICP approach is sound and complete, but struggles to scale to long and complex specifications. Drawing on recent advances in trajectory optimization for piecewise-affine systems, w…
▽ More
The state-of-the-art in optimal control from timed temporal logic specifications, including Metric Temporal Logic (MTL) and Signal Temporal Logic (STL), is based on Mixed-Integer Convex Programming (MICP). The standard MICP approach is sound and complete, but struggles to scale to long and complex specifications. Drawing on recent advances in trajectory optimization for piecewise-affine systems, we propose a new MICP encoding for finite transition systems that significantly improves scalability to long and complex MTL specifications. Rather than seeking to reduce the number of variables in the MICP, we focus instead on designing an encoding with a tight convex relaxation. This leads to a larger optimization problem, but significantly improves branch-and-bound solver performance. In simulation experiments involving a mobile robot in a grid-world, the proposed encoding can reduce computation times by several orders of magnitude.
△ Less
Submitted 2 December, 2021;
originally announced December 2021.
-
Active Perception and Control from PrSTL Specifications
Authors:
Rafael Rodrigues da Silva,
Vince Kurtz,
Hai Lin
Abstract:
Next-generation intelligent systems must plan and execute complex tasks with imperfect information about their environment. As a result, plans must also include actions to learn about the environment. This is known as active perception. Most active perception algorithms rely on reward or cost functions, which are usually challenging to specify and offer few theoretical guarantees. On the other han…
▽ More
Next-generation intelligent systems must plan and execute complex tasks with imperfect information about their environment. As a result, plans must also include actions to learn about the environment. This is known as active perception. Most active perception algorithms rely on reward or cost functions, which are usually challenging to specify and offer few theoretical guarantees. On the other hand, symbolic control methods can account for complex tasks using temporal logic but often do not deal well with uncertainties. This work combines symbolic control with active perception to achieve complex tasks in a partially observed and noisy control system with hybrid dynamics. Our basic idea is to employ a counterexample-guided-inductive-synthesis approach for control from probabilistic signal temporal logic (PrSTL) specifications. Our proposed algorithm combines bounded model checking (BMC) with sampling-based trajectory synthesis for uncertain hybrid systems. Active perception is inherently built into the framework because PrSTL formulas are defined in the chance domain.
△ Less
Submitted 3 November, 2021;
originally announced November 2021.
-
Control Barrier Functions for Singularity Avoidance in Passivity-Based Manipulator Control
Authors:
Vince Kurtz,
Patrick M. Wensing,
Hai Lin
Abstract:
Task-space Passivity-Based Control (PBC) for manipulation has numerous appealing properties, including robustness to modeling error and safety for human-robot interaction. Existing methods perform poorly in singular configurations, however, such as when all the robot's joints are fully extended. Additionally, standard methods for constrained task-space PBC guarantee passivity only when constraints…
▽ More
Task-space Passivity-Based Control (PBC) for manipulation has numerous appealing properties, including robustness to modeling error and safety for human-robot interaction. Existing methods perform poorly in singular configurations, however, such as when all the robot's joints are fully extended. Additionally, standard methods for constrained task-space PBC guarantee passivity only when constraints are not active. We propose a convex-optimization-based control scheme that provides guarantees of singularity avoidance, passivity, and feasibility. This work paves the way for PBC with passivity guarantees under other types of constraints as well, including joint limits and contact/friction constraints. The proposed methods are validated in simulation experiments on a 7 degree-of-freedom manipulator.
△ Less
Submitted 27 September, 2021;
originally announced September 2021.
-
Trajectory Optimization for High-Dimensional Nonlinear Systems under STL Specifications
Authors:
Vince Kurtz,
Hai Lin
Abstract:
Signal Temporal Logic (STL) has gained popularity in recent years as a specification language for cyber-physical systems, especially in robotics. Beyond being expressive and easy to understand, STL is appealing because the synthesis problem---generating a trajectory that satisfies a given specification---can be formulated as a trajectory optimization problem. Unfortunately, the associated cost fun…
▽ More
Signal Temporal Logic (STL) has gained popularity in recent years as a specification language for cyber-physical systems, especially in robotics. Beyond being expressive and easy to understand, STL is appealing because the synthesis problem---generating a trajectory that satisfies a given specification---can be formulated as a trajectory optimization problem. Unfortunately, the associated cost function is nonsmooth and non-convex. As a result, existing synthesis methods scale poorly to high-dimensional nonlinear systems. In this letter, we present a new trajectory optimization approach for STL synthesis based on Differential Dynamic Programming (DDP). It is well known that DDP scales well to extremely high-dimensional nonlinear systems like robotic quadrupeds and humanoids: we show that these advantages can be harnessed for STL synthesis. We prove the soundness of our proposed approach, demonstrate order-of-magnitude speed improvements over the state-of-the-art on several benchmark problems, and demonstrate the scalability of our approach to the full nonlinear dynamics of a 7 degree-of-freedom robot arm.
△ Less
Submitted 13 November, 2020;
originally announced November 2020.
-
Automatic Trajectory Synthesis for Real-Time Temporal Logic
Authors:
Rafael Rodrigues da Silva,
Vince Kurtz,
Hai Lin
Abstract:
Many safety-critical systems must achieve high-level task specifications with guaranteed safety and correctness. Much recent progress towards this goal has been made through controller synthesis from temporal logic specifications. Existing approaches, however, have been limited to relatively short and simple specifications. Furthermore, existing methods either consider some prior discretization of…
▽ More
Many safety-critical systems must achieve high-level task specifications with guaranteed safety and correctness. Much recent progress towards this goal has been made through controller synthesis from temporal logic specifications. Existing approaches, however, have been limited to relatively short and simple specifications. Furthermore, existing methods either consider some prior discretization of the state-space, deal only with a convex fragment of temporal logic, or are not provably complete. We propose a scalable, provably complete algorithm that synthesizes continuous trajectories to satisfy non-convex \gls*{rtl} specifications. We separate discrete task planning and continuous motion planning on-the-fly and harness highly efficient boolean satisfiability (SAT) and \gls*{lp} solvers to find dynamically feasible trajectories that satisfy non-convex \gls*{rtl} specifications for high dimensional systems. The proposed design algorithms are proven sound and complete, and simulation results demonstrate our approach's scalability.
△ Less
Submitted 14 September, 2020;
originally announced September 2020.
-
A Smooth Robustness Measure of Signal Temporal Logic for Symbolic Control
Authors:
Yann Gilpin,
Vince Kurtz,
Hai Lin
Abstract:
Recent years have seen an increasing use of Signal Temporal Logic (STL) as a formal specification language for symbolic control, due to its expressiveness and closeness to natural language. Furthermore, STL specifications can be encoded as cost functions using STL's robust semantics, transforming the synthesis problem into an optimization problem. Unfortunately, these cost functions are non-smooth…
▽ More
Recent years have seen an increasing use of Signal Temporal Logic (STL) as a formal specification language for symbolic control, due to its expressiveness and closeness to natural language. Furthermore, STL specifications can be encoded as cost functions using STL's robust semantics, transforming the synthesis problem into an optimization problem. Unfortunately, these cost functions are non-smooth and non-convex, and exact solutions using mixed-integer programming do not scale well. Recent work has focused on using smooth approximations of robustness, which enable faster gradient-based methods to find local maxima, at the expense of soundness and/or completeness. We propose a novel robustness approximation that is smooth everywhere, sound, and asymptotically complete. Our approach combines the benefits of existing approximations, while enabling an explicit tradeoff between conservativeness and completeness.
△ Less
Submitted 9 June, 2020;
originally announced June 2020.
-
Robust Approximate Simulation for Hierarchical Control of Linear Systems under Disturbances
Authors:
Vince Kurtz,
Patrick M. Wensing,
Hai Lin
Abstract:
Approximate simulation, an extension of simulation relations from formal methods to continuous systems, is a powerful tool for hierarchical control of complex systems. Finding an approximate simulation relation between the full "concrete" system and a simplified "abstract" system establishes a bound on the output error between the two systems, allowing one to design a controller for the abstract s…
▽ More
Approximate simulation, an extension of simulation relations from formal methods to continuous systems, is a powerful tool for hierarchical control of complex systems. Finding an approximate simulation relation between the full "concrete" system and a simplified "abstract" system establishes a bound on the output error between the two systems, allowing one to design a controller for the abstract system while formally certifying performance on the concrete system. However, many real-world control systems are subject to external disturbances, which are not accounted for in the standard approximate simulation framework. We present a notion of robust approximate simulation, which considers external disturbances to the concrete system. We derive output error bounds for the case of linear systems subject to two types of additive disturbances: bounded disturbances and a sequence of (unbounded) impulse disturbances. We demonstrate the need for robust approximate simulation and the effectiveness of our proposed approach with a simulated robot motion planning example.
△ Less
Submitted 9 March, 2020;
originally announced March 2020.
-
Kalman Filtering with Gaussian Processes Measurement Noise
Authors:
Vince Kurtz,
Hai Lin
Abstract:
Real-world measurement noise in applications like robotics is often correlated in time, but we typically assume i.i.d. Gaussian noise for filtering. We propose general Gaussian Processes as a non-parametric model for correlated measurement noise that is flexible enough to accurately reflect correlation in time, yet simple enough to enable efficient computation. We show that this model accurately r…
▽ More
Real-world measurement noise in applications like robotics is often correlated in time, but we typically assume i.i.d. Gaussian noise for filtering. We propose general Gaussian Processes as a non-parametric model for correlated measurement noise that is flexible enough to accurately reflect correlation in time, yet simple enough to enable efficient computation. We show that this model accurately reflects the measurement noise resulting from vision-based Simultaneous Localization and Map** (SLAM), and argue that it provides a flexible means of modeling measurement noise for a wide variety of sensor systems and perception algorithms. We then extend existing results for Kalman filtering with autoregressive processes to more general Gaussian Processes, and demonstrate the improved performance of our approach.
△ Less
Submitted 23 September, 2019;
originally announced September 2019.
-
Active Perception and Control from Temporal Logic Specifications
Authors:
Rafael Rodrigues da Silva,
Vince Kurtz,
Hai Lin
Abstract:
Next-generation autonomous systems must execute complex tasks in uncertain environments. Active perception, where an autonomous agent selects actions to increase knowledge about the environment, has gained traction in recent years for motion planning under uncertainty. One prominent approach is planning in the belief space. However, most belief-space planning starts with a known reward function, w…
▽ More
Next-generation autonomous systems must execute complex tasks in uncertain environments. Active perception, where an autonomous agent selects actions to increase knowledge about the environment, has gained traction in recent years for motion planning under uncertainty. One prominent approach is planning in the belief space. However, most belief-space planning starts with a known reward function, which can be difficult to specify for complex tasks. On the other hand, symbolic control methods automatically synthesize controllers to achieve logical specifications, but often do not deal well with uncertainty. In this work, we propose a framework for scalable task and motion planning in uncertain environments that combines the best of belief-space planning and symbolic control. Specifically, we provide a counterexample-guided-inductive-synthesis algorithm for probabilistic temporal logic over reals (PRTL) specifications in the belief space. Our method automatically generates actions that improve confidence in a belief when necessary, thus using active perception to satisfy PRTL specifications.
△ Less
Submitted 9 May, 2019;
originally announced May 2019.
-
Bayesian Optimization for Polynomial Time Probabilistically Complete STL Trajectory Synthesis
Authors:
Vince Kurtz,
Hai Lin
Abstract:
In recent years, Signal Temporal Logic (STL) has gained traction as a practical and expressive means of encoding control objectives for robotic and cyber-physical systems. The state-of-the-art in STL trajectory synthesis is to formulate the problem as a Mixed Integer Linear Program (MILP). The MILP approach is sound and complete for bounded specifications, but such strong correctness guarantees co…
▽ More
In recent years, Signal Temporal Logic (STL) has gained traction as a practical and expressive means of encoding control objectives for robotic and cyber-physical systems. The state-of-the-art in STL trajectory synthesis is to formulate the problem as a Mixed Integer Linear Program (MILP). The MILP approach is sound and complete for bounded specifications, but such strong correctness guarantees come at the price of exponential complexity in the number of predicates and the time bound of the specification. In this work, we propose an alternative synthesis paradigm that relies on Bayesian optimization rather than mixed integer programming. This relaxes the completeness guarantee to probabilistic completeness, but is significantly more efficient: our approach scales polynomially in the STL time-bound and linearly in the number of predicates. We prove that our approach is sound and probabilistically complete, and demonstrate its scalability with a nontrivial example.
△ Less
Submitted 8 May, 2019;
originally announced May 2019.
