arXiv subjects

Shouvik Roy

Publications and source records attributed to Shouvik Roy.

5 recordsLinked to original sources

arXiv2025

Cumulative-Time Signal Temporal Logic

Signal Temporal Logic (STL) is a widely adopted specification language in cyber-physical systems for expressing critical temporal requirements, such as safety conditions and response time. However, STL's expressivity is not sufficient to capture the cumulative duration during which a property holds within an interval of time. To overcome this limitation, we introduce Cumulative-Time Signal Temporal Logic (CT-STL) that operates over discrete-time signals and extends STL with a new cumulative-time operator. This operator compares the sum of all time steps for which its nested formula is true with a threshold. We present both a qualitative and a quantitative (robustness) semantics for CT-STL and prove both their soundness and completeness properties. We provide an efficient online monitoring algorithm for both semantics. Finally, we show the applicability of CT-STL in two case studies: specifying and monitoring cumulative temporal requirements for a microgrid and an artificial pancreas.

cs.LO↗

arXiv2022

A Barrier Certificate-based Simplex Architecture for Systems with Approximate and Hybrid Dynamics

We present Barrier-based Simplex (Bb-Simplex), a new, provably correct design for runtime assurance of continuous dynamical systems. Bb-Simplex is centered around the Simplex control architecture, which consists of a high-performance advanced controller that is not guaranteed to maintain safety of the plant, a verified-safe baseline controller, and a decision module that switches control of the plant between the two controllers to ensure safety without sacrificing performance. In Bb-Simplex, Barrier certificates are used to prove that the baseline controller ensures safety. Furthermore, Bb-Simplex features a new automated method for deriving, from the barrier certificate, the conditions for switching between the controllers. Our method is based on the Taylor expansion of the barrier certificate and yields computationally inexpensive switching conditions. We also propose extensions to Bb-Simplex to enable its use in hybrid systems, which have multiple modes each with its own dynamics, and to support its use when only approximate dynamics (not exact dynamics) are available, for both continuous-time and hybrid dynamical systems. We consider significant applications of Bb-Simplex to microgrids featuring advanced controllers in the form of neural networks trained using reinforcement learning. These microgrids are modeled in RTDS, an industry-standard high-fidelity, real-time power systems simulator. Our results demonstrate that Bb-Simplex can automatically derive switching conditions for complex continuous-time and hybrid systems, the switching conditions are not overly conservative, and Bb-Simplex ensures safety even in the presence of adversarial attacks on the neural controller when only approximate dynamics (with an error bound) are available.

eess.SY↗

arXiv2020

A Distributed Simplex Architecture for Multi-Agent Systems

We present Distributed Simplex Architecture (DSA), a new runtime assurance technique that provides safety guarantees for multi-agent systems (MASs). DSA is inspired by the Simplex control architecture of Sha et al., but with some significant differences. The traditional Simplex approach is limited to single-agent systems or a MAS with a centralized control scheme. DSA addresses this limitation by extending the scope of Simplex to include MASs under distributed control. In DSA, each agent has a local instance of traditional Simplex such that the preservation of safety in the local instances implies safety for the entire MAS. We provide a proof of safety for DSA, and present experimental results for several case studies, including flocking with collision avoidance, safe navigation of ground rovers through way-points, and the safe operation of a microgrid.

cs.MA↗

arXiv2020

Learning Distributed Controllers for V-Formation

We show how a high-performing, fully distributed and symmetric neural V-formation controller can be synthesized from a Centralized MPC (Model Predictive Control) controller using Deep Learning. This result is significant as we also establish that under very reasonable conditions, it is impossible to achieve V-formation using a deterministic, distributed, and symmetric controller. The learning process we use for the neural V-formation controller is significantly enhanced by CEGkR, a Counterexample-Guided k-fold Retraining technique we introduce, which extends prior work in this direction in important ways. Our experimental results show that our neural V-formation controller generalizes to a significantly larger number of agents than for which it was trained (from 7 to 15), and exhibits substantial speedup over the MPC-based controller. We use a form of statistical model checking to compute confidence intervals for our neural V-formation controller's convergence rate and time to convergence.

cs.MA↗

arXiv2019

Neural Flocking: MPC-based Supervised Learning of Flocking Controllers

We show how a distributed flocking controller can be synthesized using deep learning from a centralized controller which generates the trajectories of the flock. Our approach is based on supervised learning, with the centralized controller providing the training data to the learning agent, i.e., the synthesized distributed controller. We use Model Predictive Control (MPC) for the centralized controller, an approach that has been successfully demonstrated on flocking problems. MPC-based flocking controllers are high-performing but also computationally expensive. By learning a symmetric distributed neural flocking controller from a centralized MPC-based flocking controller, we achieve the best of both worlds: the neural controllers have high performance (on par with the MPC controllers) and high efficiency. Our experimental results demonstrate the sophisticated nature of the distributed controllers we learn. In particular, the neural controllers are capable of achieving myriad flocking-oriented control objectives, including flocking formation, collision avoidance, obstacle avoidance, predator avoidance, and target seeking. Moreover, they generalize the behavior seen in the training data in order to achieve these objectives in a significantly broader range of scenarios.

cs.MA↗