arXiv subjects

Mahathi Anand

Publications and source records attributed to Mahathi Anand.

11 recordsLinked to original sources

arXiv2026

CSymPlan: Certified Symbolic Planning and Control for High-DOF Manipulators

Robot manipulators are commonly engineered around a decoupled motion-generation stack: a planner computes a collision-free path and a lower-level controller tracks the resulting reference. This separation is computationally convenient, but it can produce references that are difficult to execute under actuator limits, tracking error, model mismatch, and small obstacle clearances. We present CSymPlan, a certified symbolic planning and control framework for high-DOF manipulators with two complementary implementations: an offline implementation that precomputes certified reach-avoid feedback policies for known workspaces; and an online implementation that synthesizes or updates symbolic policies at runtime from changing task and perception information using parallelization. The offline implementation reduces the manipulator dynamics to a sampled perturbed double-integrator model in operational space through feedback linearization, treats torque-realization errors, modeling inaccuracies, and measurement uncertainty as bounded disturbances, and refines the synthesized symbolic policy to the Franka FR3 through a quantization--lookup--torque realization pipeline. The online implementation uses the same abstraction and refinement interface, but replaces the precomputed policy table with a runtime pFaces request--synthesis--execution loop. In randomized simulated benchmarks and perception-driven Franka FR3 experiments, both implementations complete reach-avoid tasks with zero safety violations; whenever no certified action exists, the robot holds, replans, or stops safely instead of executing an uncertified command.

cs.RO↗

arXiv2026

Learning from Demonstrations over Riemannian Manifolds using Neural ODEs: An Extended Abstract

Learning from demonstratins (LfD) is usually performed over Euclidean spaces, while the robot state, e.g. orientation, naturally evolves over curved spaces. Therefore, to ensure natural, complex motion generation, we investigate learning from demonstrations over Riemannian manifolds that are capable of encoding both position and orientation data. Here, geodesic paths provide for natural motion between two arbitrary points within the manifold. We propose to numerically estimate geodesics via neural ordinary differential equations, mitigating large computational overhead of existing approaches. Finally, these geodesics can be decoded back into the original task space before deploying on the robot. In this extended abstract, we discuss the architecture of our framework, provide some initial insights from our simulation experiments, including comparison to other geodesic computation mechanisms, and discuss the challenges and prospects for future work.

cs.RO↗

arXiv2026

Safety for Weakly-Hard Control Systems via Graph-Based Barrier Functions

Despite significant advancement in technology, communication and computational failures are still prevalent in safety-critical engineering applications. Often, networked control systems experience packet dropouts, leading to open-loop behavior that significantly affects the behavior of the system. Similarly, in real-time control applications, control tasks frequently experience computational overruns and thus occasionally no new actuator command is issued. This article addresses the safety verification and controller synthesis problem for a class of control systems subject to weakly-hard constraints, i.e., a set of window-based constraints where the number of failures are bounded within a given time horizon. The results are based on a new notion of graph-based barrier functions that are specifically tailored to the considered system class, offering a set of constraints whose satisfaction leads to safety guarantees despite communication failures. Subsequent reformulations of the safety constraints are proposed to alleviate conservatism and improve computational tractability, and the resulting trade-offs are discussed. Finally, several numerical case studies demonstrate the effectiveness of the proposed approach.

eess.SY↗

arXiv2025

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↗

arXiv2025

Safe and Stable Neural Network Dynamical Systems for Robot Motion Planning

Learning safe and stable robot motions from demonstrations remains a challenge, especially in complex, nonlinear tasks involving dynamic, obstacle-rich environments. In this paper, we propose Safe and Stable Neural Network Dynamical Systems S$^2$-NNDS, a learning-from-demonstration framework that simultaneously learns expressive neural dynamical systems alongside neural Lyapunov stability and barrier safety certificates. Unlike traditional approaches with restrictive polynomial parameterizations, S$^2$-NNDS leverages neural networks to capture complex robot motions, providing probabilistic guarantees through split conformal prediction in learned certificates. Experimental results in various 2D and 3D datasets -- including LASA handwriting and demonstrations recorded kinesthetically from the Franka Emika Panda robot -- validate the effectiveness of S$^2$-NNDS in learning robust, safe, and stable motions from potentially unsafe demonstrations. The source code, supplementary material and experiment videos can be accessed via https://github.com/allemmbinn/S2NNDS

cs.RO↗

arXiv2025

Density Matrix-based Dynamics for Quantum Robotic Swarms

In a robotic swarm, parameters such as position and proximity to the target can be described in terms of probability amplitudes. This idea led to recent studies on a quantum approach to the definition of the swarm, including a block-matrix representation. However, the size of such matrix-based representation increases drastically with the swarm size, making them impractical for large swarms. Hence, in this work, we propose a new approach for modeling robotic swarms and robotic networks by considering them as mixed quantum states that can be represented mathematically via density matrices. The size of such an approach only depends on the available degrees of freedom of the robot, and not its swarm size and thus scales well to large swarms. Moreover, it also enables the extraction of local information of the robots from the global swarm information contained in the density matrices, facilitating decentralized behavior that aligns with the collective swarm behavior. Our approach is validated on several simulations including large-scale swarms of up to 1000 robots. Finally, we provide some directions for future research that could potentially widen the impact of our approach.

cs.RO↗

arXiv2025

On the Completeness and Ordering of Path-Complete Barrier Functions

This paper is concerned with path-complete barrier functions which offer a graph-based methodology for verifying safety properties in switched systems. The path-complete framework leverages algebraic (barrier functions) as well as combinatorial (graph) components to characterize a set of safety conditions for switched systems, thus offering high flexibility (two degrees of freedom) in searching for suitable safety certificates. In this paper, we do not propose any new safety criteria. Instead, we further investigate the role that the combinatorial component plays in the safety verification problem. First, we prove that path-completeness, which is a property on a graph that describes the switching sequences, is necessary to obtain a set of valid safety conditions. As a result, the path-complete framework is able to provide a complete characterization of safety conditions for switched systems. Furthermore, we provide a systematic methodology for comparing two path-complete graphs and the conservatism associated with the resulting safety conditions. Specifically, we prove that under some conditions, such as when there exists a simulation relation between two path-complete graphs, it is possible to conclude that one graph is always able to provide less conservative safety conditions than another, independent of the algebraic properties of the switched system and the template of the barrier function under consideration. Such a result paves the way for a systematic use of the path-complete framework with barrier functions, as one can then consistently choose the appropriate graph that provides less conservative safety conditions.

eess.SY↗

arXiv2021

Verification of Switched Stochastic Systems via Barrier Certificates

The paper presents a methodology for temporal logic verification of continuous-time switched stochastic systems. Our goal is to find the lower bound on the probability that a complex temporal property is satisfied over a finite time horizon. The required temporal properties of the system are expressed using a fragment of linear temporal logic, called safe-LTL with respect to finite traces. Our approach combines automata-based verification and the use of barrier certificates. It relies on decomposing the automaton associated with the negation of specification into a sequence of simpler reachability tasks and compute upper bounds for these reachability probabilities by means of common or multiple barrier certificates. Theoretical results are illustrated by applying a counter-example guided inductive synthesis framework to find barrier certificates.

cs.LO↗

arXiv2021

Verification of Hyperproperties for Uncertain Dynamical Systems via Barrier Certificates

Hyperproperties are system properties that require quantification over multiple execution traces of a system. Hyperproperties can express several specifications of interest for cyber-physical systems--such as opacity, robustness, and noninterference--which cannot be expressed using linear-time properties. This paper presents for the first time a discretization-free approach for the formal verification of discrete-time uncertain dynamical systems against hyperproperties. The proposed approach involves decomposition of complex hyperproperties into several verification conditions by exploiting the automata-based structures corresponding to the complements of the original specifications. These verification conditions are then discharged by synthesizing so-called augmented barrier certificates, which provide certain safety guarantees for the underlying system. For systems with polynomial-type dynamics, we present a sound procedure to synthesize polynomial-type augmented barrier certificates by reducing the problem to sum-of-squares optimizations. We demonstrate the effectiveness of our proposed approaches on two physical case studies against two important hyperproperties: initial-state opacity and initial-state robustness.

eess.SY↗

arXiv2021

Compositional Synthesis of Control Barrier Certificates for Networks of Stochastic Systems against $\omega$-Regular Specifications

This paper is concerned with a compositional scheme for the construction of control barrier certificates for interconnected discrete-time stochastic systems. The main objective is to synthesize switching control policies against $\omega$-regular properties that can be described by accepting languages of deterministic Streett automata (DSA) along with providing probabilistic guarantees for the satisfaction of such specifications. The proposed framework leverages the interconnection topology and a notion of so-called \emph{control sub-barrier certificates} of subsystems, which are used to compositionally construct control barrier certificates of interconnected systems by imposing some dissipativity-type compositionality conditions. We propose a systematic approach to decompose high-level $\omega$-regular specifications into simpler tasks by utilizing the automata corresponding to the specifications. In addition, we formulate an alternating direction method of multipliers (ADMM) optimization problem in order to obtain suitable control sub-barrier certificates of subsystems while satisfying compositionality conditions. For systems with polynomial dynamics, we provide a sum-of-squares (SOS) optimization problem for the computation of control sub-barrier certificates and local control policies of subsystems. Finally, we demonstrate the effectiveness of our proposed approaches by applying them to a physical case study.

eess.SY↗

arXiv2021

From Small-Gain Theory to Compositional Construction of Barrier Certificates for Large-Scale Stochastic Systems

This paper is concerned with a compositional approach for the construction of control barrier certificates for large-scale interconnected stochastic systems while synthesizing hybrid controllers against high-level logic properties. Our proposed methodology involves decomposition of interconnected systems into smaller subsystems and leverages the notion of control sub-barrier certificates of subsystems, enabling one to construct control barrier certificates of interconnected systems by employing some max-type small-gain conditions. The main goal is to synthesize hybrid controllers enforcing complex logic properties including the ones represented by the accepting language of deterministic finite automata, while providing probabilistic guarantees on the satisfaction of given specifications in bounded-time horizons. To do so, we propose a systematic approach to first decompose high-level specifications into simple reachability tasks by utilizing automata corresponding to the complement of specifications. We then construct control sub-barrier certificates and synthesize local controllers for those simpler tasks and combine them to obtain a hybrid controller that ensures satisfaction of the complex specification with some lower bound on the probability of satisfaction. To compute control sub-barrier certificates and corresponding local controllers, we provide two systematic approaches based on sum-of-squares (SOS) optimization program and counter-example guided inductive synthesis (CEGIS) framework. We finally apply our proposed techniques to two physical case studies.

eess.SY↗