|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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
LOTOS EXP |
| 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: http://cadp.inria.fr/publications/Mendes-Lang-et-al-13.html or from: http://bioinformatics.oxfordjournals.org/content/29/6/749 |
| Contact: | Prof. Claudine Chaouyia Instituto Gulbenkian de Ciência Rua da Quinta Grande 6 2780-156 Oeiras PORTUGAL Email: [email protected] |
| Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page