publications

2025

1. Automatic Synthesis of Smooth Infinite Horizon Paths Satisfying Linear Temporal Logic Specifications

   Samuel Williams and Jyotirmoy Deshmukh

   In Computer Aided Verification, Zagreb, HR, Jul 2025

   Abs DOI

   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.

2024

1. Potential Games on Cubic Splines for Self-Interested Multi-Agent Motion Planning

   Samuel Williams and Jyotirmoy Deshmukh

   IEEE Control Systems Letters, Nov 2024

   Abs DOI

   Existing multi-agent motion planners face scalability challenges with the number of agents and route plans that span long time horizons. We tackle these issues by introducing additional abstraction by interpolating agent trajectories with natural cubic splines and leveraging existing results that under some natural assumptions, the resulting game has the structure of a potential game. We prove a simultaneous gradient descent method using independent per-agent step sizes is guaranteed to converge to a local Nash equilibrium. Compared with recent iLQR-based potential game solvers, our method solves for local Nash equilibrium trajectories faster in games with up to 52 agents, and we demonstrate scalability to long horizons.

2. LB4TL: A Smooth Semantics for Temporal Logic to Train Neural Feedback Controllers

   Navid Hashemi, Samuel Williams, Bardh Hoxha, and 3 more authors

   In The 8th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), Boulder, CO, Jul 2024

   Abs DOI

   This paper presents a framework for training neural network (NN)-based feedback controllers for autonomous agents with deterministic nonlinear dynamics to satisfy task objectives and safety constraints expressed in discrete-time Signal Temporal Logic (DT-STL). Control synthesis that uses the robustness semantics of DT-STL poses challenges due to its non-convexity, non-differentiability, and recursive definition, in particular when it is used to train NNbased controllers. We introduce a smooth neuro-symbolic computation graph to encode DTSTL robustness to represent a smooth approximation of the robustness, enabling the use of powerful stochastic gradient descent and backpropagation-based optimization for training. Our approximation guarantees that it lower bounds the robustness value of a given DT-STL formula, and shows orders of magnitude improvement over existing smooth approximations when applied to control synthesis. We demonstrate our approach on planning to satisfy complex spatiotemporal and sequential tasks, and show scalability with formula complexity.