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.

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 accepted in Mathematical Structures in Computer Science journal.
Please refer to the preprint version.

Feel free to discuss this article using the comments below.

@article{PMR12-MSCS,
  author = {Paulev\'{e}, {L}o{\"i}c. and Magnin, Morgan and Roux, Olivier},
  title = {Static Analysis of Biological Regulatory Networks Dynamics using Abstract Interpretation},
  journal = {Mathematical Structures in Computer Science},
  year = {2012},
  volume = {in press}
}

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.

Feel free to discuss this article using the comments below.

@ARTICLE{PMR10-SASB,
  author = {{P}aulev{\'e}, {L}o{\"i}c and {M}agnin, {M}organ and {R}oux, {O}livier},
  title = {{A}bstract {I}nterpretation of {D}ynamics of {B}iological {R}egulatory
	{N}etworks},
  journal = {Electronic Notes in Theoretical Computer Science},
  year = {2011},
  volume = {272},
  pages = {43-56},
  note = {Proceedings of {T}he {F}irst {I}nternational {W}orkshop on {S}tatic
	{A}nalysis and {S}ystems {B}iology ({SASB} 2010)},
  doi = {10.1016/j.entcs.2011.04.004}
}

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.

@Incollection{PMR10-TCSB,
  author = {{P}aulev{\'e}, {L}o{\"i}c and {M}agnin, {M}organ and {R}oux, {O}livier},
  title = {Refining Dynamics of Gene Regulatory Networks in a Stochastic $\pi$-Calculus
	Framework},
  booktitle = {Transactions on Computational Systems Biology XIII},
  publisher = {Springer Berlin / Heidelberg},
  year = {2011},
  editor = {Priami, Corrado and Back, Ralph-Johan and Petre, Ion and de Vink,
	Erik},
  volume = {6575},
  series = {Lecture Notes in Computer Science},
  pages = {171-191},
  affiliation = {IRCCyN, UMR CNRS 6597, École Centrale de Nantes, France},
  doi = {10.1007/978-3-642-19748-2_8}
}

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.