The Verification Of Symbolic Bisimulations In Asymmetric X～≠-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 the main direction of current computer technology. Meanwhile, the intrinsic complexity of concurrent distributed computation makes the investigation and development of concurrent distributed system very difficult, and the correctness and dependability of such kind of system is too difficult to be assured. Therefore assuring the correctness and dependability of such kind of system is what should be solved urgently. While applying the formal method to the specification and verificaion of systems is an important approach to solve this problem.The process algebra is an important kind of formalization. The well-known process algebras include CCS, CSP and π-calculus. The process algebra, such as π-calculus, is widely applied to specification description, analysis, design, verification and information security of concurrent distributed system because of its concise concepts, rich available mathematical tools and flexible mathematical methods.The x-calculus is the development of π-calculus. From the operational viewpoint, the x-calculus is a symmetric mobile process calculus obtained from π-calculus by removing asymmetry of the latter. This modification results in significant change in observational properties. Many aspects of the x-calculus have been studied. These investigations help us to improve our understanding of π-like calculus for mobile processes. Interesting results about the x-calculus include the revelation of the subtlety of the weak observational equivalence relations and the discovery of the complex laws for these relations. But in the concurrent distributed systems, most of them communicate with each other asymmetrically, and the mismatch combinator is often required. Therefore, we study asymmetric x~≠-calculus, the s-calculus with asymmetric communication and mismatch operator in this thesis. The main contribution of the thesis includes the following three aspects:1. Inspired by Fu Yuxi's open bisimulations definition about x~≠-calculus, we give the strong open bisimulations definition of asymmetric x~≠-calculus, and the week version.2. Based on Lin Huiming's symbolic idea and Zhong Farong' operational semantic of...