@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} } @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 = {Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees}, booktitle = {Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics and 14th Workshop on Structural Operational Semantics, {EXPRESS/SOS} 2017, Berlin, Germany, 4th September 2017.}, year = {2017}, doi = {10.4204/EPTCS.255.3}, url = {https://doi.org/10.4204/EPTCS.255.3}, author = {James Ferlez and Rance Cleaveland and Steven I. Marcus} } @conference {, title = {Query Checking for Linear Temporal Logic}, year = {2017}, month = {25 August 2017}, publisher = {Springer, Cham}, organization = {Springer, Cham}, abstract = {

The query-checking problem for temporal logic may be formulated as follows. Given a Kripke structure\ M\ and a temporal-logic\ query\ of form\ ϕ[var]ϕ[var], which may be thought of as a temporal formula with a missing propositional subformula\ varvar, find the most precise propositional formula\ f\ that, when substituted for\ varvar\ in\ ϕ[var]ϕ[var], ensures\ M\ satisfies the resulting temporal property. Query checking has been used for system comprehension, specification reconstruction, and other related applications in the formal analysis of systems.

In this paper we present an automaton-based methodology for query checking over linear temporal logic (LTL). While this problem is known to be hard in the general case, we show that by exploiting several key observations about the interplay between the input model\ M\ and the query\ ϕ[var]ϕ[var], we can produce results for many problems of interest. In support of this claim, we report on preliminary experimental data for an implementation of our technique.

}, isbn = {978-3-319-67113-0}, doi = {https://doi.org/10.1007/978-3-319-67113-0_3}, url = {https://link.springer.com/chapter/10.1007/978-3-319-67113-0_3}, author = {Samuel Huang and Rance Cleaveland} } @conference {, title = {A framework for opacity in linear systems}, booktitle = {2016 American Control Conference, {ACC} 2016, Boston, MA, USA, July 6-8, 2016}, year = {2016}, doi = {10.1109/ACC.2016.7526666}, url = {https://doi.org/10.1109/ACC.2016.7526666}, author = {Bhaskar Ramasubramanian and Rance Cleaveland and Steven I. Marcus} } @conference {, title = {An Extensible Operational Semantics for {UML} Activity Diagrams}, booktitle = {Software Engineering and Formal Methods - 13th International Conference, {SEFM} 2015, York, UK, September 7-11, 2015. Proceedings}, year = {2015}, doi = {10.1007/978-3-319-22969-0\_25}, url = {https://doi.org/10.1007/978-3-319-22969-0\_25}, author = {Zamira Daw and Rance Cleaveland} }