Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


Title: Automatic Synthesis of Smooth Infinite Horizon Paths Satisfying Linear Temporal Logic Specifications
Abstract Automatically constructing smooth paths that satisfy a formal specification is a challenging problem. Existing methods struggle to scale to long horizon specifications and challenging environments. We present a method that uses abstraction, model checking, and convex optimization to solve for a smooth Bézier spline that is guaranteed to satisfy a Linear Temporal Logic specification. Our approach uses a coarse abstraction to avoid the state explosion of other abstraction based methods, and successfully avoids the computational challenges of directly optimizing the non-convex temporal logic semantics. We prove our method is sound and complete and demonstrate a significant computational advantage relative to state of the art approaches. Generating such smooth paths has natural applications in path planning for autonomous robots, and we demonstrate the applicability of our method on path planning for a quadrotor.  more » « less
Award ID(s):
2048094
PAR ID:
10698699
Author(s) / Creator(s):
;
Editor(s):
Piskac, R; Rakamarić, Z
Publisher / Repository:
Computer Aided Verification. CAV 2025. Lecture Notes in Computer Science, vol 15934.
Date Published:
Page Range / eLocation ID:
249 to 273
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ; (, American Control Conference (ACC))
    This paper studies the synthesis of control policies for an agent that has to satisfy a temporal logic specification in a partially observable environment, in the presence of an adversary. The interaction of the agent (defender) with the adversary is modeled as a partially observable stochastic game. The search for policies is limited to over the space of finite state controllers, which leads to a tractable approach to determine policies. The goal is to generate a defender policy to maximize satisfaction of a given temporal logic specification under any adversary policy. We relate the satisfaction of the specification in terms of reaching (a subset of) recurrent states of a Markov chain. We then present a procedure to determine a set of defender and adversary finite state controllers of given sizes that will satisfy the temporal logic specification. We illustrate our approach with an example. 
    more » « less
  2. ; ; ; (, IEEE International Conference on Robotics and Automation)
    This paper proposes an optimization-based task and motion planning framework, named “Logic Network Flow”, to integrate signal temporal logic (STL) specifications into efficient mixed-binary linear programmings. In this framework, temporal predicates are encoded as polyhedron constraints on each edge of the network flow, instead of as constraints between the nodes as in the traditional Logic Tree formulation. Synthesized with Dynamic Network Flows, Logic Network Flows render a tighter convex relaxation compared to Logic Trees derived from these STL specifications. Our formulation is evaluated on several multi-robot motion planning case studies. Empirical results demonstrate that our formulation outperforms Logic Tree formulation in terms of computation time for several planning problems. As the problem size scales up, our method still discovers better lower and upper bounds by exploring fewer number of nodes during the branch-andbound process, although this comes at the cost of increased computational load for each node when exploring branches. 
    more » « less
  3. ; ; ; ; (, 2020 American Control Conference)
    We present planning and control techniques for non-periodic locomotion tasks specified by temporal logic in rough cluttered terrains. Our planning approach is based on a discrete set of motion primitives for the center of mass (CoM) of a general bipedal robot model. A deterministic shortest path problem is solved over the Bu ̈chi automaton of the temporal logic task specification, composed with the graph of CoM keyframe states generated by the motion primitives. A low-level controller based on quadratic programming is proposed to track the resulting CoM and foot trajectories. We demonstrate dynamically stable, non-periodic locomotion of a kneed compass gait bipedal robot satisfying complex task specifications. 
    more » « less
  4. ; ; ; (, ACM)
    We present algorithms for Cyber-Physical Systems (CPS) falsification and control, which take advantage of knowing the entire language of the temporal logic specification - that is, the set of signals that satisfy the formula. In the design of CPS, falsification and control play key roles. Falsification is a testing task, where the goal is to find an input signal that causes the system's output trajectory to violate the correctness requirements. Control is the dual task, where the goal is to find an input signal that causes the system's output to satisfy the specification. When the specification is expressed in a temporal logic, most existing work relies on local optimization heuristics to perform both tasks. In this paper, we explore whether a different expression of the specification offers advantages when performing falsification and control. Recent work presented a method for computing a representation of the language of a formula in (discrete-time) Signal Temporal Logic (STL), showing that the language can be represented as a union of polytopes. We introduce new falsification algorithms which combine distance information to the different components of the language to accelerate the convergence to a falsifier. And we introduce a new algorithm for computing a satisfying control signal which works by repeatedly projecting violating output trajectories back onto the language's components. Moreover, these algorithms are trivially parallelizable to take advantage of multiple processors. Despite their relative simplicity, our algorithms demonstrate 10x to 100x speedups relative to the state-of-the-art. 
    more » « less
  5. ; ; (, ASME Letters in Translational Robotics)
    Abstract Researchers are exploring augmented reality (AR) interfaces for online robot programming to streamline automation and user interaction in various environments. This study designs, implements, and experimentally validates an AR interface for online programming and data visualization. This new interface integrates human manipulation in the randomized robot path planning, reducing the inherent randomness of the methods with human intervention. The interface uses holographic items that correspond to physical elements to interact with redundant robot manipulators. Utilizing rapidly random tree star (RRT*) and spherical linear interpolation (SLERP) algorithms, the interface achieves end-effector's progression through the collision-free path with smooth rotation. Next, sequential quadratic programming (SQP) achieve robot's configurations for this progression. The platform executes the RRT* algorithm in a loop, with each iteration independently exploring the shortest path through random sampling, leading to variations in the optimized paths produced. These paths are then demonstrated to AR users, who select the most appropriate path based on the environmental context and their intuition. The accuracy and effectiveness of the interface are validated through its implementation and testing with a 7-degrees-of-freedom (DOFs) manipulator, indicating its potential to optimize path planning and to advance current practices in robot programming. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Text Encoded Conversion
  • XML
  • Save / Share this Record
  • Send to Email