کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
422305 | 685065 | 2008 | 15 صفحه PDF | دانلود رایگان |

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 - Volume 192, Issue 3, 10 November 2008, Pages 23-37