Abstract
The sodium-potassium exchange pump is a transmembrane transport protein that establishes and maintains the appropriate internal concentrations of sodium and potassium ions in cells. This exchange is an important physiological process; it is critical in maintaining the osmotic balance of the cell. Inspired by the functioning of this pump, we introduce and study a threshold-based type system in a bio-inspired formalism. Such a system can avoid errors in the definition of the formal model used to model certain biologic processes. For this type system we prove a subject reduction theorem.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Aman, B., Ciobanu, G.: Typed membrane systems. In: Păun, G., Pérez-Jiménez, M.J., Riscos-Núñez, A., Rozenberg, G., Salomaa, A. (eds.) WMC 2009. LNCS, vol. 5957, pp. 169–181. Springer, Heidelberg (2010)
Aman, B., Dezani-Ciancaglini, M., Troina, A.: Type disciplines for analysing biologically relevant properties. Electron. Notes Theor. Comput. Sci. 227, 97–111 (2009)
Besozzi, D., Ciobanu, G.: A P system description of the sodium-potassium pump. In: Mauri, G., Păun, G., Jesús Pérez-Jímenez, M., Rozenberg, G., Salomaa, A. (eds.) WMC 2004. LNCS, vol. 3365, pp. 210–223. Springer, Heidelberg (2005)
Bioglio, L.: Enumerated type semantics for the calculus of looping sequences. RAIRO - Theor. Inform. Appl. 45, 35–58 (2011)
Bioglio, L., Dezani-Ciancaglini, M., Giannini, P., Troina, A.: Typed stochastic semantics for the calculus of looping sequences. Theoret. Comput. Sci. 431, 165–180 (2012)
Ciobanu, G.: Software verification of the biomolecular systems. In: Modelling in Molecular Biology, Natural Computing Series, pp. 40–59. Springer, Heidelberg (2004)
Ciobanu, G., Ciubotariu, V., Tanasă, B.: A Pi-Calculus model of the Na/K pump. Genome Inf. 13, 469–472 (2002). Universal Academy Press
Guyton, A., Hall, J.: Textbook of Medical Physiology, 12th edn. Elsevier (2010)
Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types, In: Proceedings POPL, pp. 273–284. ACM Press, New York (2008)
Kennedy, B.G., Lunn, G., Hoffman, J.F.: Effects of altering the ATP/ADP ratio on pump-mediated Na/K and Na/Na exchanges in resealed human red blood cell ghosts. J. Gen. Physiol. 87, 47–72 (1986)
Lingrel, J.B., Kuntzweiler, T.: Na\(^+\), K\(^+\)-ATPase. J. Biol. Chem. 269, 19659–19662 (1994)
Zs.-Nagy, I., Lustyik, G., Zs.-Nagy, V., Zarandi, B., Bertoni-Freddari, C.: Intracellular N+/K+ ratios in human cancer cells as revealed by energy dispersive X-ray microanalysis. J. Cell Biol. 90, 769–777 (1981)
Păun, G., Rozenberg, G., Salomaa, G. (eds.): Handbook of Membrane Computing. Oxford University Press, Oxford (2010)
Salomaa, A.: Formal Languages. Academic Press, Edinburgh (1973)
Acknowledgements
Many thanks to the reviewers for their useful comments. The work was supported by a grant of the Romanian National Authority for Scientific Research, project number PN-II-ID-PCE-2011-3-0919.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Aman, B., Ciobanu, G. (2014). Behavioural Types Inspired by Cellular Thresholds. In: Counsell, S., Núñez, M. (eds) Software Engineering and Formal Methods. SEFM 2013. Lecture Notes in Computer Science(), vol 8368. Springer, Cham. https://doi.org/10.1007/978-3-319-05032-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-05032-4_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-05031-7
Online ISBN: 978-3-319-05032-4
eBook Packages: Computer ScienceComputer Science (R0)