【作者】 宋磊；

【导师】 傅育熙；

【作者基本信息】 上海交通大学 ， 计算机软件与理论， 2009， 硕士

【摘要】 随着计算机技术和网络通信技术的高速发展,以并发性、分布性、实时性、异构性和互操作性等主要特征的并发分布式系统已成为计算机技术的主流方向。并发现象以其固有的复杂性,对计算机科学家提出了挑战。与顺序计算不同,我们对并行与并发计算实质的认识尚处于初级阶段。进程代数主要是用来描述并发计算的数学模型,它研究并发现象,即多个计算主体(进程)同时活动,通过交换信息(通讯)进行协作,以共同完成预期任务的特定计算现象。对于一个进程演算,通常需要研究其语法语义,而公理化系统便是理解其操作语义的一个很好的方法。近年来,在解决并发系统问题的算法构造过程中,随机方法被证明是一种重要的工具。相对确定算法而言,随机算法可以更加有效,因为它们通常有着更加简单的结构,使用更少的内存,并且可以得到一些确定算法不能得到的好结果。传统上,对并发系统进行建模的进程演算中,并不涉及定量分析,因此对于一个并发系统会以多大的概率发生某个动作这样的问题就无法提供有用的信息。但是从应用的角度来看,进行这样的定量分析非常必要,因为在本质上并发系统的许多方面是与随机相关的,或至少可以建模成随机行为。因此,在传统的模型中加入随机因素可以使我们更加有效来分析并发系统。在本文中,首先介绍一种概率进程演算,称为πsp。πsp是π演算的一个概率扩展,在π演算的基础上加入概率选择符,同时支持概率选择和不确定选择。接着,分别介绍强概率符号互模拟、弱概率符号互模拟以及概率符号同余的定义,并给出强概率符号互模拟和概率符号同余的公理化系统,最后证明公理化系统的正确性和完备性。公理化系统的正确性比较容易证明,故本文的大部分篇幅用于证明其完备性。对于强概率符号互模拟,我们首先证明其同余性,在此基础上给出包含推导规则、选择规则和约束规则的公理化系统。同样地,我们证明任意进程都可以分解为多个相对简单的子进程之和。对于弱概率符号互模拟,由于其不具有同余性,我们提出了符号观测同余,并在强概率符号互模拟的基础上加入τ规则,组成了其公理化系统,其完备性证明同强互模拟一样。为了处理并发算子,我们使用了扩展规则,使任意并发算子都能够转化为等价的不含并发算子的进程。本文的创新点在于首次在概率选择和不确定选择同时存在的情况下,给出了概率符号互模拟的公理化系统。更多还原

【Abstract】 With the rapid development of computer technology and network communication,concurrent and distributed systems that feature concurrency, distribution, real time,heterogeneity and interoperability have become a major direction. The phenomenon ofconcurrency challenges computer scientists by its intrinsic complexity. Di?erent fromthat of sequentiality, its study is just beginning.Process algebra is a math framework mainly used to describe concurrent systems,it studies the phenomenon of concurrency, i.e. multiagent work together to achievea certain computing phenomenon through exchanging information. It is necessary tostudy the syntax and semantics of one process algebra and the axiomatic approach isan important way to study the semantics.During the recent years, randomization has been proved to be an useful tool in theconstruction of certain algorithms for concurrent systems. Compared to the determin-istic algorithms, randomization algorithms are normally more e?ciently, have simplerstructures and use less memory. More importantly, we can get better results that areimpossible for deterministic algorithms.Traditionally, the modeling of concurrent systems has abstracted away from quan-titative aspects. As a result, there is no information about how frequently or with whatchances certain behavior of a system will occur, whereas, at a practical level, thereneed to be distinctions relating to this, since many aspects of concurrent systems areprobabilistic in nature, or at least can be modeled as random behavior.In this thesis, we introduce a probabilistic progress calculus calledπsp.πsp is anextension ofπ-calculus which supports the co-existence of nondeterministic and prob-abilistic behaviors. We also introduce the definitions of strong probabilistic symbolicbisimulation, weak probabilistic symbolic bisimulation and probabilistic symbolic ob-servation congruence. Then we give the inference systems for strong probabilisticsymbolic bisimulation and probabilistic symbolic observation congruence respectively. Finally we prove the correctness and completeness of the inference systems. The cor-rectness part is obvious, so this thesis is devoted to the completeness. To the strongprobabilistic symbolic bisimulation, we prove its congruence at first and then give itsinference system including inference rules, choice rules and restriction rules. As usual,we also prove that any process can be decomposed to the sum of many subprocesses.As the weak probabilistic symbolic bisimulation is not congruent, we introduce thesymbolic observation congruence and give its inference system by addingτrules to theinference system of the strong case. We also use the expansion law to avoid the paralleloperator.This is the first work, to our knowledge, that provides complete axiomatizationfor probabilistic symbolic bisimulations in the presence of both nondeterministic andprobabilistic choice.更多还原