Modal Logics for Brane Calculus

Giorgio Bacci, Marino Miculan

Research output: Contribution to journalConference article in JournalResearchpeer-review

12 Citations (Scopus)
86 Downloads (Pure)

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.
Original languageEnglish
Book seriesLecture Notes in Computer Science
Volume4210
Pages (from-to)1-16
ISSN0302-9743
DOIs
Publication statusPublished - 2006
Externally publishedYes
EventConference on Computational Methods in Systems Biology - Trento, Italy
Duration: 18 Oct 200619 Oct 2006
Conference number: 4

Conference

ConferenceConference on Computational Methods in Systems Biology
Number4
Country/TerritoryItaly
CityTrento
Period18/10/200619/10/2006

Fingerprint

Dive into the research topics of 'Modal Logics for Brane Calculus'. Together they form a unique fingerprint.

Cite this