Database of Case Studies Achieved Using CADP

Composition and Abstraction of Logical Regulatory Modules

Organisation: Instituto Gulbenkian de Ciência, Oeiras (PORTUGAL)
Inria Grenoble Rhône-Alpes and LIG, Grenoble (FRANCE)
IBISC, Université d'Evry Val d'Essonne, Evry (FRANCE)
Inria Paris Rocquencourt, Le Chesnay (FRANCE)
TAGC, INSERM U1090 AMU, Marseille (FRANCE)

Method: Logical Regulatory Modules

Tools used: GINsim
CADP (Construction and Analysis of Distributed Processes)

Domain: Bioinformatics

Period: 2013

Size: 26 million states

Description: Logical (Boolean or multi-valued) modelling is widely employed to study regulatory or signalling networks. Even though these discrete models constitute a coarse, yet useful, abstraction of reality, the analysis of large networks faces a classical combinatorial problem.

This case study proposes to take advantage of the intrinsic modularity of inter-cellular networks to set up a compositional procedure that enables a significant reduction of the dynamics, yet preserving the reachability of stable states. A novel compositional approach to support the logical modelling of interconnected cellular networks is developped. First, the concept of logical regulatory modules and their composition is formalised. Then, this framework is made operational by transposing the composition of logical modules into LOTOS and EXP. Importantly, the combination of incremental composition, abstraction, and minimisation using an appropriate equivalence relation (here the safety equivalence) yields huge reductions of the dynamics.

The potential of this approach is illustrated with two case-studies: the Segment-Polarity and the Delta-Notch modules.

Conclusions: This work relies on CADP for the composition, abstraction, and minimisation operations. The experiments show that huge reductions of the state space corresponding to a logical model can be obtained. In the case of the reduced Segment-Polarity model, the number of states of the dynamics is reduced by two orders of magnitude.

Minimisation modulo safety equivalence provides a good compromise between algorithmic complexity and compression of the state space. Most importantly, the safety equivalence preserves the reachability of stable states, a crucial property when studying differentiation processes. This property could be enriched to verify additional features along the trajectories leading to the states of interest, such as whether a given component is always required to change. To this aim, other verification techniques could prove efficient, such as on-the-fly verification of temporal logic properties.

Publications: [Mendes-Lang-et-al-13] Nuno Mendes, Frédéric Lang, Yves-Stan Le Cornec, Radu Mateescu, Grégory Batt, and Claudine Chaouiya. "Composition and abstraction of logical regulatory modules: application to multicellular systems". Bioinformatics 29(6):749-757, Oxford University Press, March 2013.

Available on-line from:
or from:

Prof. Claudine Chaouyia
Instituto Gulbenkian de Ciência
Rua da Quinta Grande 6
2780-156 Oeiras

Further remarks: This case study, amongst others, is described on the CADP Web site:

Last modified: Mon Sep 7 14:47:17 2015.

Back to the CADP case studies page