arXiv subjects

Vince Kurtz

Publications and source records attributed to Vince Kurtz.

29 records · Page 2Linked to original sources

arXiv2021

Active Perception and Control from PrSTL Specifications

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.

eess.SY↗

arXiv2021

Control Barrier Functions for Singularity Avoidance in Passivity-Based Manipulator Control

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.

cs.RO↗

arXiv2020

Approximate Simulation for Template-Based Whole-Body Control

Reduced-order template models are widely used to control high degree-of-freedom legged robots, but existing methods for template-based whole-body control rely heavily on heuristics and often suffer from robustness issues. In this letter, we propose a template-based whole-body control method grounded in the formal framework of approximate simulation. Our central contribution is to demonstrate how the Hamiltonian structure of rigid-body dynamics can be exploited to establish approximate simulation for a high-dimensional nonlinear system. The resulting controller is passive, more robust to push disturbances, uneven terrain, and modeling errors than standard QP-based methods, and naturally enables high center of mass walking. Our theoretical results are supported by simulation experiments with a 30 degree-of-freedom Valkyrie humanoid model.

cs.RO↗

arXiv2020

Trajectory Optimization for High-Dimensional Nonlinear Systems under STL Specifications

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.

cs.RO↗

arXiv2020

Automatic Trajectory Synthesis for Real-Time Temporal Logic

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.

eess.SY↗

arXiv2020

A Smooth Robustness Measure of Signal Temporal Logic for Symbolic Control

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.

eess.SY↗

arXiv2020

Robust Approximate Simulation for Hierarchical Control of Linear Systems under Disturbances

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.

eess.SY↗

arXiv2019

Kalman Filtering with Gaussian Processes Measurement Noise

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 Mapping (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.

stat.ML↗

arXiv2019

Formal Connections between Template and Anchor Models via Approximate Simulation

Reduced-order template models like the Linear Inverted Pendulum (LIP) and Spring-Loaded Inverted Pendulum (SLIP) are widely used tools for controlling high-dimensional humanoid robots. However, connections between templates and whole-body models have lacked formal underpinnings, preventing formal guarantees when it comes to integrated controller design. We take a small step towards addressing this gap by considering the notion of approximate simulation. Derived from simulation relations for discrete transition systems in formal methods, approximate similarity means that the outputs of two systems can remain $ε$-close. In this paper, we consider the case of controlling a balancer via planning with the LIP model. We show that the balancer approximately simulates the LIP and derive linear constraints that are sufficient conditions for maintaining ground contact. This allows for rapid planning and replanning with the template model by solving a quadratic program that enforces contact constraints in the full model. We demonstrate the efficacy of this planning and control paradigm in a simulated push recovery scenario for a planar 4-link balancer.

cs.RO↗

arXiv2019

Active Perception and Control from Temporal Logic Specifications

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.

eess.SY↗

arXiv2019

Bayesian Optimization for Polynomial Time Probabilistically Complete STL Trajectory Synthesis

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.

cs.RO↗