Abstract
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 language | English |
|---|---|
| Journal | Electronic Notes in Theoretical Computer Science |
| Volume | 192 |
| Issue number | 3 |
| Pages (from-to) | 23-37 |
| ISSN | 1571-0661 |
| DOIs | |
| Publication status | Published - 10 Nov 2008 |
| Externally published | Yes |
| Event | Workshop on Developments in Computational Models - Wroclaw, Poland Duration: 15 Jul 2007 → 15 Jul 2007 Conference number: 3 |
Workshop
| Workshop | Workshop on Developments in Computational Models |
|---|---|
| Number | 3 |
| Country/Territory | Poland |
| City | Wroclaw |
| Period | 15/07/2007 → 15/07/2007 |