Searcharxiv⌕ Search

arXiv subjects

Pushpak Jagtap

Publications and source records attributed to Pushpak Jagtap.

At least 37 records · Page 2Linked to original sources

Towards Certified Sim-to-Real Transfer via Stochastic Simulation-Gap Functions

This paper introduces the notion of stochastic simulation-gap function, which formally quantifies the gap between an approximate mathematical model and a high-fidelity stochastic simulator. Since controllers designed for the mathematical model may fail in practice due to unmodeled gaps, the stochastic simulation-gap function enables the simulator to be interpreted as the nominal model with bounded state- and input-dependent disturbances. We propose a data-driven approach and establish a formal guarantee on the quantification of this gap. Leveraging the stochastic simulation-gap function, we design a controller for the mathematical model that ensures the desired specification is satisfied in the high-fidelity simulator with high confidence, taking a step toward bridging the sim-to-real gap. We demonstrate the effectiveness of the proposed method using a TurtleBot model and a pendulum system in stochastic simulators.

eess.SY↗

Neural Control Barrier Functions for Signal Temporal Logic Specifications with Input Constraints

Signal Temporal Logic (STL) provides a powerful framework to describe complex tasks involving temporal and logical behavior in dynamical systems. This work addresses controller synthesis for continuous-time systems subject to STL specifications and input constraints. We propose a neural network-based framework for synthesizing time-varying control barrier functions (TVCBF) and their corresponding controllers for systems to fulfill a fragment of STL specifications while respecting input constraints. We formulate barrier conditions incorporating the spatial and temporal logic of the given STL specification. We also incorporate a method to refine the time-varying set that satisfies the STL specification for the given input constraints. Additionally, we introduce a validity condition to provide formal safety guarantees across the entire state space. Finally, we demonstrate the effectiveness of the proposed approach through several simulation studies considering different STL tasks for various dynamical systems (including affine and non-affine systems).

eess.SY↗

Prescribed Performance Control of Unknown Euler-Lagrange Systems Under Input Constraints

In this paper, we present a prescribed performance control framework for trajectory tracking in Euler-Lagrange systems with unknown dynamics and prescribed input constraints. The proposed approach enforces hard funnel constraints, meaning that the prescribed performance bounds must not be violated during operation. We derive feasibility conditions that guarantee the tracking error evolves within these predefined funnels while ensuring bounded control inputs. To handle situations where the feasibility conditions are not satisfied, we introduce two approximation-free control strategies: one that actively drives the error back toward the funnel and another that prioritizes safety by preventing further deviation. The effectiveness and robustness of the proposed method are demonstrated through simulation studies and hardware experiments, highlighting its suitability for real-world robotic systems operating under strict input limits.

cs.RO↗

Input-to-State Stabilizing Neural Controllers for Unknown Switched Nonlinear Systems within Compact Sets

This paper develops a neural network based control framework that ensures system safety and input-to-state stability (ISS) for general nonlinear switched systems with unknown dynamics. Leveraging the concept of dwell time, we derive Lyapunov based sufficient conditions under which both safety and ISS of the closed-loop switched system are guaranteed. The feedback controllers and the associated Lyapunov functions are parameterized using neural networks and trained from data collected over a compact state space via deterministic sampling. To provide formal stability guarantees under the learned controllers, we introduce a validity condition based on Lipschitz continuity assumptions, which is embedded directly into the training framework. This ensures that the resulting neural network controllers satisfy provable correctness and stability guarantees beyond the sampled data. As a special case, the proposed framework recovers ISS and safety under arbitrary switching when a common Lyapunov function exists. Simulation results on a representative switched nonlinear system demonstrate the effectiveness of the proposed approach.

eess.SY↗

Scalable and Approximation-free Symbolic Control for Unknown Euler-Lagrange Systems

We propose a novel symbolic control framework for enforcing temporal logic specifications in Euler-Lagrange systems that addresses the key limitations of traditional abstraction-based approaches. Unlike existing methods that require exact system models and provide guarantees only at discrete sampling instants, our approach relies only on bounds on system parameters and input constraints, and ensures correctness for the full continuous-time trajectory. The framework combines scalable abstraction of a simplified virtual system with a closed-form, model-free controller that guarantees trajectories satisfy the original specification while respecting input bounds and remaining robust to unknown but bounded disturbances. We provide feasibility conditions for the construction of confinement regions and analyze the trade-off between efficiency and conservatism. Case studies on pendulum dynamics, a two-link manipulator, and multi-agent systems, including hardware experiments, demonstrate that the proposed approach ensures both correctness and safety while significantly reducing computational time and memory requirements. These results highlight its scalability and practicality for real-world robotic systems where precise models are unavailable and continuous-time guarantees are essential.

eess.SY↗

Spatiotemporal Tubes for Probabilistic Temporal Reach-Avoid-Stay Task in Uncertain Dynamic Environment

In this work, we extend the Spatiotemporal Tube (STT) framework to address Probabilistic Temporal Reach-Avoid-Stay (PrT-RAS) tasks in dynamic environments with uncertain obstacles. We develop a real-time tube synthesis procedure that explicitly accounts for time-varying uncertain obstacles and provides formal probabilistic safety guarantees. The STT is formulated as a time-varying ball in the state space whose center and radius evolve online based on uncertain sensory information. We derive a closed-form, approximation-free control law that confines the system trajectory within the tube, ensuring both probabilistic safety and task satisfaction. Our method offers a formal guarantee for probabilistic avoidance and finite-time task completion. The resulting controller is model-free, approximation-free, and optimization-free, enabling efficient real-time execution while guaranteeing convergence to the target. The effectiveness and scalability of the framework are demonstrated through simulation studies and hardware experiments on mobile robots, a UAV, and a 7-DOF manipulator navigating in cluttered and uncertain environments.

cs.RO↗

Neural Controller for Incremental Stability of Unknown Continuous-time Systems

This work primarily focuses on synthesizing a controller that guarantees an unknown continuous-time system to be incrementally input-to-state stable ($δ$-ISS). In this context, the notion of $δ$-ISS control Lyapunov function ($δ$-ISS-CLF) for the continuous-time system is introduced. Combined with the controller, the $δ$-ISS-CLF guarantees that the system is incrementally stable. As the paper deals with unknown dynamical systems, the controller as well as the $δ$-ISS-CLF are parametrized using neural networks. The data set used to train the neural networks is generated from the state space of the system by proper sampling. Now, to give a formal guarantee that the controller makes the system incrementally stable, we develop a validity condition by having some Lipschitz continuity assumptions and incorporate the condition into the training framework to ensure a provable correctness guarantee at the end of the training process. Finally, we demonstrate the effectiveness of the proposed approach through several case studies: a scalar system with a non-affine, non-polynomial structure, a one-link manipulator system, a nonlinear Moore-Greitzer model of a jet engine, a magnetic levitator system and a rotating rigid spacecraft model.

eess.SY↗

Learning Spatiotemporal Tubes for Temporal Reach-Avoid-Stay Tasks using Physics-Informed Neural Networks

This paper presents a Spatiotemporal Tube (STT)-based control framework for general control-affine MIMO nonlinear pure-feedback systems with unknown dynamics to satisfy prescribed time reach-avoid-stay tasks under external disturbances. The STT is defined as a time-varying ball, whose center and radius are jointly approximated by a Physics-Informed Neural Network (PINN). The constraints governing the STT are first formulated as loss functions of the PINN, and a training algorithm is proposed to minimize the overall violation. The PINN being trained on certain collocation points, we propose a Lipschitz-based validity condition to formally verify that the learned PINN satisfies the conditions over the continuous time horizon. Building on the learned STT representation, an approximation-free closed-form controller is defined to guarantee satisfaction of the T-RAS specification. Finally, the effectiveness and scalability of the framework are validated through two case studies involving a mobile robot and an aerial vehicle navigating through cluttered environments.

cs.RO↗

Computation of Feasible Assume-Guarantee Contracts: A Resilience-based Approach

We propose a resilience-based framework for computing feasible assume-guarantee contracts that ensure the satisfaction of temporal specifications in interconnected discrete-time systems. Interconnection effects are modeled as structured disturbances. We use a resilience metric, the maximum disturbance under which local specifications hold, to refine assumptions and guarantees across subsystems iteratively. We first demonstrate correctness and monotone refinement of guarantees for two subsystems. Then, we extend our approach to general networks of L subsystems using weighted combinations of interconnection effects. We instantiate the framework on linear systems by meeting finite-horizon safety, exact-time reachability, and finite-horizon reachability specifications, and on nonlinear systems by fulfilling general finite-horizon specifications. Our approach is demonstrated through numerical linear examples and a nonlinear DC microgrid case study, showcasing the impact of our framework on verifying temporal logic specifications with compositional reasoning.

eess.SY↗

Scalable Formal Verification of Incremental Stability in Large-Scale Systems Using Graph Neural Networks

This work proposes a novel distributed framework for verifying the incremental stability of large-scale systems with unknown dynamics and known interconnection structures using graph neural networks. Our proposed approach relies on the construction of local incremental Lyapunov functions for subsystems, which are then composed together to obtain a suitable Lyapunov function for the interconnected system. Graph neural networks are used to synthesize these functions in a data-driven fashion. The formal correctness guarantee is then obtained by leveraging Lipschitz bounds of the trained neural networks. Finally, the effectiveness of our approach is validated through two nonlinear case studies.

eess.SY↗

Real-Time Spatiotemporal Tubes for Dynamic Unsafe Sets

This paper presents a real-time control framework for nonlinear pure-feedback systems with unknown dynamics to satisfy reach-avoid-stay tasks within a prescribed time in dynamic environments. To achieve this, we introduce a real-time spatiotemporal tube (STT) framework. An STT is defined as a time-varying ball in the state space whose center and radius adapt online using only real-time sensory input. A closed-form, approximation-free control law is then derived to constrain the system output within the STT, ensuring safety and task satisfaction. We provide formal guarantees for obstacle avoidance and on-time task completion. The effectiveness and scalability of the framework are demonstrated through simulations and hardware experiments on a mobile robot and an aerial vehicle, navigating in cluttered dynamic environments.

cs.RO↗

Approximation-free Control for Signal Temporal Logic Specifications using Spatiotemporal Tubes

This paper presents a spatiotemporal tube (STT)-based control framework for satisfying Signal Temporal Logic (STL) specifications in unknown control-affine systems. We formulate STL constraints as a robust optimization problem (ROP) and recast it as a scenario optimization program (SOP) to construct STTs with formal correctness guarantees. We also propose a closed-form control law that operates independently of the system dynamics, and ensures the system trajectory evolves within the STTs, thereby satisfying the STL specifications. The proposed approach is validated through case studies and comparisons with state-of-the-art methods, demonstrating superior computational efficiency, trajectory quality, and applicability to complex STL tasks.

eess.SY↗

Formally Verified Neural Network Controllers for Incremental Input-to-State Stability of Unknown Discrete-Time Systems

This work aims to synthesize a controller that ensures that an unknown discrete-time system is incrementally input-to-state stable ($δ$-ISS). In this work, we introduce the notion of $δ$-ISS control Lyapunov function ($δ$-ISS-CLF), which, in conjunction with the controller, ensures that the closed-loop system is incrementally ISS. To address the unknown dynamics of the system, we parameterize the controller as well as the $δ$-ISS-CLF as neural networks and learn them by utilizing the sampled data from the state space of the unknown system. To formally verify the obtained $δ$-ISS-CLF, we develop a validity condition and incorporate the condition into the training framework to ensure a provable correctness guarantee at the end of the training process. Finally, the usefulness of the proposed approach is proved using multiple case studies - the first one is a scalar system with a non-affine non-polynomial structure, the second example is a one-link manipulator system, the third system is a nonlinear Moore-Grietzer model of the jet engine and the final one is a rotating rigid spacecraft model.

eess.SY↗

Spatiotemporal Tubes based Control of Unknown Multi-Agent Systems for Temporal Reach-Avoid-Stay Tasks

The paper focuses on designing a controller for unknown dynamical multi-agent systems to achieve temporal reach-avoid-stay tasks for each agent while preventing inter-agent collisions. The main objective is to generate a spatiotemporal tube (STT) for each agent and thereby devise a closed-form, approximation-free, and decentralized control strategy that ensures the system trajectory reaches the target within a specific time while avoiding time-varying unsafe sets and collisions with other agents. In order to achieve this, the requirements of STTs are formulated as a robust optimization problem (ROP) and solved using a sampling-based scenario optimization problem (SOP) to address the issue of infeasibility caused by the infinite number of constraints in ROP. The STTs are generated by solving the SOP, and the corresponding closed-form control is designed to fulfill the specified task. Finally, the effectiveness of our approach is demonstrated through two case studies, one involving omnidirectional robots and the other involving multiple drones modelled as Euler-Lagrange systems.

eess.SY↗

Control Barrier Functions for the Full Class of Signal Temporal Logic Tasks using Spatiotemporal Tubes

This paper introduces a new framework for synthesizing time-varying control barrier functions (TV-CBFs) for general Signal Temporal Logic (STL) specifications using spatiotemporal tubes (STT). We first formulate the STT synthesis as a robust optimization problem (ROP) and solve it through a scenario optimization problem (SOP), providing formal guarantees that the resulting tubes capture the given STL specifications. These STTs are then used to construct TV-CBFs, ensuring that under any control law rendering them invariant, the system satisfies the STL tasks. We demonstrate the framework through case studies on a differential-drive mobile robot and a quadrotor, and provide a comparative analysis showing improved efficiency over existing approaches.

eess.SY↗

Smooth Spatiotemporal Tube Synthesis for Prescribed-Time Reach-Avoid-Stay Control

In this work, we address the issue of controller synthesis for a control-affine nonlinear system to meet prescribed time reach-avoid-stay specifications. Our goal is to improve upon previous methods based on spatiotemporal tubes (STTs) by eliminating the need for circumvent functions, which often lead to abrupt tube modifications and high control effort. We propose an adaptive framework that constructs smooth STTs around static unsafe sets, enabling continuous avoidance while guiding the system toward the target within the prescribed time. A closed-form, approximation-free control law is derived to ensure the system trajectory remains within the tube and satisfies the RAS task. The effectiveness of the proposed approach is demonstrated through a case study, showing a significant reduction in control effort compared to prior methods.

eess.SY↗

Controller for Incremental Input-to-State Practical Stabilization of Partially Unknown systems with Invariance Guarantees

Incremental stability is a property of dynamical systems that ensures the convergence of trajectories with respect to each other rather than a fixed equilibrium point or a fixed trajectory. In this paper, we introduce a related stability notion called incremental input-to-state practical stability (δ-ISpS), ensuring safety guarantees. We also present a feedback linearization based control design scheme that renders a partially unknown system incrementally input-to-state practically stable and safe with formal guarantees. To deal with the unknown dynamics, we utilize Gaussian process regression to approximate the model. Finally, we implement the controller synthesized by the proposed scheme on a manipulator example

eess.SY↗

Periodic Event-Triggered Prescribed Time Control of Euler-Lagrange Systems under State and Input Constraints

This article proposes a periodic event-triggered adaptive barrier control policy for the trajectory tracking problem of perturbed Euler-Lagrangian systems with state, input, and temporal (SIT) constraints. In particular, an approximation-free adaptive-barrier control architecture is designed to ensure prescribed-time convergence of the tracking error to a prescribed bound while rejecting exogenous disturbances. In contrast to existing approaches that necessitate continuous real-time control action, the proposed controller generates event-based updates through periodic evaluation of the triggering condition. Additionally, we derive an upper bound on the monitoring period by analysing the performance degradation of the filtered tracking error to facilitate periodic evaluation of the event-triggered strategy. To this end, a time-varying threshold function is considered in the triggering mechanism to reduce the number of triggers during the transient phase of system behaviour. Notably, the proposed design avoids Zeno behaviour and precludes the need for continuous monitoring of the triggering condition. A simulation and experimental study is undertaken to demonstrate the efficacy of the proposed control scheme.

eess.SY↗