Modeling biological pathway dynamics with timed automata

Stefano Schivo, Jetse Scholma, B. Wanders, Janine Nicole Post, Hermanus Bernardus Johannes Karperien, P.E. van der Vet, Romanus Langerak, Jaco van de Pol

Research output: Contribution to conferencePosterAcademic

Abstract

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.
Original languageEnglish
Pages--
Publication statusPublished - 2011
Externally publishedYes
EventEMBO|EMBL Symposium on Structure and Dynamics of Protein Networks 2011 - EMBL Advanced Training Centre, Heidelberg, Germany
Duration: 13 Oct 201116 Oct 2011
https://www.embo-embl-symposia.org/symposia/2011/EES11-03/index.html

Symposium

SymposiumEMBO|EMBL Symposium on Structure and Dynamics of Protein Networks 2011
CountryGermany
CityHeidelberg
Period13/10/1116/10/11
Internet address

Fingerprint

Model checking
Phosphorylation
Petri nets
Experiments
Chemical activation
Semantics
Topology

Keywords

  • METIS-283534

Cite this

Schivo, S., Scholma, J., Wanders, B., Post, J. N., Karperien, H. B. J., van der Vet, P. E., ... van de Pol, J. (2011). Modeling biological pathway dynamics with timed automata. --. Poster session presented at EMBO|EMBL Symposium on Structure and Dynamics of Protein Networks 2011, Heidelberg, Germany.
Schivo, Stefano ; Scholma, Jetse ; Wanders, B. ; Post, Janine Nicole ; Karperien, Hermanus Bernardus Johannes ; van der Vet, P.E. ; Langerak, Romanus ; van de Pol, Jaco. / Modeling biological pathway dynamics with timed automata. Poster session presented at EMBO|EMBL Symposium on Structure and Dynamics of Protein Networks 2011, Heidelberg, Germany.
@conference{1d39d24106bb48ac85da0b030a9d769c,
title = "Modeling biological pathway dynamics with timed automata",
abstract = "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.",
keywords = "METIS-283534",
author = "Stefano Schivo and Jetse Scholma and B. Wanders and Post, {Janine Nicole} and Karperien, {Hermanus Bernardus Johannes} and {van der Vet}, P.E. and Romanus Langerak and {van de Pol}, Jaco",
year = "2011",
language = "English",
pages = "----",
note = "EMBO|EMBL Symposium on Structure and Dynamics of Protein Networks 2011 ; Conference date: 13-10-2011 Through 16-10-2011",
url = "https://www.embo-embl-symposia.org/symposia/2011/EES11-03/index.html",

}

Schivo, S, Scholma, J, Wanders, B, Post, JN, Karperien, HBJ, van der Vet, PE, Langerak, R & van de Pol, J 2011, 'Modeling biological pathway dynamics with timed automata' EMBO|EMBL Symposium on Structure and Dynamics of Protein Networks 2011, Heidelberg, Germany, 13/10/11 - 16/10/11, pp. --.

Modeling biological pathway dynamics with timed automata. / Schivo, Stefano; Scholma, Jetse; Wanders, B.; Post, Janine Nicole; Karperien, Hermanus Bernardus Johannes; van der Vet, P.E.; Langerak, Romanus; van de Pol, Jaco.

2011. -- Poster session presented at EMBO|EMBL Symposium on Structure and Dynamics of Protein Networks 2011, Heidelberg, Germany.

Research output: Contribution to conferencePosterAcademic

TY - CONF

T1 - Modeling biological pathway dynamics with timed automata

AU - Schivo, Stefano

AU - Scholma, Jetse

AU - Wanders, B.

AU - Post, Janine Nicole

AU - Karperien, Hermanus Bernardus Johannes

AU - van der Vet, P.E.

AU - Langerak, Romanus

AU - van de Pol, Jaco

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

KW - METIS-283534

M3 - Poster

SP - --

ER -

Schivo S, Scholma J, Wanders B, Post JN, Karperien HBJ, van der Vet PE et al. Modeling biological pathway dynamics with timed automata. 2011. Poster session presented at EMBO|EMBL Symposium on Structure and Dynamics of Protein Networks 2011, Heidelberg, Germany.