@conference {, title = {MPC-guided Imitation Learning of Bayesian Neural Network Policies for the Artificial Pancreas}, booktitle = {Proceedings of CDC 2021, the 60th IEEE Conference on Decision and Control}, year = {2021}, month = {12/2021}, author = {H. Chen and N. Paoletti and S. A. Smolka and S. Lin} } @article {, title = {Neural Predictive Monitoring and a Comparison of Frequentist and Bayesian Approaches}, journal = {International Journal on Software Tools for Technology Transfer}, year = {2021}, month = {05/2021}, author = {L. Bortolussi and F. Cairoli and N. Paoletti and S. A. Smolka and S. D. Stoller} } @article {, title = {Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems}, journal = {IEEE Access}, year = {2020}, author = {F. Shmarov and S. Soudjani and N. Paoletti and E. Bartocci and S. Lin and S. A. Smolka and P. Zuliani} } @conference {, title = {Bayesian Neural Predictive Monitoring}, booktitle = {Proceedings of OVERLAY-20, Second Workshop on Formal Methods for AI}, year = {2020}, month = {09/2020}, author = {L. Bortolussi and F. Cairoli and N. Paoletti and S. A. Smolka and S. D. Stoller} } @article {, title = {Data-Driven Robust Control for a Closed-Loop Artificial Pancreas}, journal = {IEEE/ACM Transactions on Computational Biology and Bioinformatics}, volume = {17}, year = {2020}, month = {11/2020}, chapter = {1981}, author = {N. Paoletti and K. S. Liu and H. Chen and S. A. Smolka and S. Lin} } @article {, title = {Data-Driven Uncertainty Quantification for Cardiac Electrophysiological Models: Impact of Physiological Variability on Action Potential and Spiral Wave Dynamics}, journal = {Frontiers in physiology}, volume = {11}, year = {2020}, month = {11/2020}, url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:tuHXwOkdijsC}, author = {Pras Pathmanathan and Suran K Galappaththige and Jonathan M Cordeiro and Abouzar Kaboudian and Flavio H Fenton and Richard A Gray} } @article {, title = {Excitable dynamics in neural and cardiac systems}, journal = {Communications in Nonlinear Science and Numerical Simulation}, volume = {86}, year = {2020}, month = {07/2020}, url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:hMsQuOkrut0C}, author = {Roberto Barrio and Stephen Coombes and Mathieu Desroches and Flavio Fenton and Stefan Luther and Esther Pueyo} } @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} } @conference {, title = {Towards Automated Comprehension and Alignment of Cardiac Models at the System Invariant Level}, booktitle = {CSBio{\textquoteright}20: Proceedings of the Eleventh International Conference on Computational Systems-Biology and Bioinformatics}, year = {2020}, author = {Huang, Samuel and Diep, Madeline and Jang, Kuk and Cherry, Elizabeth M and Fenton, Flavio H and Cleaveland, Rance and Lindvall, Mikael and Mangharam, Rahul and Porter, Adam} } @conference {, title = {Declarative vs Rule-based Control for Flocking Dynamics}, booktitle = {Proceedings of the 33rd Annual ACM Symposium on Applied Computing}, year = {2018}, publisher = {ACM}, organization = {ACM}, address = {New York, NY, USA}, isbn = {978-1-4503-5191-1}, doi = {10.1145/3167132.3167222}, url = {http://doi.acm.org/10.1145/3167132.3167222}, author = {Mehmood, Usama and Paoletti, Nicola and Phan, Dung and Grosu, Radu and Lin, Shan and Stoller, Scott D. and Tiwari, Ashish and Yang, Junxing and Smolka, Scott A.} } @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 = {Closed-loop quantitative verification of rate-adaptive pacemakers}, journal = {ACM Transactions on Cyber-Physical Systems, to appear}, year = {2017}, abstract = {

Cardiac pacemakers are electrical devices that treat arrhythmias delivering electrical stimuli to the patient heart {\textbullet} Rate-adaptation: regulation of pacing rate according to patient{\textquoteright}s needs (e.g. increased pacing rate during exercise) {\textbullet} Programming of rate-adaptation parameters depends on many patient-specific factors (age, lifestyle, tolerance to rapid pacing, {\textellipsis}) {\textbullet} Effective personalisation achievable only through extensive exercise testing: intolerable for a cardiac patient {\textbullet} We introduce a data-driven and model-based approach for subjectspecific verification of rate-adaptive pacemakers

}, author = {Nicola Paoletti and Andrea Patan{\`e} and Marta Kwiatkowska} } @article {, title = {Collision Avoidance for Mobile Robots with Limited Sensing and Limited Information about Moving Obstacles}, journal = {Formal Methods in System Design}, year = {2017}, month = {01/2017}, author = {D. Phan and J. Yang and R. Grosu and S. A. Smolka and S. D. Stoller} } @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 = {{SMT-based Synthesis of Safe and Robust PID Controllers for Stochastic Hybrid Systems}}, booktitle = {Haifa Verification Conference, to appear}, year = {2017}, abstract = {

Abstract. 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 use in industry, no automated method currently exists for deriving a PID controller (or any other type of controller, for that matter) with safety and performance guarantees for such a general class of systems. In particular, we consider hybrid systems with nonlinear dynamics (Lipschitzcontinuous ordinary differential equations) and random parameters, and we synthesize PID controllers such that the resulting closed-loop systems satisfy safety and performance constraints given as probabilistic bounded reachability properties. Our technique leverages SMT solvers over the reals and nonlinear differential equations to provide formal guarantees that the synthesized controllers satisfy such properties. These controllers are also robust by design since they minimize the probability of reaching an unsafe state in the presence of random disturbances. We apply our approach to the problem of insulin regulation for type 1 diabetes, synthesizing controllers with robust responses to large random meal disturbances, thereby enabling them to maintain blood glucose levels within healthy, safe ranges.

}, author = {Fedor Shmarov and Nicola Paoletti and Ezio Bartocci and Shan Lin and Scott Smolka and Paolo Zuliani} } @conference {, title = {Bifurcation Analysis of Cardiac Alternans Using δ -Decidability.}, booktitle = {CMSB}, year = {2016}, publisher = {Springer}, organization = {Springer}, keywords = {dblp}, isbn = {978-3-319-45176-3}, url = {http://dblp.uni-trier.de/db/conf/cmsb/cmsb2016.html$\#$IslamBKCCFGJS16}, author = {Islam, Md. Ariful and Byrne, Greg and Kong, Soonho and Clarke, Edmund M. and Cleaveland, Rance and Fenton, Flavio H. and Grosu, Radu and Jones, Paul L. and Smolka, Scott A.}, editor = {Bartocci, Ezio and Li{\`o}, Pietro and Paoletti, Nicola} } @conference {, title = {Cybercardia project: Modeling, verification and validation of implantable cardiac devices}, booktitle = {2016 IEEE International Conference on Bioinformatics and Biomedicine (BIBM)}, year = {2016}, publisher = {IEEE}, organization = {IEEE}, author = {Islam, Md Ariful and Lim, Hyunkyung and Paoletti, Nicola and Abbas, Houssam and Jiang, Zhihao and Cyranka, Jacek and Cleaveland, Rance and Gao, Sicun and Clarke, Edmund and Grosu, Radu and others} }