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.
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.
| Original language | English |
|---|---|
| Book series | Lecture Notes in Computer Science |
| Volume | 4210 |
| Pages (from-to) | 1-16 |
| ISSN | 0302-9743 |
| DOIs | |
| Publication status | Published - 2006 |
| Externally published | Yes |
| Event | Conference on Computational Methods in Systems Biology - Trento, Italy Duration: 18 Oct 2006 → 19 Oct 2006 Conference number: 4 |
Conference
| Conference | Conference on Computational Methods in Systems Biology |
|---|---|
| Number | 4 |
| Country/Territory | Italy |
| City | Trento |
| Period | 18/10/2006 → 19/10/2006 |