由于多栈的模型图灵等价,因此,通用的异步通信程序模型的验证问题不可判定.为此,基于Petri网,提出了一个新的模型通信——通信Petri网,对异步通信程序进行刻画.通过对输入通信进行肛型限制以及对每个栈进行基于正则语言泵引理的抽象,通过将这样限制下的模型编码到数据Petri网,证明了限制下的新模型可覆盖性可判定.%Since multi-stack models are generally Turing-complete,verification problems on general models for asynchronous communication programs are undecidable.This paper proposes a new model based Petri net,named communication Petri nets (C-Petri nets) to model asynchronous communication programs.Applying the k-shaped restriction on the input communications and the abstraction on each stack based on popping lemma of regular languages,the coverability problem of the restricted C-Petri net is decidable by encoding the model to data Petri nets.
展开▼
