2011 IEEE International Conference on Bioinformatics and Biomedicine (2011)
Atlanta, Georgia USA
Nov. 12, 2011 to Nov. 15, 2011
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/BIBM.2011.124
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 Ren´e 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).
Model Checking, Biological Regulatory Networks, Linear Temporal Logic, Kinetic Logic
J. Ahmad, U. Siddique, U. Niazi and U. Rauf, "Formal Modeling and Analysis of Biological Regulatory Networks Using SPIN," 2011 IEEE International Conference on Bioinformatics and Biomedicine(BIBM), Atlanta, Georgia USA, 2011, pp. 304-308.