Analyzing resilience properties in oscillatory biological systems using parametric model checking

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.