Finite Axiomatization For Symbolic Probabilistic Pi-Calculus

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.