@booklet {, title = {Adversarial Training is Not Ready for Robot Learning}, year = {2021}, author = {Mathias Lechner and Ramin Hasani and Radu Grosu and Daniela Rus and Thomas A. Henzinger} } @booklet {, title = {Lagrangian Reachtubes: The Next Generation}, year = {2020}, author = {Sophie Gruenbacher and Jacek Cyranka and Mathias Lechner and Md. Ariful Islam and Scott A. Smolka and Radu Grosu} } @booklet {, title = {Learning Distributed Controllers for V-Formation}, year = {2020}, author = {Shouvik Roy and Usama Mehmood and Radu Grosu and Scott A. Smolka and Scott D. Stoller and Ashish Tiwari} } @booklet {, title = {Liquid Time-constant Networks}, year = {2020}, author = {Ramin Hasani and Mathias Lechner and Alexander Amini and Daniela Rus and Radu Grosu} } @booklet {, title = {Neural Flocking: MPC-based Supervised Learning of Flocking Controllers}, year = {2020}, author = {Shouvik Roy and Usama Mehmood and Radu Grosu and Scott A. Smolka and Scott D. Stoller and Ashish Tiwari} } @booklet {, title = {Neural Simplex Architecture}, year = {2020}, author = {Dung T. Phan and Radu Grosu and Nils Jansen and Nicola Paoletti and Scott A. Smolka and Scott D. Stoller} } @booklet {, title = {On The Verification of Neural ODEs with Stochastic Guarantees}, year = {2020}, author = {Sophie Gruenbacher and Ramin Hasani and Mathias Lechner and Jacek Cyranka and Scott A. Smolka and Radu Grosu} } @article {, title = {An Algebraic Framework for Runtime Verification}, journal = {CoRR}, volume = {abs/1802.03775}, year = {2018}, url = {http://arxiv.org/abs/1802.03775}, author = {Stefan Jaksic and Ezio Bartocci and Radu Grosu and Dejan Nickovic} } @article {, title = {Dynamic Network Model from Partial Observations}, journal = {CoRR}, volume = {abs/1805.10616}, year = {2018}, url = {http://arxiv.org/abs/1805.10616}, author = {Elahe Ghalebi K. and Baharan Mirzasoleiman and Radu Grosu and Jure Leskovec} } @conference {, title = {Neural State Classification for Hybrid Systems}, booktitle = {Proc.\ 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018)}, year = {2018}, publisher = {Springer-Verlag}, organization = {Springer-Verlag}, author = {Dung Phan and Nicola Paoletti and Timothy Zhang and Radu Grosu and Scott A. Smolka and Scott D. Stoller} } @article {, title = {Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans}, journal = {Theoretical Computer Science}, year = {2018}, month = {02/2018}, abstract = {

Using a probabilistic reachability-based approach, we present a multi-parameter bifurcation analysis of electrical alternans in the two-current Mitchell{\textendash}Schaeffer (MS) cardiac-cell model. Electrical alternans is a phenomenon characterized by a variation in successive Action Potential Durations generated by a cardiac cell or tissue. Alternans are known to initiate re-entrant waves and are an important physiological indicator of an impending life-threatening arrhythmia such as ventricular fibrillation. The multi-parameter bifurcation analysis we perform identifies a bifurcation hypersurface in the MS model parameter space, such that a small perturbation to this region results in a transition from highly likely alternans to highly likely non-alternans behavior. Our approach to this problem rests on encoding alternans-like behavior in the MS model as a five-mode, multinomial hybrid automaton. To perform multi-parameter bifurcation analysis of cardiac alternans, we first treat the parameters in question as bounded random variables. We then apply a sophisticated guided-search-based probabilistic reachability analysis to compute a bounded bifurcation region (possibly very tight) that contains the bifurcation hypersurface (BH). Our probabilistic reachability analysis uses a technique that combines a δ-decision procedure with statistical tests. In the process of computing the bifurcation region, we further partition the parameter space into two more regions such that any valuation chosen from one of the regions will either produce alternans or non-alternans behavior with a probability greater than a user-defined threshold.

}, keywords = {Bifurcation analysis, Cardiac alternans, Cardiac modeling, Formal methods, Hybrid systems, Probabilistic reachability}, issn = {0304-3975}, doi = {https://doi.org/10.1016/j.tcs.2018.02.005}, url = {http://www.sciencedirect.com/science/article/pii/S0304397518300823}, author = {Md. Ariful Islam and Rance Cleaveland and FLAVIO H. FENTON and Radu Grosu and Paul L. Jones and Scott A. Smolka} } @conference {, title = {Unsupervised Wafermap Patterns Clustering via Variational Autoencoders}, booktitle = {2018 International Joint Conference on Neural Networks (IJCNN)}, year = {2018}, month = {07/2018}, publisher = {IEEE}, organization = {IEEE}, address = {Rio, Brasil}, author = {Peter Tulala and Hamidreza Mahyar and Elahe Ghalebi and Radu Grosu} } @conference {, title = {Lagrangian Reachabililty}, booktitle = {Computer Aided Verification - 29th International Conference, {CAV} 2017 Proceedings, Part {I}}, year = {2017}, abstract = {

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 of the Cauchy-Green stretching factor (SF), which is derived from an over-approximation of the gradient of the solution flows. The SF measures the discrepancy between two states propagated by the system solution from two initial states lying in a well-defined region, thereby allowing LRT to compute a reachtube with a ball-overestimate in a metric where the computed enclosure is as tight as possible. To evaluate its performance, we implemented a prototype of LRT in C++/Matlab, and ran it on a set of well-established benchmarks. Our results show that LRT compares very favorably with respect to the CAPD and Flow* tools.

}, doi = {10.1007/978-3-319-63387-9_19}, author = {Jacek Cyranka and Md. Ariful Islam and Greg Byrne and Paul L. Jones and Scott A. Smolka and Radu Grosu} } @conference {, title = {Quantitative Regular Expressions for Arrhythmia Detection Algorithms}, booktitle = {International Conference on Computational Methods in Systems Biology}, year = {2017}, month = {09/2017}, publisher = {Springer, Cham}, organization = {Springer, Cham}, address = {Darmstadt, Germany }, abstract = {

Motivated by the problem of verifying the correctness of arrhythmia-detection algorithms, we present a formalization of these algorithms in the language of Quantitative Regular Expressions. QREs are a flexible formal language for specifying complex numerical queries over data streams, with provable runtime and memory consumption guarantees. The medical-device algorithms of interest include peak detection (where a peak in a cardiac signal indicates a heartbeat) and various discriminators, each of which uses a feature of the cardiac signal to distinguish fatal from non-fatal arrhythmias. Expressing these algorithms{\textquoteright} desired output in current temporal logics, and implementing them via monitor synthesis, is cumbersome, error-prone, computationally expensive, and sometimes infeasible.

In contrast, we show that a range of peak detectors (in both the time and wavelet domains) and various discriminators at the heart of today{\textquoteright}s arrhythmia-detection devices are easily expressible in QREs. The fact that one formalism (QREs) is used to describe the desired end-to-end operation of an arrhythmia detector opens the way to formal analysis and rigorous testing of these detectors{\textquoteright} correctness and performance. Such analysis could alleviate the regulatory burden on device developers when modifying their algorithms. The performance of the peak-detection QREs is demonstrated by running them on real patient data, on which they yield results on par with those provided by a cardiologist.

}, isbn = {978-3-319-67471-1}, doi = {https://doi.org/10.1007/978-3-319-67471-1_2}, author = {Houssam Abbas and Alena Rodionova and Ezio Bartocci and Scott A. Smolka and Radu Grosu} }