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.
