表达能力是评价一个计算模型的标准之一。本申请项目主要研究两类并发计算模型进程演算和Petri网之间的相对表达能力,具体包括以下三项内容(1) Place/Transition网与CCS;(2)带抑制弧的Petri网与pi演算;(3)着色Petri网与pi演算。基本方法是,根据模型M1和M2的语法和语义定义从M1到M2的编码,然后对该编码进行验证,如果该编码满足表达能力准则- - 操作一致性和完全抽象,则说明M2的表达能力至少不弱于M1;如果模型M1的表达能力不弱于M2且模型M2的表达能力也不弱于M1,那么两个模型表达能力是相同的;而如果从模型M1到模型M2和从模型M2到模型M1都不存在满足准则的编码,那么两个模型是不可比较的。在表达能力判断准则中,本项目选用了独立于模型的等价关系子互模拟,这也是本项目的特点之一。本项目的研究工作将有助于丰富并发理论研究成果,并进一步服务于实际应用。
Concurrency Model;Petri Net;Process calculus;Expressiveness;
并发计算模型是现代计算机科学基础研究课题之一。图灵机和lambda演算等是顺序系统的计算模型,但是这些模型无法正确描述具有并发性、交互性、分布性和行为不确定性等特点的并发系统,因此计算机科学研究者们致力于为并发系统建立相应的模型,其中Petri网和进程演算就是两类这样的模型。它们从不同角度反映了并发的本质,各具特点。随着实际应用的需要,研究者们提出了越来越多的并发模型。要想更好地发展和完善并发模型相关理论,则很有必要去研究,这些并发模型中哪些模型在本质上是有别于其他模型的,哪些模型可以通过表达关系而解决相关问题。本项目就是致力于研究一些并发模型之间的表达能力。我们主要在有界和无界P/T网到CCS的编码、真并发模型多元pi演算的 local cause 变体在交错框架下的刻画、缓存pi演算编码以及良结构下推系统的表达能力等方面取得了相关研究进展和成果。(1)我们给出了有界和无界P/T网到CCS的编码,证明了它们之间的表达能力相同。研究结果表明,在表达能力判断准则中,Fu和Lv在进程演算理论基础上提出的模型间的互模拟关系--子互模拟(subbisimilarity),适用于研究P/T网和CCS之间的表达能力问题。(2)我们研究了多元pi演算的 local cause 变体,其中Local cause 语义是进程演算中的一种真并发语义,可以在交错框架下完全抽象刻画。结果表明,多元pi演算的表达能力不会弱于带local cause的多元pi演算。同时带local cause多元pi演算的local cause互模拟关系的判定可规约为多元pi演算进程间的弱互模拟关系的判定。这也为Petri网的真并发语义和pi演算的交错式语义之间建立了更好的桥梁关系。(3)为了保证进程演算模型在异步通信时,能像着色Petri网那样保持数据的有序性,我们在pi演算中引入了带缓存(buffer)的通道,证明了在强互模拟关系下,缓存pi演算和多元pi演算(polyadic pi calculus)表达能力是一致的。为了验证缓存pi演算的表达能力,我们还给出了并发语言的缓存pi演算编码。(4)研究了良结构下推系统的表达能力,证明了分支向量加法系统、递归向量加法系统、一位零测试向量加法系统的表达能力都不超过良结构下推系统。我们的研究丰富了并发模型理论系统,給出了部分并发模型之间的表达关系。