کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
426575 686112 2012 20 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Multiset rewriting for the verification of depth-bounded processes with name binding
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Multiset rewriting for the verification of depth-bounded processes with name binding
چکیده انگلیسی

We combine two of the existing approaches to the study of concurrency by means of multiset rewriting: multiset rewriting with existential quantification (MSR) and constrained multiset rewriting. We obtain ν-MSR, where we rewrite multisets of atomic formulae, in which terms can only be pure names, where some names can be restricted. We consider the subclass of depth-bounded ν-MSR, for which the interdependence of names is bounded. We prove that they are strictly Well Structured Transition Systems, so that coverability, termination and boundedness are all decidable for depth-bounded ν-MSR. This allows us to obtain new verification results for several formalisms with name binding that can be encoded within ν-MSR, namely polyadic ν-PN (Petri nets with tuples of names as tokens), the π-calculus, MSR or Mobile Ambients.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 215, June 2012, Pages 68–87
نویسندگان
, ,