arXiv subjects

Kevin Leahy

Publications and source records attributed to Kevin Leahy.

At least 19 recordsLinked to original sources

arXiv2026

Robustness-Based Synthesis for Time Window Temporal Logic Specifications via Mixed-Integer Linear Programming

Time Window Temporal Logic (TWTL) is a rich specification language for cyber-physical systems that can compactly express sequential tasks with explicit timing constraints. In this paper, we consider the problem of synthesizing control inputs for discrete-time linear systems subject to TWTL task specifications. Building on the quantitative semantics (robustness) recently introduced for TWTL in [1], we encode the robust satisfaction of a TWTL formula as a set of Mixed-Integer Linear constraints and pose synthesis as a Mixed Integer Linear Program (MILP) that maximizes the robustness degree. We prove that any feasible solution with positive objective value guarantees Boolean satisfaction of the specification. We address two synthesis settings: an \emph{open-loop} formulation that optimizes the full control sequence from the initial state, and a \emph{closed-loop} receding-horizon Model Predictive Controller (MPC) formulation that re-solves the MILP at each step using the current measured state. A key feature of our MPC formulation is a \emph{task-adaptive horizon} that exploits the TWTL Deterministic Finite Automaton (DFA) to determine the active sub-task at each step, limiting the prediction horizon to the remaining window of the current task rather than the full formula horizon, this makes each re-solve significantly cheaper than the initial open-loop solve.

cs.RO↗

arXiv2026

Conflict-Aware Switching for CBF-CLF-Based Multi-Goal Navigation

Quadratic programs (QPs) using Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs) are widely used for safe control in reach-and-avoid navigation. However, the inherently conflicting nature of CBF and CLF constraints can lead to performance degradation, including slowdowns and deadlocks. This issue is exacerbated in multi-goal scenarios, where multiple nominal control objectives must be satisfied under shared safety constraints. Existing approaches for preemptive safety are often computationally expensive or overly conservative, while methods that relax or switch between nominal objectives are not well-suited for sequential goal-to-goal navigation. To address these limitations, we propose a conflict-aware switching strategy that detects high-conflict conditions and switches between available nominal control objectives to reduce constraint conflict. We apply this approach to multi-agent, multi-goal reach-and-avoid scenarios under CBF-CLF-QP control. Compared to a baseline sequential goal traversal strategy, our method reduces both completion time and timeout rates, demonstrating improved performance in satisfying all nominal control objectives while respecting safety constraints.

cs.RO↗

arXiv2026

Robust Multi-Agent Target Tracking in Intermittent Communication Environments via Analytical Belief Merging

Autonomous multi-agent target tracking in GPS-denied and communication-restricted environments (e.g., underwater exploration, subterranean search and rescue, and adversarial domains) forces agents to operate independently and only exchange information during brief reconnection windows. Because transmitting complete observation and trajectory histories is bandwidth-exhaustive, exchanging probabilistic belief maps serves as a highly efficient proxy that preserves the topology of agent knowledge. While minimizing divergence metrics to merge these decentralized beliefs is conceptually sound, traditional approaches often rely on numerical solvers that introduce critical quantization errors and artificial noise floors. In this paper, we formulate the decentralized belief merging problem as Forward and Reverse Kullback-Leibler (KL) divergence optimizations and derive their exact closed-form analytical solutions. By deploying these derivations, we mathematically eliminate optimization artifacts, achieving perfect mathematical fidelity while reducing the computational complexity of the belief merge to $\mathcal{O}(N|S|)$ scalar operations. Furthermore, we propose a novel spatially-aware visit-weighted KL merging strategy that dynamically weighs agent beliefs based on their physical visitation history. Validated across tens of thousands of distributed simulations, extensive sensitivity analysis demonstrates that our proposed method significantly suppresses sensor noise and outperforms standard analytical means in environments characterized by highly degraded sensors and prolonged communication intervals.

cs.RO↗

arXiv2026

Complex-Valued GNNs for Distributed Basis-Invariant Control of Planar Systems

Graph neural networks (GNNs) are a well-regarded tool for learned control of networked dynamical systems due to their ability to be deployed in a distributed manner. However, current distributed GNN architectures assume that all nodes in the network collect geometric observations in compatible bases, which limits the usefulness of such controllers in GPS-denied and compass-denied environments. This paper presents a GNN parametrization that is globally invariant to choice of local basis. 2D geometric features and transformations between bases are expressed in the complex domain. Inside each GNN layer, complex-valued linear layers with phase-equivariant activation functions are used. When viewed from a fixed global frame, all policies learned by this architecture are strictly invariant to choice of local frames. This architecture is shown to increase the data efficiency, tracking performance, and generalization of learned control when compared to a real-valued baseline on an imitation learning flocking task.

cs.LG↗

arXiv2026

Real-Time Optical Communication Using Event-Based Vision with Moving Transmitters

In multi-robot systems, traditional radio frequency (RF) communication struggles with contention and jamming. Optical communication offers a strong alternative. However, conventional frame-based cameras suffer from limited frame rates, motion blur, and reduced robustness under high dynamic range lighting. Event cameras support microsecond temporal resolution and high dynamic range, making them extremely sensitive to scene changes under fast relative motion with an optical transmitter. Leveraging these strengths, we develop a complete optical communication system capable of tracking moving transmitters and decoding messages in real time. Our system achieves over $95\%$ decoding accuracy for text transmission during motion by implementing a Geometry-Aware Unscented Kalman Filter (GA-UKF), achieving 7x faster processing speed compared to the previous state-of-the-art method, while maintaining equivalent tracking accuracy at transmitting frequencies $\geq$ 1 kHz.

cs.RO↗

arXiv2025

Belief Space Control of Safety-Critical Systems Under State-Dependent Measurement Noise

Safety-critical control is imperative for deploying autonomous systems in the real world. Control Barrier Functions (CBFs) offer strong safety guarantees when accurate system and sensor models are available. However, widely used additive, fixed-noise models are not representative of complex sensor modalities with state-dependent error characteristics. Although CBFs have been designed to mitigate uncertainty using fixed worst-case bounds on measurement noise, this approach can lead to overly-conservative control. To solve this problem, we extend the Belief Control Barrier Function (BCBF) framework to accommodate state-dependent measurement noise via the Generalized Extended Kalman Filter (GEKF) algorithm, which models measurement noise as a linear function of the state. Using the original BCBF framework as baseline, we demonstrate the performance of the BCBF-GEKF approach through simulation results on a 1D single integrator setpoint tracking scenario and 2D unicycle kinematics trajectory tracking scenario. Our results confirm that the BCBF-GEKF approach offers less conservative control with greater safety.

eess.SY↗

arXiv2025

Multi-layer Motion Planning with Kinodynamic and Spatio-Temporal Constraints

We propose a novel, multi-layered planning approach for computing paths that satisfy both kinodynamic and spatiotemporal constraints. Our three-part framework first establishes potential sequences to meet spatial constraints, using them to calculate a geometric lead path. This path then guides an asymptotically optimal sampling-based kinodynamic planner, which minimizes an STL-robustness cost to jointly satisfy spatiotemporal and kinodynamic constraints. In our experiments, we test our method with a velocity-controlled Ackerman-car model and demonstrate significant efficiency gains compared to prior art. Additionally, our method is able to generate complex path maneuvers, such as crossovers, something that previous methods had not demonstrated.

cs.RO↗

arXiv2024

Comp-LTL: Temporal Logic Planning via Zero-Shot Policy Composition

This work develops a zero-shot mechanism, Comp-LTL, for an agent to satisfy a Linear Temporal Logic (LTL) specification given existing task primitives trained via reinforcement learning (RL). Autonomous robots often need to satisfy spatial and temporal goals that are unknown until run time. Prior work focuses on learning policies for executing a task specified using LTL, but they incorporate the specification into the learning process. Any change to the specification requires retraining the policy, either via fine-tuning or from scratch. We present a more flexible approach -- to learn a set of composable task primitive policies that can be used to satisfy arbitrary LTL specifications without retraining or fine-tuning. Task primitives can be learned offline using RL and combined using Boolean composition at deployment. This work focuses on creating and pruning a transition system (TS) representation of the environment in order to solve for deterministic, non-ambiguous, and feasible solutions to LTL specifications given an environment and a set of task primitive policies. We show that our pruned TS is deterministic, contains no unrealizable transitions, and is sound. We verify our approach via simulation and compare it to other state of the art approaches, showing that Comp-LTL is safer and more adaptable.

cs.RO↗

arXiv2024

Accelerating Proximal Policy Optimization Learning Using Task Prediction for Solving Environments with Delayed Rewards

In this paper, we tackle the challenging problem of delayed rewards in reinforcement learning (RL). While Proximal Policy Optimization (PPO) has emerged as a leading Policy Gradient method, its performance can degrade under delayed rewards. We introduce two key enhancements to PPO: a hybrid policy architecture that combines an offline policy (trained on expert demonstrations) with an online PPO policy, and a reward shaping mechanism using Time Window Temporal Logic (TWTL). The hybrid architecture leverages offline data throughout training while maintaining PPO's theoretical guarantees. Building on the monotonic improvement framework of Trust Region Policy Optimization (TRPO), we prove that our approach ensures improvement over both the offline policy and previous iterations, with a bounded performance gap of $(2ςγα^2)/(1-γ)^2$, where $α$ is the mixing parameter, $γ$ is the discount factor, and $ς$ bounds the expected advantage. Additionally, we prove that our TWTL-based reward shaping preserves the optimal policy of the original problem. TWTL enables formal translation of temporal objectives into immediate feedback signals that guide learning. We demonstrate the effectiveness of our approach through extensive experiments on an inverted pendulum and a lunar lander environments, showing improvements in both learning speed and final performance compared to standard PPO and offline-only approaches.

cs.LG↗

arXiv2024

Grand Challenges in the Verification of Autonomous Systems

Autonomous systems use independent decision-making with only limited human intervention to accomplish goals in complex and unpredictable environments. As the autonomy technologies that underpin them continue to advance, these systems will find their way into an increasing number of applications in an ever wider range of settings. If we are to deploy them to perform safety-critical or mission-critical roles, it is imperative that we have justified confidence in their safe and correct operation. Verification is the process by which such confidence is established. However, autonomous systems pose challenges to existing verification practices. This paper highlights viewpoints of the Roadmap Working Group of the IEEE Robotics and Automation Society Technical Committee for Verification of Autonomous Systems, identifying these grand challenges, and providing a vision for future research efforts that will be needed to address them.

cs.RO↗

arXiv2024

Tell Me What You Want (What You Really, Really Want): Addressing the Expectation Gap for Goal Conveyance from Humans to Robots

Conveying human goals to autonomous systems (AS) occurs both when the system is being designed and when it is being operated. The design-step conveyance is typically mediated by robotics and AI engineers, who must appropriately capture end-user requirements and concepts of operations, while the operation-step conveyance is mediated by the design, interfaces, and behavior of the AI. However, communication can be difficult during both these periods because of mismatches in the expectations and expertise of the end-user and the roboticist, necessitating more design cycles to resolve. We examine some of the barriers in communicating system design requirements, and develop an augmentation for applied cognitive task analysis (ACTA) methods, that we call robot task analysis (RTA), pertaining specifically to the development of autonomous systems. Further, we introduce a top-down view of an underexplored area of friction between requirements communication -- implied human expectations -- utilizing a collection of work primarily from experimental psychology and social sciences. We show how such expectations can be used in conjunction with task-specific expectations and the system design process for AS to improve design team communication, alleviate barriers to user rejection, and reduce the number of design cycles.

cs.RO↗

arXiv2024

Uncertainty Quantification for Recursive Estimation in Adaptive Safety-Critical Control

In this paper, we present a framework for online parameter estimation and uncertainty quantification in the context of adaptive safety-critical control. The key insight enabling our approach is that the parameter estimate generated by the continuous-time recursive least squares (RLS) algorithm at any point in time is an affine transformation of the initial parameter estimate. This property allows for parameterizing such estimates using objects that are closed under affine transformation, such as zonotopes, and enables the efficient propagation of such set-based estimates as time progresses. We illustrate how such an approach facilitates the synthesis of safety-critical controllers for systems with parametric uncertainty and additive disturbances using control barrier functions, and demonstrate the utility of our approach through illustrative examples.

eess.SY↗

arXiv2024

Graph Q-Learning for Combinatorial Optimization

Graph-structured data is ubiquitous throughout natural and social sciences, and Graph Neural Networks (GNNs) have recently been shown to be effective at solving prediction and inference problems on graph data. In this paper, we propose and demonstrate that GNNs can be applied to solve Combinatorial Optimization (CO) problems. CO concerns optimizing a function over a discrete solution space that is often intractably large. To learn to solve CO problems, we formulate the optimization process as a sequential decision making problem, where the return is related to how close the candidate solution is to optimality. We use a GNN to learn a policy to iteratively build increasingly promising candidate solutions. We present preliminary evidence that GNNs trained through Q-Learning can solve CO problems with performance approaching state-of-the-art heuristic-based solvers, using only a fraction of the parameters and training time.

cs.LG↗

arXiv2023

A Flexible and Efficient Temporal Logic Tool for Python: PyTeLo

Temporal logic is an important tool for specifying complex behaviors of systems. It can be used to define properties for verification and monitoring, as well as goals for synthesis tools, allowing users to specify rich missions and tasks. Some of the most popular temporal logics include Metric Temporal Logic (MTL), Signal Temporal Logic (STL), and weighted STL (wSTL), which also allow the definition of timing constraints. In this work, we introduce PyTeLo, a modular and versatile Python-based software that facilitates working with temporal logic languages, specifically MTL, STL, and wSTL. Applying PyTeLo requires only a string representation of the temporal logic specification and, optionally, the dynamics of the system of interest. Next, PyTeLo reads the specification using an ANTLR-generated parser and generates an Abstract Syntax Tree (AST) that captures the structure of the formula. For synthesis, the AST serves to recursively encode the specification into a Mixed Integer Linear Program (MILP) that is solved using a commercial solver such as Gurobi. We describe the architecture and capabilities of PyTeLo and provide example applications highlighting its adaptability and extensibility for various research problems.

cs.LO↗

arXiv2023

Safety-Aware Task Composition for Discrete and Continuous Reinforcement Learning

Compositionality is a critical aspect of scalable system design. Reinforcement learning (RL) has recently shown substantial success in task learning, but has only recently begun to truly leverage composition. In this paper, we focus on Boolean composition of learned tasks as opposed to functional or sequential composition. Existing Boolean composition for RL focuses on reaching a satisfying absorbing state in environments with discrete action spaces, but does not support composable safety (i.e., avoidance) constraints. We advance the state of the art in Boolean composition of learned tasks with three contributions: i) introduce two distinct notions of safety in this framework; ii) show how to enforce either safety semantics, prove correctness (under some assumptions), and analyze the trade-offs between the two safety notions; and iii) extend Boolean composition from discrete action spaces to continuous action spaces. We demonstrate these techniques using modified versions of value iteration in a grid world, Deep Q-Network (DQN) in a grid world with image observations, and Twin Delayed DDPG (TD3) in a continuous-observation and continuous-action Bullet physics environment. We believe that these contributions advance the theory of safe reinforcement learning by allowing zero-shot composition of policies satisfying safety properties.

cs.LG↗

arXiv2023

STL: Surprisingly Tricky Logic (for System Validation)

Much of the recent work developing formal methods techniques to specify or learn the behavior of autonomous systems is predicated on a belief that formal specifications are interpretable and useful for humans when checking systems. Though frequently asserted, this assumption is rarely tested. We performed a human experiment (N = 62) with a mix of people who were and were not familiar with formal methods beforehand, asking them to validate whether a set of signal temporal logic (STL) constraints would keep an agent out of harm and allow it to complete a task in a gridworld capture-the-flag setting. Validation accuracy was $45\% \pm 20\%$ (mean $\pm$ standard deviation). The ground-truth validity of a specification, subjects' familiarity with formal methods, and subjects' level of education were found to be significant factors in determining validation correctness. Participants exhibited an affirmation bias, causing significantly increased accuracy on valid specifications, but significantly decreased accuracy on invalid specifications. Additionally, participants, particularly those familiar with formal methods, tended to be overconfident in their answers, and be similarly confident regardless of actual correctness. Our data do not support the belief that formal specifications are inherently human-interpretable to a meaningful degree for system validation. We recommend ergonomic improvements to data presentation and validation training, which should be tested before claims of interpretability make their way back into the formal methods literature.

cs.AI↗

arXiv2023

Robust Multi-Agent Coordination from CaTL+ Specifications

We consider the problem of controlling a heterogeneous multi-agent system required to satisfy temporal logic requirements. Capability Temporal Logic (CaTL) was recently proposed to formalize such specifications for deploying a team of autonomous agents with different capabilities and cooperation requirements. In this paper, we extend CaTL to a new logic CaTL+, which is more expressive than CaTL and has semantics over a continuous workspace shared by all agents. We define two novel robustness metrics for CaTL+: the traditional robustness and the exponential robustness. The latter is sound, differentiable almost everywhere and eliminates masking, which is one of the main limitations of the traditional robustness metric. We formulate a control synthesis problem to maximize CaTL+ robustness and propose a two-step optimization method to solve this problem. Simulation results are included to illustrate the increased expressivity of CaTL+ and the efficacy of the proposed control synthesis approach.

eess.SY↗

arXiv2023

Learning Minimally-Violating Continuous Control for Infeasible Linear Temporal Logic Specifications

This paper explores continuous-time control synthesis for target-driven navigation to satisfy complex high-level tasks expressed as linear temporal logic (LTL). We propose a model-free framework using deep reinforcement learning (DRL) where the underlying dynamic system is unknown (an opaque box). Unlike prior work, this paper considers scenarios where the given LTL specification might be infeasible and therefore cannot be accomplished globally. Instead of modifying the given LTL formula, we provide a general DRL-based approach to satisfy it with minimal violation. To do this, we transform a previously multi-objective DRL problem, which requires simultaneous automata satisfaction and minimum violation cost, into a single objective. By guiding the DRL agent with a sampling-based path planning algorithm for the potentially infeasible LTL task, the proposed approach mitigates the myopic tendencies of DRL, which are often an issue when learning general LTL tasks that can have long or infinite horizons. This is achieved by decomposing an infeasible LTL formula into several reach-avoid sub-tasks with shorter horizons, which can be trained in a modular DRL architecture. Furthermore, we overcome the challenge of the exploration process for DRL in complex and cluttered environments by using path planners to design rewards that are dense in the configuration space. The benefits of the presented approach are demonstrated through testing on various complex nonlinear systems and compared with state-of-the-art baselines. The Video demonstration can be found here:https://youtu.be/jBhx6Nv224E.

cs.RO↗