论文部分内容阅读
随着计算机网络和多核处理器的出现,并行系统被广泛应用于生产实践中。作为描述并行系统的形式化模型,Petri网和Pi演算(π-演算)得以迅速发展,并在各自领域内建立起了强大的理论基础。 Petri网和Pi演算之间最大的区别在于,前者是基于图形化表示的,而后者是基于文本描述的。由于具备直观的图形化表示和严格的数学分析理论,Petri网可以用于对离散事件动态系统建模。然而,Petri网的结构是固定的,很难对结构易变的松耦合系统进行建模。相反,Pi演算的输入连接是能够随时改变的,可将通道名沿通道传递出去,这样就能够轻松实现对以并行计算为代表的松耦合系统的建模。然而,Pi演算缺少用于同步的原语,难以实现并行进程间多个交互的同步。 由于Petri网和Pi演算具有各自的特点,人们希望能够将一种模型转换为另一种模型,从而将这两种模型的优点结合起来。这样,在一种模型中难以解决的问题,就可以转换到另一个模型中进行研究。实际上,从Petri网到Pi演算的转换为我们使用Pi演算的验证技巧来证明Petri网的性质提供了可能。需要指出的是,一种模型转换为另一种模型必须保证该转换满足两种模型间模拟的要求。 此外,研究形式化模型间的行为模拟有助于研究模型的表达能力。在Web服务组合的研究领域中,Petri网和Pi演算都可以作为研究的形式化模型,但哪种模型更为合适则广受争议,这就需要研究两种模型的表达能力。如果Pi演算可以模拟Petri网的所有行为,就可以认定Pi演算至少和Petri网具有相同的表达能力。 Pi演算模拟Petri网的相关研究已经取得了一些重要的研究成果,但有一个尚未回答的问题是Pi演算能否模拟所有的一般Petri网系统。本文则重点研究了Pi演算模拟库所容量受限的一般Petri网系统。 本文在现有研究成果的基础上,提出了Pi演算模拟Petri网的严格定义,并在定义中使用标号迁移系统来描述Pi演算和Petri网的行为。 通过引入同步机制,本文定义了用于模拟库所容量受限Petri网系统的状态表达式,并提出了从库所容量受限Petri网系统到状态表达式的转换。本文为每一个库所定义了一系列带状态的库所进程,为每一个变迁定义了一系列带状态的变迁进程。每一个库所连同其中的托肯转换为一个带状态的库所进程。每一个变迁连同其输入库所和输出库所中托肯的分布信息转换为一个带状态的变迁进程。每一个变迁发生都用一个归约序列来表示。为了防止归约序列发生死锁,本文设计了一个同步器进程。最后将这些库所进程、变迁进程和同步器进程用并行算子连接起来就构成了状态表达式。 本文从理论上证明了所提出的转换满足Pi演算模拟Petri网的定义,并从实践上验证了转换方法的正确性和可行性。研究结果表明,Pi演算可以模拟库所容量受限的Petri网系统。