Skip to main content

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

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNBI,volume 5688))

Abstract

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.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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)

    Article  CAS  PubMed  Google Scholar 

  2. Panyutin, I., Hsieh, P.: The kinetics of spontaneous DNA branch migration. Proc. National Academy of Science USA 91(6), 2021–2025 (1994)

    Article  CAS  Google Scholar 

  3. Mao, C., Sun, W., Seeman, N.: Assembly of Borromean rings from DNA. Nature 386(6621), 137–138 (1997)

    Article  CAS  PubMed  Google Scholar 

  4. Watson, J., Crick, F.: A Structure for Deoxyribose Nucleic Acid. Nature 171, 737–738 (1953)

    Article  CAS  PubMed  Google Scholar 

  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)

    Chapter  Google Scholar 

  6. Yin, P., Harry, M., Choi, M., Colby, R., Calvert, R., Pierce, N.: Programming biomolecular self-assembly pathways. Nature 451, 318–322 (2008)

    Article  CAS  PubMed  Google Scholar 

  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)

    Chapter  Google Scholar 

  8. Fages, F.: Symbolic model-checking for biochemical systems. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol. 2916, pp. 102–102. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  9. Peleg, M., Yeh, I., Altman, R.B.: Modelling biological processes using workflow and petri net models. Bioinformatics 18(6), 825–837 (2002)

    Article  CAS  PubMed  Google Scholar 

  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)

    Chapter  Google Scholar 

  11. Minsky, M.: Computation: finite and infinite machines. Prentice-Hall, Englewood Cliffs (1967)

    Google Scholar 

  12. Danos, V., Laneve, C.: Formal molecular biology. TCS 325(1), 69–110 (2004)

    Article  Google Scholar 

  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. Reisig, W.: Petri nets: an introduction. Springer, Heidelberg (1985)

    Book  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  CAS  Google Scholar 

  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. Talcott, C.L.: Pathway logic. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 21–53. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  21. Mayr, R., Rusinowitch, M.: Reachability is decidable for ground ac rewrite systems. In: Infinity 1998, pp. 53–64 (1998)

    Google Scholar 

  22. Mayr, R.: Process rewrite systems. Inf. Comput. 156(1-2), 264–286 (2000)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  24. Dauchet, M., Tison, S.: The theory of ground rewrite systems is decidable. In: LICS, pp. 242–248 (1990)

    Google Scholar 

  25. Jacquemard, F.: Decidable approximations of term rewriting systems. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 362–376. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  26. Salomaa, K.: Deterministic tree pushdown automata and monadic tree rewriting systems. J. Comput. Syst. Sci. 37(3), 367–394 (1988)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  28. Boneva, I., Talbot, J.M.: When ambients cannot be opened. Theor. Comput. Sci. 333(1-2), 127–169 (2005)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  30. Delzanno, G., Montagna, R.: On reachability and spatial reachability in fragments of bioambients. Electr. Notes Theor. Comput. Sci. 171(2), 69–79 (2007)

    Article  Google Scholar 

  31. Zavattaro, G.: Reachability analysis in bioambients. ENTCS 227, 179–193 (2009)

    Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  34. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! TCS 256(1-2), 63–92 (2001)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Delzanno, G., Di Giusto, C., Gabbrielli, M., Laneve, C., Zavattaro, G. (2009). The κ-Lattice: Decidability Boundaries for Qualitative Analysis in Biological Languages. In: Degano, P., Gorrieri, R. (eds) Computational Methods in Systems Biology. CMSB 2009. Lecture Notes in Computer Science(), vol 5688. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03845-7_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-03845-7_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-03844-0

  • Online ISBN: 978-3-642-03845-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics