Sub Asynchronous Pi-calculus And Its Fully Abstract Encoding

As multithreaded concurrent computing becomes more and more common in our lives,?-calculus is widely used in the modeling of dynamic systems as an important concurrent computing model.At the same time,asynchronous communication is more common in many concurrent systems,such as distributed systems.Therefore,based on the synchronization of the ?-calculus,an asynchronous ?-calculus that can communicate asynchronously is derived.So research on the expressive power of both has emerged.The most common research method is the transform encoding.However,limited by the control of the encoding on the name,the existing transform encoding has obvious deficiency:the equivalent object cannot be transformed into an equivalent object by the encoding,that is,the full abstraction property is not satisfied.This paper presents a sub asynchronous ?-calculus based on the asynchronous ?-calculus,and constructs a transform encoding from the synchronous ?-calculus to this calculus that satisfies the full abstraction.The main research work of the sub asynchronous?-calculus includes the following three aspects:· On the basis of not changing the asynchronous ?-calculus asynchronous communication capability,two different names of the principal names and the auxiliary names are constructed,and the auxiliary name is strengthened to control the reduction order.Furthermore,the characteristics of the sub asynchronous ?-calculus are studied,and the operational semantics are given by the labelled transition system.The model system of sub asynchronous ?-calculus is completely constructed.· The barbed equivalence relationship and bisimulation relationship in the sub asynchronous ?-calculus are defined.On this basis,the up-to bisimulation relationship is studied to further reduce the scale of the relationship.The research proves that the bisimulation relationship in the sub asynchronous ?-calculus is an absolute equivalence,a complete behavioral equivalence theory is formed.This theory can be used to analyze and verify the equivalence of different objects in the study of expressive ability.· The mirror version encoding of synchronous ?-calculus to sub asynchronous ?-calculus is realized.Corresponding to the operation consistency of the transfer,we solved the defect that the original encoding does not satisfy the completeness.And using the behavioral equivalence theory and the structural theorem to strictly prove the full abstraction of the the encoding under the bisimulation relationship,and verified by examples.In summary,the sub asynchronous ?-calculus and corresponding encoding studied in this paper enhances the control of names and makes multi-step reduction more controllable.The corresponding calculus construction rules,as well as proof techniques such as context's construction and up-to bisimulation used in the proof,provide a theoretical basis for further research on the fullly abstract encoding of asynchronous to synchronous communication.