An extension of the qualitative simulation method is currently being explored by G. Batt (INRIA Rhône-Alpes) in his thesis research. The aim is to develop a method for the validation of models of genetic regulatory networks, by comparing the predicted qualitative behaviors with experimentally-measured expression profiles. The validation of a model is complicated by the size of the state transition graph obtained through qualitative simulation, which for networks with more than a dozen genes becomes too big to analyze by hand. The validation method is based on existing, highly-efficient model-checking techniques developed for the verification of discrete transition systems. The validation of models of genetic regulatory networks is at the heart of a collaboration with Radu Mateescu (INRIA Rhône-Alpes). The collaboration has resulted in a new prototype version of GNA that is coupled to two well-known state-of-the-art model checkers, NuSMV and CADP.
G. Batt, D. Ropers, H. de Jong, J. Geiselmann, R. Mateescu, M. Page, D. Schneider (2005), Validation of qualitative models of genetic regulatory networks by model checking: Analysis of the nutritional stress response in Escherichia coli, Bioinformatics. To appear.
E.M. Clarke, O. Grumberg, D.A. Peled (1999), Model Checking, MIT Press, Boston, MA.