Introduction

The Process Hitting is a recently introduced framework for concurrent modelling. It aims at being simple and at allowing very efficient formal checking.

Systems biology is the main application field of the Process Hitting, with  notably the modelling of Biological Regulatory Networks (BRNs).  Recent work addresses the formal checking of BRNs relating more than 100 components.

The main features of the Process Hitting are:

• Sorts (components) regroup a finite set of processes;
• at any time one and only one process of each sort is present;
• actions are of the form “process a_k hits process b_i to make it bounce to process b_j” where a and b are sorts.
• Efficient stable states (or fix points) listing.
• Efficient reachability analysis.
• Temporal and stochastic parameters for actions.

Pint (Process Hitting related tools) gathers various programs manipulating Process Hitting models (stochastic simulation, model checking, stable state listing, export/import of various formats, etc.).

Main bibliographic references are listed by posts in the “Papers” category.

“Concretizing the Process Hitting into Biological Regulatory Networks” (M. Folschette, L. Paulevé, K. Inoue, M. Magnin, O. Roux)

The Process Hitting (PH) is a recently introduced framework to model concurrent processes. Its major originality lies in a specific restriction on the causality of actions, which makes the formal analysis of very large systems tractable. PH is suitable to model Biological Regulatory Networks (BRNs) with complete or partial knowledge of cooperations between regulators by defining the most permissive dynamics with respect to these constraints.

On the other hand, the qualitative modeling of BRNs has been widely addressed using René Thomas’ formalism, leading to numerous theoretical work and practical tools to understand emerging behaviors.
Given a PH model of a BRN, we first tackle the inference of the underlying Interaction Graph between components. Then the inference of corresponding Thomas’ models is provided using Answer Set Programming, which allows notably an efficient enumeration of (possibly numerous) compatible parametrizations.

In addition to giving a formal link between different approaches for qualitative BRNs modeling, this work emphasizes the ability of PH to deal with large BRNs with incomplete knowledge on cooperations, where Thomas’ approach fails because of the combinatorics of parameters.

Article presented at CMSB’12

Full text available on Springer.

L. Paulevé, M. Magnin and O. Roux, “Static analysis of biological regulatory networks dynamics using abstract interpretation” in Mathematical Structures in Computer Science

The analysis of dynamics of Biological Regulatory Networks (BRNs) requires innovative
methods to cope with the state space explosion. This paper settles an original approach
for deciding reachability properties based on the Process Hitting, a framework suitable to
model dynamical complex systems. In particular, the Process Hitting has been shown of
interest to provide compact models of dynamics of BRNs with discrete values. The
Process Hitting splits a finite number of processes into so-called sorts and describes the
way each process is able to act upon (i.e. to ”hit”) an other one (or itself) in order to
”bounce” it as another process of the same sort further acting.

By using complementary abstract interpretations of the succession of actions in Process
Hitting, we build a very efficient static analysis to over- and under-approximate
reachability properties, which avoids building the underlying states graph. The analysis
is proven to have a low theoretical complexity, in particular when the number of
processes per sorts is limited while a very large number of sorts can be managed.

This makes such an approach very promising for the scalable analysis of abstract
complex systems. We illustrate this through the analysis of a large BRN of 94
components. Our method replies quasi-instantaneously to reachability questions while
standard model-checking techniques regularly fail because of the combinatoric explosion
of behaviours.

Article published in Mathematical Structures in Computer Science journal.
Read online.

L. Paulevé, M. Magnin and O. Roux, “Abstract Interpretation of Dynamics of Biological Regulatory Networks” at SASB 2010

This paper introduces very efficient formal checking of process reachability within Process Hittings, by using abstract interpretation and static analysis techniques.
It has been presented at the first international workshop on Systems Biology and Static Analysis (SASB), in September 2010 in Perpignan, France.

Please refer to the edited version; and to the slides of the talk.

L. Paulevé, M. Magnin and O. Roux, “Refining Dynamics of Gene Regulatory Networks in a Stochastic π-Calculus Framework” in TCSB

The paper introducing the Process Hitting framework for modelling biological regulatory networks has been accepted for publication in the journal Transactions on Computational Systems Biology. We thank the reviewers for their very helpful comments and suggestions that allowed to improve the paper a lot.

Please refer to the edited version.

Feel free to discuss this article using the comments below.

Pint sources under CeCILL licence

Pint sources are now available under the CeCILL licence at http://code.google.com/p/pint/.

For more information on the CeCILL licence, please visit CeCILL information page.