Abstract
The Brane Calculus is a calculus of mobile processes, intended to model the transport machinery of a cell system. In this paper, we introduce the Brane Logic, a modal logic for expressing formally properties about systems in Brane Calculus. Similarly to previous logics for mobile ambients, Brane Logic has specific spatial and temporal modalities. Moreover, since in Brane Calculus the activity resides on membrane surfaces and not inside membranes, we need to add a specific logic (akin Hennessy-Milner’s) for reasoning about membrane activity.
We present also a proof system for deriving valid sequents in Brane Logic. Finally, we present a model checker for a decidable fragment of this logic.
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
Preview
Unable to display preview. Download preview PDF.
References
Alberts, B., Bray, D., Lewis, J., Raff, M., Roberts, K., Watson, J.D.: Molecular biology of the cell, 2nd edn., Garland (1989)
Caires, L.: Behavioral and spatial observations in a logic for the pi-calculus. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 72–89. Springer, Heidelberg (2004)
Cardelli, L.: Brane calculi. In: Danos, V., Schachter, V. (eds.) CMSB 2004. LNCS (LNBI), vol. 3082, pp. 257–278. Springer, Heidelberg (2005)
Cardelli, L.: Abstract machines of systems biology. T. Comp. Sys. Biology 3737, 145–168 (2005)
Cardelli, L., Gordon, A.D.: Anytime, anywhere: Modal logics for mobile ambients. In: Proc. POPL, pp. 365–377 (2000)
Charatonik, W., Dal-Zilio, S., Gordon, A.D., Mukhopadhyay, S., Talbot, J.-M.: Model checking mobile ambients. Theor. Comput. Sci. 308(1-3), 277–331 (2003)
Danos, V., Pradalier, S.: Projective brane calculus. In: Danos, V., Schachter, V. (eds.) CMSB 2004. LNCS (LNBI), vol. 3082, pp. 134–148. Springer, Heidelberg (2005)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)
Hughes, G.E., Cresswell, M.J.: A companion to Modal Logic. Methuen, London (1984)
Mardare, R., Priami, C.: A decidable extension of hennessy-milner logic with spatial operators. Technical Report DIT-06-009, Dipartimento di Informatica e Telecomunicazioni, University of Trento (2006)
Miculan, M., Bacci, G.: Modal logics for brane calculus. Technical Report UDMI/08/2006/RR, Dept. of Mathematics and Computer Science, Univ. of Udine (2006), http://www.dimi.uniud.it/miculan/Papers/UDMI082006.pdf
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Regev, A., Silverman, W., Shapiro, E.Y.: Representation and simulation of biochemical processes using the pi-calculus process algebra. In: Pacific Symposium on Biocomputing, pp. 459–470 (2001)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society Press, Los Alamitos (2002)
Sangiorgi, D.: Extensionality and intensionality of the ambient logics. In: Proc. POPL, pp. 4–13 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miculan, M., Bacci, G. (2006). Modal Logics for Brane Calculus. In: Priami, C. (eds) Computational Methods in Systems Biology. CMSB 2006. Lecture Notes in Computer Science(), vol 4210. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11885191_1
Download citation
DOI: https://doi.org/10.1007/11885191_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-46166-1
Online ISBN: 978-3-540-46167-8
eBook Packages: Computer ScienceComputer Science (R0)