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.
|Journal||Electronic Notes in Theoretical Computer Science|
|Publication status||Published - 10 Nov 2008|
|Event||Workshop on Developments in Computational Models - Wroclaw, Poland|
Duration: 15 Jul 2007 → 15 Jul 2007
Conference number: 3
|Workshop||Workshop on Developments in Computational Models|
|Period||15/07/2007 → 15/07/2007|