title: Analyzing resilience properties in oscillatory biological systems using parametric model checking.
abstract: Automated verification of living organism models allows us to gain previously unknown knowledge about underlying biological processes. In this paper we show how parametric time model checking can be applied to define the time behavior of biological oscillatory systems more precisely. In particular, we focus on the resilience properties of such systems. This notion was introduced to understand the behavior of biological systems (e.g. the mammalian circadian rhythm) that are reactive and adaptive enough to endorse major changes in their environment (e.g. jet-lags, day-night alternating work-time). We formalize these properties through parametric TCTL and investigate the influence of environmental conditions changes on the resilience of living organisms under the uncertainty in parameters. In particular, we discuss the influence of various perturbations, e.g. artificial jet-lag or components knock-out on the parameters controlling the oscillatory behavior. This analysis is crucial when it comes to model elicitation for dynamic biological systems. We demonstrate the applicability of this technique using a simplified model of circadian clock and discuss its results with regard to other previous studies based on hybrid modeling.
authors.affiliation: Saarland University, 66123 Saarbrucken, Germany. Electronic address: alexander.andreychenko@uni-saarland.de.
authors.forename: Alexander
authors.initials: A
authors.lastname: Andreychenko
authors.affiliation: École Centrale de Nantes, IRCCyN UMR CNRS 6597 (Institut de Recherche en Communications et Cybernétique de Nantes), Nantes, France; National Institute of Informatics, 2-1-2, Hitotsubashi, Chiyoda-ku, Tokyo 101-8430, Japan. Electronic address: morgan.magnin@irccyn.ec-nantes.fr.
authors.forename: Morgan
authors.initials: M
authors.lastname: Magnin
authors.affiliation: National Institute of Informatics, 2-1-2, Hitotsubashi, Chiyoda-ku, Tokyo 101-8430, Japan; Tokyo Institute of Technology, 2-12-1 Ookayama, Meguro-ku, Tokyo 152-8552, Japan. Electronic address: inoue@nii.ac.jp.
authors.forename: Katsumi
authors.initials: K
authors.lastname: Inoue
mesh_terms: D000818:Animals; D001683:Biological Clocks / Q000502:physiology; D002940:Circadian Rhythm / Q000502:physiology; D008954:Models, Biological
keywords: Biological oscillators; Model checking; Parametric model checking; Resilience