Formal Modeling and Analysis of Biological Regulatory Networks Using SPIN

In the last two decades, formal verification has emerged as an important technique for the formal modeling and analysis of real time reactive and unpredictable systems. The main advantage of model checking over simulation based analysis is its inherent soundness and reliability of computed results. In this paper, we propose to use explicit state model checker (SPIN) for formal modeling and Linear Temporal Logic (LTL) for the exploration of the complex dynamics (cycles) of biological regulatory networks (BRNs). The main contribution of this paper also includes the generalized framework for modeling BRNs based on well known Kinetic Logic of Rene Thomas and state-of-the-art SPIN model checker. To demonstrate the usefulness of current work, we utilized it for the analysis of mucus production system in Pseudomonas aeruginosa and BRN involving Indoleamine 2, 3-dioxygenase (IDO).