@conference {, title = {Collision-Free 3D Flocking Using the Distributed Simplex Architecture}, booktitle = {Proceedings of ISoLA Extra in Rhodes}, year = {2021}, month = {10/2021}, author = {U. Mehmood and R. Grosu and S. A. Smolka and S. D. Stoller} } @conference {, title = {Distributed Control for Flocking Maneuvers via Acceleration-Weighted Neighborhooding}, booktitle = {Proceedings of ACC 2021, The 2021 American Control Conference}, year = {2021}, month = {06/2021}, author = {S. Roy and U. Mehmood and R. Grosu and S. A. Smolka and S. D. Stoller and A. Tiwari} } @conference {, title = {A Distributed Simplex Architecture for Multi-Agent Systems}, booktitle = {Proceedings of SETTA 2021, Symposium on Dependable Software Engineering}, year = {2021}, month = {11/2021}, author = {U. Mehmood and S. D. Stoller and R. Grosu and S. Roy and A. Damare and S. D. Smolka} } @conference {, title = {Model-Checking Support for File System Development}, booktitle = {Proceeding of HotStorage {\textquoteright}21, the 13th ACM Workshop on Hot Topics in Storage and File Systems}, year = {2021}, month = {07/2021}, author = {W. Su and Y. Liu and G. Ganesan and G. Holzmann and G. Kuenning and S. A. Smolka and E. Zadok} } @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 = {Quantifying arrhythmic long QT effects of hydroxychloroquine and azithromycin with whole-heart optical mapping and simulations}, journal = {Heart Rhythm O2}, volume = {2}, year = {2021}, month = {08/2021}, url = {https://scholar.google.com/citations?view_op=view_citation\&hl=en\&user=jKiNd-0AAAAJ\&sortby=pubdate\&citation_for_view=jKiNd-0AAAAJ:Ug5p-4gJ2f0C}, author = {Ilija Uzelac and Abouzar Kaboudian and Shahriar Iravanian and Jimena G Siles-Paredes and James C Gumbart and Hiroshi Ashikaga and Neal Bhatia and Robert F Gilmour Jr and Elizabeth M Cherry and Flavio H Fenton} } @conference {, title = {Safe CPS from Unsafe Controllers}, booktitle = {Proceedings of CAADSPC 2001, the 2021 CPS-IoT Workshop on Computation-Aware Algorithmic Design for Cyber-Physical Systems}, year = {2021}, month = {06/2021}, author = {U. Mehmood and S. Bak and S. A. Smolka and S. D. Stoller} } @conference {, title = {Verification of Neural ODEs with Stochastic Guarantees}, booktitle = {Proceedings of AAAI-21, 35th AAAI Conference on Artificial Intelligence}, year = {2021}, month = {02/2021}, author = {S. Gruenbacher and J. Cyranka and M. Lechner and S. A. Smolka and R. Grosu} } @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} } @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} } @conference {, title = {A Natural Lottery Ticket Winner: Reinforcement Learning with Ordinary Neural Circuits}, booktitle = {Proceedings of the 37th International Conference on Machine Learning}, year = {2020}, month = {13{\textendash}18 Jul}, publisher = {PMLR}, organization = {PMLR}, abstract = {

We propose a neural information processing system obtained by re-purposing the function of a biological neural circuit model to govern simulated and real-world control tasks. Inspired by the structure of the nervous system of the soil-worm, C. elegans, we introduce ordinary neural circuits (ONCs), defined as the model of biological neural circuits reparameterized for the control of alternative tasks. We first demonstrate that ONCs realize networks with higher maximum flow compared to arbitrary wired networks. We then learn instances of ONCs to control a series of robotic tasks, including the autonomous parking of a real-world rover robot. For reconfiguration of the purpose of the neural circuit, we adopt a search-based optimization algorithm. Ordinary neural circuits perform on par and, in some cases, significantly surpass the performance of contemporary deep learning models. ONC networks are compact, 77\% sparser than their counterpart neural controllers, and their neural dynamics are fully interpretable at the cell-level.

}, url = {http://proceedings.mlr.press/v119/hasani20a.html}, author = {Hasani, Ramin and Lechner, Mathias and Amini, Alexander and Rus, Daniela and Grosu, Radu}, editor = {Hal Daum{\'e} III and Aarti Singh} } @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} } @conference {, title = {Next-Generation Lagrangian Reachtubes}, booktitle = {Proceedings of CDC 2020, 59th IEEE Conference on Decision and Control}, year = {2020}, month = {12/2020}, author = {S. Gruenbacher and J. Cyranka and M. Lechner and Md. A. Islam and S. A. Smolka and R. Grosu} } @article {, title = {Single-variable delay-differential equation approximations of the Fitzhugh-Nagumo and Hodgkin-Huxley models}, journal = {Communications in Nonlinear Science and Numerical Simulation}, volume = {82}, year = {2020}, pages = {105066}, doi = {10.1016/j.cnsns.2019.105066}, url = {https://doi.org/10.1016/j.cnsns.2019.105066}, author = {Raffael Bechara Rameh and ELIZABETH M. CHERRY and Rodrigo Weber dos Santos} } @article {, title = {Swarm Model Checking on the GPU}, journal = {International Journal on Software Tools for Technology Transfer}, year = {2020}, author = {R. DeFrancisco and S. Cho and M. Ferdman and S. A. Smolka} } @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 = {Delay differential equation-based models of cardiac tissue: Efficient implementation and effects on spiral-wave dynamics}, journal = {Chaos: An Interdisciplinary Journal of Nonlinear Science}, volume = {29}, year = {2019}, pages = {123128}, doi = {10.1063/1.5128240}, url = {https://doi.org/10.1063/1.5128240}, author = {Johnny Moreira Gomes and Marcelo Lobosco and Rodrigo Weber dos Santos and ELIZABETH M. CHERRY} } @booklet {, title = {From Reactive Systems to Cyber-physical Systems: Essays Dedicated to Scott A. Smolka on the Occasion of His 65th Birthday}, year = {2019}, author = {Bartocci, Ezio and Cleaveland, Rance and Grosu, Radu and Sokolsky, Oleg} } @article {, title = {Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans}, journal = {Theoretical Computer Science}, volume = {765}, year = {2019}, pages = {158{\textendash}169}, author = {Islam, Md Ariful and Cleaveland, Rance and Fenton, Flavio H and Grosu, Radu and Jones, Paul L and Smolka, Scott A} } @conference {, title = {Automated Specification Extraction and Analysis with Specstractor}, booktitle = {Software Engineering and Formal Methods - 16th International Conference, {SEFM} 2018, Held as Part of {STAF} 2018, Toulouse, France, June 27-29, 2018, Proceedings}, year = {2018}, doi = {10.1007/978-3-319-92970-5\_3}, url = {https://doi.org/10.1007/978-3-319-92970-5\_3}, author = {Christoph Schulze and Rance Cleaveland and Mikael Lindvall} } @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.} } @article {, title = {Electromechanical vortex filaments during cardiac fibrillation}, journal = {Nature}, volume = {555}, year = {2018}, pages = {667+}, abstract = {

The self-organized dynamics of vortex-like rotating waves, which are also known as scroll waves, are the basis of the formation of complex spatiotemporal patterns in many excitable chemical and biological systems. In the heart, filament-like phase singularities5,6\ that are associated with three-dimensional scroll waves7\ are considered to be the organizing centres of life-threatening cardiac arrhythmias. The mechanisms that underlie the onset, maintenance and control14,15,16\ of electromechanical turbulence in the heart are inherently three-dimensional phenomena. However, it has not previously been possible to visualize the three-dimensional spatiotemporal dynamics of scroll waves inside cardiac tissues. Here we show that three-dimensional mechanical scroll waves and filament-like phase singularities can be observed deep inside the contracting heart wall using high-resolution four-dimensional ultrasound-based strain imaging. We found that mechanical phase singularities co-exist with electrical phase singularities during cardiac fibrillation. We investigated the dynamics of electrical and mechanical phase singularities by simultaneously measuring the membrane potential, intracellular calcium concentration and mechanical contractions of the heart. We show that cardiac fibrillation can be characterized using the three-dimensional spatiotemporal dynamics of mechanical phase singularities, which arise inside the fibrillating contracting ventricular wall. We demonstrate that electrical and mechanical phase singularities show complex interactions and we characterize their dynamics in terms of trajectories, topological charge and lifetime. We anticipate that our findings will provide novel perspectives for non-invasive diagnostic imaging and therapeutic applications.

}, doi = {https://doi.org/10.1038/nature26001}, author = {Jan Christoph and M. Chebbok and Carl Richter and Johannes Schr{\"o}der-Schetelig and Philip Bittihn and Seth Stein and Ilija Uzelac and FLAVIO H. FENTON and Gerd Hasenfuss and Robert F. Gilmour and Stefan Luther} } @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} } @conference {, title = {OpenUAV: A UAV Testbed for the CPS and Robotics Community}, booktitle = {Proceedings of the 9th ACM/IEEE International Conference on Cyber-Physical Systems}, year = {2018}, publisher = {IEEE Press}, organization = {IEEE Press}, address = {Piscataway, NJ, USA}, isbn = {978-1-5386-5301-2}, doi = {10.1109/ICCPS.2018.00021}, url = {https://doi.org/10.1109/ICCPS.2018.00021}, author = {Schmittle, Matt and Lukina, Anna and Vacek, Lukas and Das, Jnaneshwar and Buskirk, Christopher P. and Rees, Stephen and Sztipanovits, Janos and Grosu, Radu and Kumar, Vijay} } @article {, title = {An Optimization-Based Algorithm for the Construction of Cardiac Purkinje Network Models}, journal = {IEEE Transactions on Biomedical Engineering}, volume = {65}, year = {2018}, pages = {2760{\textendash}2768}, doi = {10.1109/tbme.2018.2815504}, url = {https://doi.org/10.1109/tbme.2018.2815504}, author = {Jesuliana N. Ulysses and Lucas A. Berg and ELIZABETH M. CHERRY and Ben R. Liu and Rodrigo W. dos Santos and Bruno G. de Barros and Bernardo M. Rocha and Rafael A. B. de Queiroz} } @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} } @article {, title = {Alternans promotion in cardiac electrophysiology models by delay differential equations}, journal = {Chaos: An Interdisciplinary Journal of Nonlinear Science}, volume = {27}, year = {2017}, pages = {093915}, abstract = {

Cardiac electrical alternans is a state of alternation between long and short action potentials and is frequently associated with harmful cardiac conditions. Different dynamic mechanisms can give rise to alternans; however, many cardiac models based on ordinary differential equations are not able to reproduce this phenomenon. A previous study showed that alternans can be induced by the introduction of delay differential equations (DDEs) in the formulations of the ion channel gating variables of a canine myocyte model. The present work demonstrates that this technique is not model-specific by successfully promoting alternans using DDEs for five cardiac electrophysiology models that describe different types of myocytes, with varying degrees of complexity. By analyzing results across the different models, we observe two potential requirements for alternans promotion via DDEs for ionic gates: (i) the gate must have a significant influence on the action potential duration and (ii) a delay must significantly impair the gate{\textquoteright}s recovery between consecutive action potentials.

}, issn = {1054-1500}, doi = {10.1063/1.4999471}, url = {http://aip.scitation.org/doi/10.1063/1.4999471}, author = {Gomes, Johnny M. and dos Santos, Rodrigo Weber and Cherry, Elizabeth M.} } @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} } @article {, title = {Improving Invariant Mining via Static Analysis}, journal = {ACM Trans. Embed. Comput. Syst.}, volume = {16}, year = {2017}, pages = {167:1{\textendash}167:20}, keywords = {automated test generation, Invariant mining, model-based development, verification and validation}, issn = {1539-9087}, doi = {10.1145/3126504}, url = {http://doi.acm.org/10.1145/3126504}, author = {Schulze, Christoph and Cleaveland, Rance} } @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} } @article {, title = {Simultaneous Quantification of Spatially Discordant Alternans in Voltage and Intracellular Calcium in Langendorff-Perfused Rabbit Hearts and Inconsistencies with Models of Cardiac Action Potentials and Ca Transients}, journal = {Frontiers in Physiology}, volume = {8}, year = {2017}, doi = {10.3389/fphys.2017.00819}, url = {https://doi.org/10.3389/fphys.2017.00819}, author = {Ilija Uzelac and Yanyan C. Ji and Daniel Hornung and Johannes Schr{\"o}der-Scheteling and Stefan Luther and Richard A. Gray and ELIZABETH M. CHERRY and FLAVIO H. FENTON} } @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} } @article {, title = {Computing Compositional Proofs of Input-to-Output Stability Using SOS Optimization and δ-Decidability}, journal = {Nonlinear Analysis: Hybrid Systems}, year = {2016}, month = {05/2016}, author = {A. Murthy and Md. A. Islam, and S. A. Smolka and R. Grosu} } @article {, title = {Estimability Analysis and Optimal Design in Dynamic Multi-scale Models of Cardiac Electrophysiology}, journal = {Journal of Agricultural, Biological, and Environmental Statistics}, year = {2016}, pages = {1{\textendash}16}, author = {Shotwell, Matthew S and Gray, Richard A} } @conference {, title = {Experience Report: Model-Based Test Automation of a Concurrent Flight Software Bus}, booktitle = {2016 IEEE 27th International Symposium on Software Reliability Engineering (ISSRE)}, year = {2016}, month = {Oct}, keywords = {aerospace computing, API, application program interfaces, Automation, Computer architecture, Concurrency, Concurrent computing, concurrent design, concurrent flight software bus, concurrent publisher-subscriber architecture style, concurrent system testing, Context, Flight Software, MBT technique, message passing, Microsoft Spec Explorer MBT tool, middleware, Model Based Testing, model-based test automation, NASA, NASA Core Flight Software software bus module, program testing, Publish-Subscribe, safety-critical software, safety-critical system, Software, software architecture, SUT, system-under-test, test case analysis, Testing}, doi = {10.1109/ISSRE.2016.47}, author = {D. Ganesan and M. Lindvall and S. Hafsteinsson and R. Cleaveland and S. L. Strege and W. Moleski} } @article {, title = {Abstract Model Repair}, journal = {Logical Methods in Computer Science}, volume = {3:11}, year = {2015}, author = {G. Chatzieleftheriou and B. Bonakdarpour and P. Katsaros and S. A. Smolka} } @article {, title = {Model-Order Reduction of Ion Channel Dynamics Using Approximate Bisimulation}, journal = {Theoretical Computer Science}, volume = {599C}, year = {2015}, month = {09/2015}, chapter = {34}, author = {Md. A. Islam and A. Murthy and E. Bartocci and E. M. Cherry and F. H. Fenton and J. Glimm and S. A. Smolka and R. Grosu} } @article {, title = {System design of stochastic models using robustness of temporal properties}, journal = {Theoretical Computer Science}, volume = {587}, year = {2015}, pages = {3 - 25}, abstract = {

Abstract Stochastic models such as Continuous-Time Markov Chains (CTMC) and Stochastic Hybrid Automata (SHA) are powerful formalisms to model and to reason about the dynamics of biological systems, due to their ability to capture the stochasticity inherent in biological processes. A classical question in formal modelling with clear relevance to biological modelling is the model checking problem, i.e. calculate the probability that a behaviour, expressed for instance in terms of a certain temporal logic formula, may occur in a given stochastic process. However, one may not only be interested in the notion of satisfiability, but also in the capacity of a system to maintain a particular emergent behaviour unaffected by the perturbations, caused e.g. from extrinsic noise, or by possible small changes in the model parameters. To address this issue, researchers from the verification community have recently proposed several notions of robustness for temporal logic providing suitable definitions of distance between a trajectory of a (deterministic) dynamical system and the boundaries of the set of trajectories satisfying the property of interest. The contributions of this paper are twofold. First, we extend the notion of robustness to stochastic systems, showing that this naturally leads to a distribution of robustness degrees. By discussing three examples, we show how to approximate the distribution of the robustness degree and the average robustness. Secondly, we show how to exploit this notion to address the system design problem, where the goal is to optimise some control parameters of a stochastic model in order to maximise robustness of the desired specifications.

}, keywords = {Temporal logic}, issn = {0304-3975}, doi = {http://dx.doi.org/10.1016/j.tcs.2015.02.046}, url = {http://www.sciencedirect.com/science/article/pii/S0304397515002224}, author = {Ezio Bartocci and Luca Bortolussi and Laura Nenzi and Guido Sanguinetti} }