Transactions on Computational Systems Biology VII

This paper examines the influence of the Raf Kinase Inhibitor Protein (RKIP) on the Extracellular signal Regulated Kinase (ERK) signalling pathway [5] through modelling in a Markovian process algebra, PEPA [11]. Two models of the system are presented, a reagent-centric view and a pathway-centric view. The models capture functionality at the level of subpathway, rather than at a molecular level. Each model affords a different perspective of the pathway and analysis. We demonstrate the two models to be formally equivalent using the timing-aware bisimulation defined over PEPA models and discuss the biological significance.

We propose to model the dynamics of gene regulatory networks as concurrent processes in the stochastic pi calculus. As a first case study, we show how to express the control of transcription initiation at the lambda switch, a prototypical example where cooperative enhancement is crucial. This requires concurrent programming techniques that are new to systems biology, and necessitates stochastic parameters that we derive from the literature. We test all components of our model by exhaustive stochastic simulations. A comparison with previous results reported in the literature, experimental and simulation based, confirms the appropriateness of our modeling approach.

Logical modelling and Petri nets constitute two complementary approaches for the dynamical modelling of biological regulatory networks. Leaning on a translation of logical models into standard Petri nets, we propose a formalisation of the notion of circuit functionality in the Petri net framework. This approach is illustrated with the modelling and analysis of a molecular regulatory network involved in the control of Th-lymphocyte differentiation.

We introduce a graph-theoretic formalism suitable for modeling biochemical networks marked by combinatorial complexity, such as signal-transduction systems, in which protein-protein interactions play a prominent role. This development extends earlier work by allowing for explicit representation of the connectivity of a protein complex. Within the formalism, typed attributed graphs are used to represent proteins and their functional components, complexes, conformations, and states of post-translational covalent modification. Graph transformation rules are used to represent protein-protein interactions and their effects. Each rule defines a generalized reaction, i.e., a class of potential reactions that are logically consistent with knowledge or assumptions about the represented biomolecular interaction. A model is specified by defining 1) molecular-entity graphs, which delimit the molecular entities and material components of a system and their possible states, 2) graph transformation rules, and 3) a seed set of graphs representing chemical species, such as the initial species present before introduction of a signal. A reaction network is generated iteratively through application of the graph transformation rules. The rules are first applied to the seed graphs and then to any and all new graphs that subsequently arise as a result of graph transformation. This procedure continues until no new graphs are generated or a specified termination condition is satisfied. The formalism supports the generation of a list of reactions in a system, which can be used to derive different types of physicochemical models, which can be simulated and analyzed in different ways. The processes of generating and simulating the network may be combined so that species are generated only as needed.

In this paper, we use some observations on the nature of biochemical reactions to derive interesting properties of qualitative biochemical Kripke structures. We show that these characteristics make Kripke structures of biochemical pathways suitable for assumption based distributed model checking. The number of chemical species participating in a biochemical reaction is usually bounded by a small constant. This observation is used to show that the Hamming distance between adjacent states of a qualitative biochemical Kripke structures is bounded. We call such structures as Bounded Hamming Distance Kripke structures (BHDKS). We, then, argue the suitability of assumption based distributed model checking for BHDKS by constructively deriving worst case upper bounds on the size of the fragments of the state space that need to be stored at each distributed node. We also show that the distributed state space can be mapped naturally to a hypercube based distributed architecture. We support our results by experimental evaluation over benchmarks and biochemical pathways from public databases.

This paper presents a graphical representation for the stochastic π-calculus, which is formalised by defining a corresponding graphical calculus. The graphical calculus is shown to be reduction equivalent to stochastic π, ensuring that the two calculi have the same expressive power. The graphical representation is used to model a couple of example biological systems, namely a bistable gene network and a mapk signalling cascade. One of the benefits of the representation is its ability to highlight the existence of cycles, which are a key feature of biological systems. Another benefit is its ability to animate interactions between system components, in order to visualise system dynamics. The graphical representation can also be used as a front end to a simulator for the stochastic π-calculus, to help make modelling and simulation of biological systems more accessible to non computer scientists.

We study rules proposed by the biologist R. Thomas relating the structure of a concurrent system of interacting genes (represented by a signed directed graph called a regulatory graph) with its dynamical properties. We prove that the results in [10] are stable under projection, and this enables us to relax the assumptions under which they are valid. More precisely, we relate here the presence of a positive (resp. negative) circuit in a regulatory graph to a more general form of biological differentiation (resp. of homeostasis).

When modelling complex biological systems it is often desirable to combine a number of distinct sub-models to form a larger composite model. We describe an XML based language that can be used to specify composite models and a lightweight computational framework that executes these models. The language supports specification of structure and implementation details for composite models, along with the interfaces provided by each sub-model. The framework executes each sub-model in its native environment, allowing extensive reuse of existing models. It uses mathematical and computational connectors and translators to unify the models computationally. Unlike other suggested approaches for model integration, our approach does not impose one modeling scheme, composition algorithm or underlying middleware framework. We demonstrate our approach by constructing a composite model describing part of the glucose homeostasis system.