Concurrent calculus (CC) and its properties

Concurrent calculus (CC) is a mathematical model for higher-order concurrent and communicating systems. Compared with the existing calculi such as CCS^[1], CMP^[2], CHOCS^[3] etc., CC includes λ-calculus^[4] as its subtheory and embodies most important characteristics of CCS and other calculi. CC treats processes and communicating ports as first-class objects, that is to say, both of them can be sent and received during communication. Besides, the communicating ports in CC-processes are allowed to be any expressions. This paper presents the syntax and semantics of CC first, some examples are given which illustrate the expressing power of CC. Then we study the high-order bisimulation equivalence of CC-processes and the algebraic laws of CC. The summation operator "+" in CC has the same meaning as that in other calculi. Following the principle that only environment can determine the evolution direction of summation process, this paper also provides a new semantics of summation operator "+", which is different from the semantics of summation in CCS, CMP, and CHOCS. CC has some expected algebraic properties under this new semantics of summation.