Modeling biological pathway dynamics with timed automata

Introduction Better insight into biological pathways is essential for understanding how cells function. We want to contribute to the study of pathways by enabling a molecular biologist to play with different settings in order to simulate a pathway, to detect missing or incorrect information, and to identify informative wet-lab experiments. The objective of our work is to provide a framework for modeling pathways using the formal support offered by Timed Automata [1]. A longer-term objective is be to be able to understand a pathway through its model via in-silico experiments: any hypotheses on the actual working of the pathway could then be tested via in-vivo experiments. The current work concentrates on kinase pathways. Methods A single timed automaton template is used to represent the concept of phosphorylation: each specific kinase interaction is an instance of this template. Kinase activation levels are represented by variables, which are updated as the corresponding reactions occur. All these details are hidden to the user, who interacts only with the graphical interface defining the topology of the pathway network and the parameters that govern the reactions. These parameters are input to approximated versions of the general equation for Michaelis-Menten kinetics. According to the user-selected approximation scenario, one to three parameters are available for the user to set. The idea is that the user plays with these parameters to obtain the desired pathway dynamics. Results A Timed Automata model can be subjected to model checking [2], which allows us to test the accuracy of models. Other interesting properties can also be verified, and thus increase the understanding of the modeled entities. The simplest way in which model checking can be used is to obtain a graph that plots kinase activation levels against time. The current state of the modeling effort allows us to obtain a behavior closely resembling empirical observations. Conclusions & Future Work Thanks to the modeling framework which is currently being developed, a user can define and test a model for a biological pathway without having to know the computational mechanisms at work under the hood. The next step in the development of the framework is the enrichment of the interface with more accessible functionalities, such as complex property checking. Moreover, the implementation of a feature for the automatic computation of parameters which let the model match given experimental data is felt to be a useful and important extension. References [1] J. Bengtsson and W. Yi. Timed automata: Semantics, algorithms and tools. In Jrg Desel, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Lectures on Concurrency and Petri Nets, volume 3098 of Lecture Notes in Computer Science, pages 87-124. Springer Berlin / Heidelberg, 2004. [2] E. Clarke, O. Grumberg, and D. Peled. Model checking. MIT Press, 1999.