کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
422305 685065 2008 15 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Undecidability of Model Checking in Brane Logic
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Undecidability of Model Checking in Brane Logic
چکیده انگلیسی

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.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 192, Issue 3, 10 November 2008, Pages 23-37