Formal analysis of oscillatory behaviors in biological regulatory networks: An alternative approach

In the realm of system biology, the study of regulatory networks leads biologists to the development of increasingly large, detailed and complex models. These complex models, replicating the dynamics of cell processes, are then analyzed using different approaches to obtain predictions. Genetic oscillations play a main role in the activity of signal transduction by maintaining the cascade of internal biochemical reactions with the extracellular environment. Molecular alterations in the performance of such behavioral rhythms can lead to severe pathological problems, e.g. cancer. Different formal approaches have been proposed to analyze Biological Regulatory Networks (BRNs) Such approaches mainly involve the use of non-functional and Binary Decision Diagrams (BDDs) based model checkers for the analysis of irregular structured BRNs, and dense time concept for the modeling of BRNs. Computational Tree Logic (CTL) based analysis of BRNs is not suitable for identifying cyclic (oscillatory) behaviors in irregular structures and the use of Linear Temporal Logic (LTL) for the analysis of multistability is not viable. Morover, the reachability problem becomes undecidable in case of dense time modeling. In order to address these issues, we use delays and Minsky machines to observe the oscillatory behavior and to overcome the limitation of LTL for the analysis of multistable states. To demonstrate our approach, we consider two different case studies: Pseudomonas aeruginosa and P53-Mdm2 feedback loop.