Multiset rewriting for the verification of depth-bounded processes with name binding

详细信息	查看全文 | 推荐本文 |

• 作者：Fernando Rosa-Velardo ; ^{fernandorosa@sip.ucm.es} ; Marí ; a Martos-Salgado ; ^{mrmartos@estumail.ucm.es}
• 关键词：Multiset rewriting ; Depth-boundedness ; WSTS ; Verification ; Decidability ; Petri nets ; Process algebra
• 刊名：Information and Computation
• 出版年：2012
• 期刊代码：132_08905401
• 类别：cp
• 出版时间：June, 2012
• 卷：215
• 期：Complete
• 页码：68-87
• 文件大小：442 K

摘要

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.