CTRL: Extension of CTL with Regular Expressions and Fairness Operators to Verify Genetic Regulatory Networks

Radu Mateescu 1, * Pedro T. Monteiro 2, 3 Estelle Dumas 2 Hidde De Jong 2
* Auteur correspondant
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
2 IBIS - Modeling, simulation, measurement, and control of bacterial regulatory networks
LAPM - Laboratoire Adaptation et pathogénie des micro-organismes [Grenoble], Inria Grenoble - Rhône-Alpes, Institut Jean Roget
Abstract : Model checking has proven to be a useful analysis technique not only for concurrent systems, but also for genetic regulatory networks (GRNs). Applications of model checking in systems biology have revealed that temporal logics should be able to capture both branching-time and fairness properties (needed for specifying multistability and oscillation properties, respectively). At the same time, they should have a user-friendly syntax easy to employ by non-experts. In this paper, we define Computation Tree Regular Logic (CTRL), an extension of CTL with regular expressions and fairness operators that attempts to match these criteria. CTRL subsumes both CTL and LTL, and has a reduced set of temporal operators indexed by regular expressions. We also develop a translation of CTRL into Hennessy-Milner Logic with Recursion (HMLR), an equational variant of the modal mu-calculus. This has allowed us to obtain an on-the-fly model checker with diagnostic for CTRL by directly reusing the verification technology available in the CADP toolbox. We illustrate the application of the CTRL model checker by analyzing the GRN controlling the carbon starvation response of Escherichia coli.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2011, Foundations of Formal Reconstruction of Biochemical Networks, 412 (26), pp.2854-2883. 〈http://www.sciencedirect.com/science/article/pii/S0304397510002902〉. 〈10.1016/j.tcs.2010.05.009〉
Liste complète des métadonnées

Littérature citée [83 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00610831
Contributeur : Radu Mateescu <>
Soumis le : lundi 25 juillet 2011 - 10:07:51
Dernière modification le : jeudi 17 mai 2018 - 12:52:03
Document(s) archivé(s) le : mercredi 26 octobre 2011 - 02:20:49

Fichier

Mateescu-Monteiro-Dumas-deJong...
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Radu Mateescu, Pedro T. Monteiro, Estelle Dumas, Hidde De Jong. CTRL: Extension of CTL with Regular Expressions and Fairness Operators to Verify Genetic Regulatory Networks. Theoretical Computer Science, Elsevier, 2011, Foundations of Formal Reconstruction of Biochemical Networks, 412 (26), pp.2854-2883. 〈http://www.sciencedirect.com/science/article/pii/S0304397510002902〉. 〈10.1016/j.tcs.2010.05.009〉. 〈inria-00610831〉

Partager

Métriques

Consultations de la notice

505

Téléchargements de fichiers

468