Abstract
Model checking has proven to be a useful analysis technique not only for concurrent systems, but also for the genetic regulatory networks (Grns) that govern the functioning of living cells. The applications of model checking in systems biology have revealed that temporal logics should be able to capture both branching-time and fairness properties. At the same time, they should have a user-friendly syntax easy to employ by non-experts. In this paper, we define Ctrl (Computation Tree Regular Logic), an extension of Ctl with regular expressions and fairness operators that attempts to match these criteria. Ctrlsubsumes both Ctl and Ltl, and has a reduced set of temporal operators indexed by regular expressions, inspired from the modalities of Pdl (Propositional Dynamic Logic). We also develop a translation of Ctrl into HmlR (Hennessy-Milner Logic with Recursion), an equational variant of the modal μ-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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Fisher, J., Henzinger, T.A.: Executable cell biology. Nature Biotechnology 25(11), 1239–1250 (2007)
Regev, A., Shapiro, E.: Cells as computation. Nature 419(6905), 343 (2002)
de Jong, H.: Modeling and simulation of genetic regulatory systems: A literature review. J. of Computational Biology 9(1), 67–103 (2002)
Antoniotti, M., Policriti, A., Ugel, N., Mishra, B.: Model building and model checking for biochemical processes. Cell Biochemistry and Biophysics 38(3), 271–286 (2003)
Barnat, J., Brim, L., Cerná, I., Drazan, S., Safranek, D.: Parallel model checking large-scale genetic regulatory networks with DiVinE. In: FBTC 2007. ENTCS, vol. 194 (2008)
Batt, G., Ropers, D., de Jong, H., Geiselmann, J., Mateescu, R., Page, M., Schneider, D.: Validation of qualitative models of genetic regulatory networks by model checking: Analysis of the nutritional stress response in Escherichia coli. Bioinformatics 21 (Suppl. 1), i19–i28 (2005)
Bernot, G., Comet, J.-P., Richard, A., Guespin, J.: Application of formal methods to biological regulatory networks: Extending Thomas’ asynchronous logical approach with temporal logic. J. of Theoretical Biology 229(3), 339–348 (2004)
Calder, M., Vyshemirsky, V., Gilbert, D., Orton, R.: Analysis of signalling pathways using the PRISM model checker. In: CMSB 2005, pp. 79–90 (2005)
Chabrier-Rivier, N., Chiaverini, M., Danos, V., Fages, F., Schächter, V.: Modeling and querying biomolecular interaction networks. TCS 325(1), 25–44 (2004)
Fisher, J., Piterman, N., Hajnal, A., Henzinger, T.A.: Predictive modeling of signaling crosstalk during C. elegans vulval development. PLoS Computational Biology 3(5), e92 (2007)
Batt, G., Bergamini, D., de Jong, H., Gavarel, H., Mateescu, R.: Model checking genetic regulatory networks using GNA and CADP. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 158–163. Springer, Heidelberg (2004)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. STTT 2(4), 410–425 (2000)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007)
Thomas, R., Thieffry, D., Kaufman, M.: Dynamical behaviour of biological regulatory networks: I. Biological role of feedback loops and practical use of the concept of the loop-characteristic state. Bulletin of Mathematical Biology 57(2), 247–276 (1995)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Specification, vol. I. Springer, Heidelberg (1992)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Emerson, E.A., Halpern, J.Y.: Sometimes and not never revisited: On branching versus linear time. In: POPL 1983, pp. 127–140 (January 1983)
Kozen, D.: Results on the propositional μ-calculus. TCS 27, 333–354 (1983)
Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 184–194. Springer, Heidelberg (1998)
Brázdil, T., Cerná, I.: Model checking of RegCTL. Computers and Artificial Intelligence 25(1) (2006)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. JCSS 18(2), 194–211 (1979)
Streett, R.: Propositional dynamic logic of looping and converse. Information and Control (1982)
Larsen, K.G.: Proof systems for Hennessy-Milner logic with recursion. In: Dauchet, M., Nivat, M. (eds.) CAAP 1988. LNCS, vol. 299, pp. 215–230. Springer, Heidelberg (1988)
Mateescu, R.: CÆSAR_SOLVE: A generic library for on-the-fly resolution of alternation-free boolean equation systems. STTT 8(1), 37–56 (2006)
Mateescu, R., Monteiro, P.T., Dumas, E., Mateescu, R.: Computation tree regular logic for genetic regulatory networks. Research Report RR-6521, INRIA (2008)
Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 363–367. Springer, Heidelberg (2001)
Holzmann, G.: The SPIN Model Checker – Primer and Reference Manual. Addison-Wesley, Reading (2003)
Wolper, P.: A translation from full branching time temporal logic to one letter propositional dynamic logic with looping (published manuscript, 1982)
Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. SCP 46(3), 255–281 (2003)
Brzozowski, J.A.: Derivatives of regular expressions. JACM 11(4), 481–494 (1964)
Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading (1986)
Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. FMSD 2(2), 121–147 (1993)
Andersen, H.R.: Model checking and boolean graphs. TCS 126(1), 3–30 (1994)
Vergauwen, B., Lewi, J.: Efficient local correctness checking for single and alternating boolean equation systems. In: Shamir, E., Abiteboul, S. (eds.) ICALP 1994. LNCS, vol. 820, pp. 304–315. Springer, Heidelberg (1994)
Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Maibaum, T.S.E. (eds.) FM 2008. LNCS, vol. 5014, pp. 148–164. Springer, Heidelberg (2008)
Arts, T., Earle, C.B., Derrick, J.: Development of a verified Erlang program for resource locking. STTT 5(2–3), 205–220 (2004)
Garavel, H.: OPEN/CÆSAR: An open software architecture for verification, simulation, and testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68–84. Springer, Heidelberg (1998)
Garavel, H., Lang, F., Mateescu, R.: Compiler construction using LOTOS NT. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 9–13. Springer, Heidelberg (2002)
Glass, L., Kauffman, S.A.: The logical analysis of continuous non-linear biochemical control networks. J. of Theoretical Biology 39(1), 103–129 (1973)
Batt, G., de Jong, H., Page, M., Geiselmann, J.: Symbolic reachability analysis of genetic regulatory networks using discrete abstractions. Automatica 44(4), 982–989 (2008)
de Jong, H., Gouzé, J.-L., Hernandez, C., Page, M., Sari, T., Geiselmann, J.: Qualitative simulation of genetic regulatory networks using piecewise-linear models. Bulletin of Mathematical Biology 66(2), 301–340 (2004)
Ropers, D., de Jong, H., Page, M., Schneider, D., Geiselmann, J.: Qualitative simulation of the carbon starvation response in Escherichia coli. Biosystems 84(2), 124–152 (2006)
Joubert, C., Mateescu, R.: Distributed local resolution of boolean equation systems. In: PDP 2005. IEEE Computer Society, Los Alamitos (2005)
Joubert, C., Mateescu, R.: Distributed on-the-fly model checking and test case generation. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 126–145. Springer, Heidelberg (2006)
Monteiro, P.T., Ropers, D., Mateescu, R., Freitas, A.T., de Jong, H.: Temporal logic patterns for querying dynamic models of cellular interaction networks. Bioinformatics (in press, 2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mateescu, R., Monteiro, P.T., Dumas, E., de Jong, H. (2008). Computation Tree Regular Logic for Genetic Regulatory Networks. In: Cha, S.(., Choi, JY., Kim, M., Lee, I., Viswanathan, M. (eds) Automated Technology for Verification and Analysis. ATVA 2008. Lecture Notes in Computer Science, vol 5311. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88387-6_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-88387-6_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88386-9
Online ISBN: 978-3-540-88387-6
eBook Packages: Computer ScienceComputer Science (R0)