Undecidability of Model checking in Brane Logic

Giorgio Bacci, Marino Miculan

Research output: Contribution to journalConference article in JournalResearchpeer-review

88 Downloads (Pure)


The Brane Calculus is a calculus intended to model the structure and the dynamics of biological membranes. In order to express properties of systems in this calculus, in previous work we have introduced a temporal-spatial logic called Brane Logic. A natural question of great practical importance is if model checking of this logic is decidable, that is, if it is possible to check automatically whether a given system satisfies a given formula. We have already shown that model checking is decidable for replication-free systems and guarantee-free formulas. In this paper, we show that admitting replication in systems, or any guarantee constructor in formulas (and quantifiers), leads model checking to be undecidable. Moreover, we give also a correspondence result between membranes and systems, showing that any system can be obtained by a canonical one where all information are contained on a membrane enclosing an empty compartment.
Original languageEnglish
JournalElectronic Notes in Theoretical Computer Science
Issue number3
Pages (from-to)23-37
Publication statusPublished - 10 Nov 2008
Externally publishedYes
EventWorkshop on Developments in Computational Models - Wroclaw, Poland
Duration: 15 Jul 200715 Jul 2007
Conference number: 3


WorkshopWorkshop on Developments in Computational Models


Dive into the research topics of 'Undecidability of Model checking in Brane Logic'. Together they form a unique fingerprint.

Cite this