Probabilistic Model Checking related to computational biology

    I collect some research papers for the analysis of computational biology by model checking technique.

Case Studies related to Biology

1. FGF signalling pathway

This model uses CTMC model to represent the biochemical reactions. The two main molecules are reprsented by two separate modules. Transitions in two modules labelled with the same action occur simulataneously. For example, module FGF involves the reactions related to FGF. The action [bind] which also occurs in module FGFR refers to the binding of FGF and FGFR. see PRISM model here.


Instead of modeling each inidivual component, an alternative is to model the number of each type of molecule. see alternative Population-based PRISM model.

Reference: link

2. Find Control Strategies in Boolean model

In this case, it aims to find a control sequence that can lead the initial state to the goal state. We assume that u is the control input (external input). It can be assigned to any nodes in Boolean network. Boolean model:


* The first paper discusses model checking approach for seeking control sequences in Boolean networks publish in 2009. I refer you to that paper Symbolic Approaches for Finding Control Strategies in Boolean Networks. The model checker tool they used is NuSMV. Since any BN can be seen as a special case of PBN, I do not rewrite that case using PRISM.

Reference: link
3. Infer Gene Regulatory network

This paper applied PRISM to infer gene regulatory relationships from time-series data. Consider the activation relationship: A& causes a direct increment of C. The terms “Node_state, Init, Up” is used to represent the state of nodes.

For that relationship, the PCTL property is as follows: P=?[(A_state<=Init U A_state=Up) U (A_state=Up & (F(G C_state=Up)))]. That describes the probability that whenever the gene A is Up and the gene C eventually is Up and then it remains Up. Another property has been introduced as well: P=?[A_state=Init U (G A_state=Up)] That decribes the probability that gene A will reach and then remain Up after its initial state.

* However, only two kinds of relationships are investigated, i.e. activation and inhibition. And they only considered the gene regulatory relationships between individual genes. But the investigation of multiple activators or inbihitors co-regulating the target gene is more reasonable in GRN.

Reference: link

4. Model checking Gene regulatory networks

The gene regulatory network space is defined as a tuple T in this paper. It introduced the special gene, the threshold functions and the weight functions to regulate activation and repression. Threshold parameters assigned to genes specify the strength necessary to sustain the gene's activety. Weight parameters assigned to edges denote the strength of their direccted effect. Its aim is to synthesize the space of parameters which characterize GRNs that satisfy a given property. The bistability property can be written as the following LTL formula: (Y¬Z→G(Y∧¬Z))∧(Z¬Y→ Z¬Y ).

Reference: link

5. Symbolic model checking of biochemical networks

I found two papers proposing several CTL queries in systems biology. Obviously, the use of CTL describes biological process. For example, CTL can be used to answer the following queries:
5.1 The Mammalian Cell Cycle Control, some queries list as below:
    a. Is there a pathway for synthesizing a protein P? ---  EF(P)
    b. Can the cell reach a state s while passing by another state s2? EF(s2 ∧ EFs)
    c. Is state s2 a necessary checkpoint for reaching state s? ---  ¬E((¬s2) U s)
5.2 Regulation of Gene Expression, some queries list as below:
    a. Which states may produce a concentration for x greater than some value t? ---  EF(x>t)

How long does it take for a molecule to become activated? * This problem proposed doesn't specify by CTL in that paper. However, it can be easily sorted by PCTL. PRISM offers Costs and Rewards to compute “expected time”.
* For a simple example: R{"time"}=?[F(state="activated")] can be used to encode 'the expected time taken before reaching activated stated’.

Reference: link1 link2

6.An overview in 2012

Section 5.3 introduces three works employing PRISM model checker. The first two works discuss how PRISM models the signaling pathway using CTMCs. The second work actually is the 1st case study shown in the page. And the first work is very similar with the second work.
* I would like to mark 'Process Algebra Operators’ here which are both used in their work. From official PRISM manual: M1 || M2 : alphabetised parallel composition of modules M1 and M2 (synchronising on only actions appearing in both M1 and M2) M1 ||| M2 : asynchronous parallel composition of M1 and M2 (fully interleaved, no synchronisation)

Reference: link

7. Probabilistic Model Checking of Complex Biological Pathways

Reference: link