The κ-Lattice: Decidability Boundaries for Qualitative Analysis in Biological Languages

  • Giorgio Delzanno
  • Cinzia Di Giusto
  • Maurizio Gabbrielli
  • Cosimo Laneve
  • Gianluigi Zavattaro
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5688)


The κ-calculus is a formalism for modelling molecular biology where molecules are terms with internal state and sites, bonds are represented by shared names labelling sites, and reactions are represented by rewriting rules. Depending on the shape of the rewriting rules, a lattice of dialects of κ can be obtained. We analyze the expressive power of some of these dialects by focusing on the thin boundary between decidability and undecidability for problems like reachability and coverability.


Decidability Boundary Graph Transformation Graph Grammar Proper Solution Reachability Analysis 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Whitesides, G., Mathias, J., Seto, C.: Molecular self-assembly and nanochemistry – a chemical strategy for the synthesis of nanostructures. Science 254, 1312–1319 (1991)CrossRefPubMedGoogle Scholar
  2. 2.
    Panyutin, I., Hsieh, P.: The kinetics of spontaneous DNA branch migration. Proc. National Academy of Science USA 91(6), 2021–2025 (1994)CrossRefGoogle Scholar
  3. 3.
    Mao, C., Sun, W., Seeman, N.: Assembly of Borromean rings from DNA. Nature 386(6621), 137–138 (1997)CrossRefPubMedGoogle Scholar
  4. 4.
    Watson, J., Crick, F.: A Structure for Deoxyribose Nucleic Acid. Nature 171, 737–738 (1953)CrossRefPubMedGoogle Scholar
  5. 5.
    Credi, A., Garavelli, M., Laneve, C., Pradalier, S., Silvi, S., Zavattaro, G.: Modelizations and simulations of nano devices in nanok calculus. In: Calder, M., Gilmore, S. (eds.) CMSB 2007. LNCS (LNBI), vol. 4695, pp. 168–183. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  6. 6.
    Yin, P., Harry, M., Choi, M., Colby, R., Calvert, R., Pierce, N.: Programming biomolecular self-assembly pathways. Nature 451, 318–322 (2008)CrossRefPubMedGoogle Scholar
  7. 7.
    Dill, D.L., Knapp, M., Gage, P., Talcott, C.L., Laderoute, K., Lincoln, P.: The pathalyzer: A tool for analysis of signal transduction pathways. In: Eskin, E., Ideker, T., Raphael, B., Workman, C. (eds.) RECOMB 2005. LNCS (LNBI), vol. 4023, pp. 11–22. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 8.
    Fages, F.: Symbolic model-checking for biochemical systems. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol. 2916, pp. 102–102. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Peleg, M., Yeh, I., Altman, R.B.: Modelling biological processes using workflow and petri net models. Bioinformatics 18(6), 825–837 (2002)CrossRefPubMedGoogle Scholar
  10. 10.
    Danos, V., Feret, J., Fontana, W., Krivine, J.: Abstract interpretation of cellular signalling networks. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 83–97. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  11. 11.
    Minsky, M.: Computation: finite and infinite machines. Prentice-Hall, Englewood Cliffs (1967)Google Scholar
  12. 12.
    Danos, V., Laneve, C.: Formal molecular biology. TCS 325(1), 69–110 (2004)CrossRefGoogle Scholar
  13. 13.
    Esparza, J., Nielsen, M.: Decidability Issues for Petri Nets-a Survey. Bulletin of the European Association for TCS 52, 245–262 (1994)Google Scholar
  14. 14.
    Reisig, W.: Petri nets: an introduction. Springer, Heidelberg (1985)CrossRefGoogle Scholar
  15. 15.
    Fages, F., Soliman, S.: Formal cell biology in biocham. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 54–80. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  16. 16.
    Fages, F., Sollman, S., Chabrier-Rivier, N.: Modelling and querying interaction networks in the biochemical abstract machine biocham. Journal of Biological Physics and Chemistry 4, 64–73 (2004)CrossRefGoogle Scholar
  17. 17.
    Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Meseguer, J., Sönmez, M.K.: Pathway logic: Symbolic analysis of biological signaling. In: Pacific Symposium on Biocomputing, pp. 400–412 (2002)Google Scholar
  18. 18.
    Talcott, C.L.: Pathway logic. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 21–53. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  19. 19.
    Heiner, M., Gilbert, D., Donaldson, R.: Petri nets for systems and synthetic biology. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 215–264. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  20. 20.
    Blinov, M.L., Yang, J., Faeder, J.R., Hlavacek, W.S.: Graph theory for rule-based modeling of biochemical networks. In: Priami, C., Ingólfsdóttir, A., Mishra, B., Riis Nielson, H. (eds.) Transactions on Computational Systems Biology VII. LNCS (LNBI), vol. 4230, pp. 89–106. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  21. 21.
    Mayr, R., Rusinowitch, M.: Reachability is decidable for ground ac rewrite systems. In: Infinity 1998, pp. 53–64 (1998)Google Scholar
  22. 22.
    Mayr, R.: Process rewrite systems. Inf. Comput. 156(1-2), 264–286 (2000)CrossRefGoogle Scholar
  23. 23.
    Coquidé, J.L., Dauchet, M., Gilleron, R., Vágvölgyi, S.: Bottom-up tree pushdown automata and rewrite systems. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 287–298. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  24. 24.
    Dauchet, M., Tison, S.: The theory of ground rewrite systems is decidable. In: LICS, pp. 242–248 (1990)Google Scholar
  25. 25.
    Jacquemard, F.: Decidable approximations of term rewriting systems. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 362–376. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  26. 26.
    Salomaa, K.: Deterministic tree pushdown automata and monadic tree rewriting systems. J. Comput. Syst. Sci. 37(3), 367–394 (1988)CrossRefGoogle Scholar
  27. 27.
    Busi, N., Zavattaro, G.: Reachability analysis in boxed ambients. In: Coppo, M., Lodi, E., Pinna, G.M. (eds.) ICTCS 2005. LNCS, vol. 3701, pp. 143–159. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  28. 28.
    Boneva, I., Talbot, J.M.: When ambients cannot be opened. Theor. Comput. Sci. 333(1-2), 127–169 (2005)CrossRefGoogle Scholar
  29. 29.
    Busi, N., Zavattaro, G.: Deciding reachability in mobile ambients. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 248–262. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  30. 30.
    Delzanno, G., Montagna, R.: On reachability and spatial reachability in fragments of bioambients. Electr. Notes Theor. Comput. Sci. 171(2), 69–79 (2007)CrossRefGoogle Scholar
  31. 31.
    Zavattaro, G.: Reachability analysis in bioambients. ENTCS 227, 179–193 (2009)Google Scholar
  32. 32.
    Drewes, F., Kreowski, H.J., Habel, A.: Hyperedge replacement, graph grammars. In: Handbook of Graph Grammars, pp. 95–162. World Scientific, Singapore (1997)Google Scholar
  33. 33.
    Joshi, S., König, B.: Applying the graph minor theorem to the verification of graph transformation systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 214–226. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  34. 34.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! TCS 256(1-2), 63–92 (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Giorgio Delzanno
    • 1
  • Cinzia Di Giusto
    • 2
  • Maurizio Gabbrielli
    • 2
  • Cosimo Laneve
    • 2
  • Gianluigi Zavattaro
    • 2
  1. 1.Dipartimento di Informatica e Scienze dell’InformazioneUniversità di GenovaItalia
  2. 2.Dipartimento di Scienze dell’InformazioneUniversità di BolognaItalia

Personalised recommendations