Modeling of Resilience Properties in Oscillatory Biological Systems using Parametric Time Petri Nets, Supplementary Information

TL;DR

This paper presents a method using parametric time Petri nets to analyze and verify the resilience of biological oscillatory systems, such as circadian rhythms, under environmental perturbations.

Contribution

It introduces a formal approach to model and analyze resilience properties in biological oscillatory systems using parametric time Petri nets and TCTL.

Findings

Effective modeling of resilience in biological clocks

Analysis of perturbations like jet-lag and knock-outs

Application to a simplified circadian clock model

Abstract

Automated verification of living organism models allows us to gain previously unknown knowledge about underlying biological processes. In this paper, we show the benefits to use parametric time Petri nets in order to analyze precisely the dynamic behavior of biological oscillatory systems. In particular, we focus on the resilience properties of such systems. This notion is crucial 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 demonstrate how changes of the environmental conditions can be tackled to guarantee the resilience of living organisms. In particular, we are able to discuss the influence of various perturbations, e.g. artificial jet-lag or components knock-out, with regard to quantitative delays. 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.