Schivo - Modelling biological pathway dynamics with Timed Automata

Stefano Schivo, Jetse Scholma, BrendWanders, Ricardo A. Urquidi Camacho, Paul E. van der Vet, Marcel Karperien,
Rom Langerak, Jaco van de Pol, and Janine N. Post

IEEE Journal of Biomedical and Health Informatics - 2013


Living cells are constantly subjected to a plethora of
environmental stimuli that require integration into an appropriate
cellular response. This integration takes place through signal
transduction events that form tightly interconnected networks.The
understanding of these networks requires capturing their dynamics
through computational support and models. ANIMO (analysis
of Networks with Interactive Modeling) is a tool that enables the
construction and exploration of executable models of biological
networks, helping to derive hypotheses and to plan wet-lab experiments.
The tool is based on the formalism of Timed Automata,
which can be analyzed via the UPPAAL model checker. Thanks
to Timed Automata, we can provide a formal semantics for the
domain-specific language used to represent signaling networks.
This enforces precision and uniformity in the definition of signaling
pathways, contributing to the integration of isolated signaling
events into complex network models. We propose an approach to
discretization of reaction kinetics that allows us to efficiently use
UPPAAL as the computational engine to explore the dynamic behavior
of the network of interest. A user-friendly interface hides
the use of Timed Automata fromthe user, while keeping the expressive
power intact. Abstraction to single-parameter kinetics speeds
up construction of models that remain faithful enough to provide
meaningful insight. The resulting dynamic behavior of the network
components is displayed graphically, allowing for an intuitive and
interactive modeling experience.