@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 = {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} } @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} } @inbook {, title = {Process Algebra and Model Checking}, booktitle = {Handbook of Model Checking.}, year = {2018}, pages = {1149{\textendash}1195}, doi = {10.1007/978-3-319-10575-8\_32}, url = {https://doi.org/10.1007/978-3-319-10575-8\_32}, author = {Rance Cleaveland and A. W. Roscoe and Scott A. Smolka} } @conference {, title = {{Data-Driven Robust Control for Type 1 Diabetes Under Meal and Exercise Uncertainties}}, booktitle = {Computational Methods in Systems Biology}, year = {2017}, publisher = {Springer}, organization = {Springer}, abstract = {

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 fully automated fashion, without requiring any manual interaction (e.g. in the form of meal announcements) with the patient. A major obstacle to achieving closed-loop insulin control is the uncertainty in those aspects of a patient{\textquoteright}s daily behavior that significantly affect blood glucose, especially in relation to meals and physical activity. To handle such uncertainties, we develop a data-driven robust model-predictive control framework, where we capture a wide range of individual meal and exercise patterns using uncertainty sets learned from historical data. These sets are then used in the controller and state estimator to achieve automated, precise, and personalized insulin therapy. We provide an extensive in silico evaluation of our robust AP design, demonstrating the potential of this approach, without explicit meal announcements, to support high carbohydrate disturbances and to regulate glucose levels in large clusters of virtual patients learned from population-wide survey data.

}, doi = {10.1007/978-3-319-67471-1_13}, author = {Nicola Paoletti and Kin Sum Liu and Scott A. Smolka and Shan Lin} } @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} }