@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}
}
@conference {,
	title = {Data assimilation for cardiac electrical dynamics},
	booktitle = {Proceedings of the 5th {International} {Conference} on {Computational} and {Mathematical} {Biomedical} {Engineering}},
	year = {2017},
	address = {Pittsburgh, PA},
	abstract = {<p>New insights into the mechanisms underlying cardiac arrhythmias may be possible from a greater understanding of variables unobserved in experimental settings. When experimental observations are sparse, data assimilation can be effective at recovering a more complete system state estimate. We have recently shown using synthetic observations of one- and three-dimensional cardiac tissue that data assimilation can be used to recover state variables observed sparsely in space and time or unobserved. Here we extend these findings to show that data assimilation remains effective in reconstructing cardiac states with underlying system spatial heterogeneity and in the presence of significant model error.</p>
},
	author = {Cherry, E. M. and Cairns, D. I. and Holt, N. and LaVigne, N. S. and Fenton, F. H. and Hoffman, M. J.},
	editor = {Nithiarasu, P. and Robertson, A. M.}
}
@article {,
	title = {System design of stochastic models using robustness of temporal properties},
	journal = {Theoretical Computer Science},
	volume = {587},
	year = {2015},
	pages = {3 - 25},
	abstract = {<p>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.</p>
},
	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}
}
