67 citations · 173 across the 30 of their papers we have counts for
33 papers
Handling Open-Vocabulary Constructs in Formalizing Specifications: Retrieval-Augmented Parsing with Expert Knowledge
Mohammad Saqib Hasan, Sayontan Ghosh, Dhruv Verma +4
We study the problem of Open-Vocabulary Constructs(OVCs) -- ones not known beforehand -- in the context of converting natural language (NL) specifications into formal languages (e.…
Cumulative-Time Signal Temporal Logic
Hongkai Chen, Zeyu Zhang, Shouvik Roy +4
Signal Temporal Logic (STL) is a widely adopted specification language in cyber-physical systems for expressing critical temporal requirements, such as safety conditions and respon…
An STL-based Approach to Resilient Control for Cyber-Physical Systems
Hongkai Chen, Scott A. Smolka, Nicola Paoletti +1
We present ResilienC, a framework for resilient control of Cyber-Physical Systems subject to STL-based requirements. ResilienC utilizes a recently developed formalism for specifyin…
An STL-based Formulation of Resilience in Cyber-Physical Systems
Hongkai Chen, Shan Lin, Scott A. Smolka +1
Resiliency is the ability to quickly recover from a violation and avoid future violations for as long as possible. Such a property is of fundamental importance for Cyber-Physical S…
Multi-Agent Spatial Predictive Control with Application to Drone Flocking (Extended Version)
Andreas Brandstätter, Scott A. Smolka, Scott D. Stoller +2
We introduce the novel concept of Spatial Predictive Control (SPC) to solve the following problem: given a collection of agents (e.g., drones) with positional low-level controllers…
GoTube: Scalable Stochastic Verification of Continuous-Depth Models
Sophie Gruenbacher, Mathias Lechner, Ramin Hasani +4
We introduce a new stochastic verification algorithm that formally quantifies the behavioral robustness of any time-continuous process formulated as a continuous-depth model. Our a…
The Black-Box Simplex Architecture for Runtime Assurance of Autonomous CPS
Usama Mehmood, Sanaz Sheikhi, Stanley Bak +2
The Simplex Architecture is a runtime assurance framework where control authority may switch from an unverified and potentially unsafe advanced controller to a backup baseline cont…
A Distributed Simplex Architecture for Multi-Agent Systems
Usama Mehmood, Scott D. Stoller, Radu Grosu +3
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…
On The Verification of Neural ODEs with Stochastic Guarantees
Sophie Gruenbacher, Ramin Hasani, Mathias Lechner +3
We show that Neural ODEs, an emerging class of time-continuous neural networks, can be verified by solving a set of global-optimization problems. For this purpose, we introduce Sto…
Lagrangian Reachtubes: The Next Generation
Sophie Gruenbacher, Jacek Cyranka, Mathias Lechner +3
We introduce LRT-NG, a set of techniques and an associated toolset that computes a reachtube (an over-approximation of the set of reachable states over a given time horizon) of a n…
Learning Distributed Controllers for V-Formation
Shouvik Roy, Usama Mehmood, Radu Grosu +3
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 D…
MPC-guided Imitation Learning of Neural Network Policies for the Artificial Pancreas
Hongkai Chen, Nicola Paoletti, Scott A. Smolka +1
Even though model predictive control (MPC) is currently the main algorithm for insulin control in the artificial pancreas (AP), it usually requires complex online optimizations, wh…
V-Formation via Model Predictive Control
Radu Grosu, Anna Lukina, Scott A. Smolka +3
We present recent results that demonstrate the power of viewing the problem of V-formation in a flock of birds as one of Model Predictive Control (MPC). The V-formation-MPC marriag…
Neural Flocking: MPC-based Supervised Learning of Flocking Controllers
Shouvik Roy, Usama Mehmood, Radu Grosu +3
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 ba…
Neural Simplex Architecture
Dung T. Phan, Radu Grosu, Nils Jansen +3
We present the Neural Simplex Architecture (NSA), a new approach to runtime assurance that provides safety guarantees for neural controllers (obtained e.g. using reinforcement lear…
Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems
Fedor Shmarov, Sadegh Soudjani, Nicola Paoletti +4
We present a new method for the automated synthesis of digital controllers with formal safety guarantees for systems with nonlinear dynamics, noisy output measurements, and stochas…
Tight Continuous-Time Reachtubes for Lagrangian Reachability
Jacek Cyranka, Md. Ariful Islam, Scott A. Smolka +2
We introduce continuous Lagrangian reachability (CLRT), a new algorithm for the computation of a tight and continuous-time reachtube for the solution flows of a nonlinear, time-var…
Neural State Classification for Hybrid Systems
Dung Phan, Nicola Paoletti, Timothy Zhang +3
We introduce the State Classification Problem (SCP) for hybrid systems, and present Neural State Classification (NSC) as an efficient solution technique. SCP generalizes the model…
Adaptive Neighborhood Resizing for Stochastic Reachability in Multi-Agent Systems
Anna Lukina, Ashish Tiwari, Scott A. Smolka +1
We present DAMPC, a distributed, adaptive-horizon and adaptive-neighborhood algorithm for solving the stochastic reachability problem in multi-agent systems, in particular flocking…
How to Learn a Model Checker
Dung Phan, Radu Grosu, Nicola Paoletti +2
We show how machine-learning techniques, particularly neural networks, offer a very effective and highly efficient solution to the approximate model-checking problem for continuous…
Declarative vs Rule-based Control for Flocking Dynamics
Usama Mehmood, Nicola Paoletti, Dung Phan +6
The popularity of rule-based flocking models, such as Reynolds' classic flocking model, raises the question of whether more declarative flocking models are possible. This question…
Automated Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems
Fedor Shmarov, Nicola Paoletti, Ezio Bartocci +3
We present a new method for the automated synthesis of safe and robust Proportional-Integral-Derivative (PID) controllers for stochastic hybrid systems. Despite their widespread us…
Data-Driven Robust Control for Type 1 Diabetes Under Meal and Exercise Uncertainties
Nicola Paoletti, Kin Sum Liu, Scott A. Smolka +1
We present a fully closed-loop design for an artificial pancreas (AP) which regulates the delivery of insulin for the control of Type I diabetes. Our AP controller operates in a fu…
Lagrangian Reachabililty
Jacek Cyranka, Md. Ariful Islam, Greg Byrne +3
We introduce LRT, a new Lagrangian-based ReachTube computation algorithm that conservatively approximates the set of reachable states of a nonlinear dynamical system. LRT makes use…