Modelling and Analysis of Biochemical Signalling Pathway Cross-talk

TL;DR

This paper presents a formal modeling approach for biochemical signalling pathway cross-talk, enabling the detection and analysis of different cross-talk types using model checking techniques.

Contribution

It introduces a modular modeling framework based on PRISM, defining five cross-talk types and demonstrating their analysis through CSL properties.

Findings

Different cross-talk types can be distinguished using CSL model checking.

The approach effectively models complex pathway interactions like TGF-b/BMP, WNT, and MAPK.

Modular models facilitate understanding of pathway cross-talk mechanisms.

Abstract

Signalling pathways are abstractions that help life scientists structure the coordination of cellular activity. Cross-talk between pathways accounts for many of the complex behaviours exhibited by signalling pathways and is often critical in producing the correct signal-response relationship. Formal models of signalling pathways and cross-talk in particular can aid understanding and drive experimentation. We define an approach to modelling based on the concept that a pathway is the (synchronising) parallel composition of instances of generic modules (with internal and external labels). Pathways are then composed by (synchronising) parallel composition and renaming; different types of cross-talk result from different combinations of synchronisation and renaming. We define a number of generic modules in PRISM and five types of cross-talk: signal flow, substrate availability, receptor function, gene expression and intracellular communication. We show that Continuous Stochastic Logic properties can both detect and distinguish the types of cross-talk. The approach is illustrated with small examples and an analysis of the cross-talk between the TGF-b/BMP, WNT and MAPK pathways.