Process Calculus are mathematically rigorous languages with well defined semantics that permit describing and verifying properties of concurrent communicating systems. They can be seen as models of processes, regarded as agents that act and interact continuously with other similar agents and with their common environment. Many different approaches are taken for describing the meaning of processes. Leading examples of process calculus include CSP, CCS, ACP, and LOTOS. In many implementations, channels have rich internal structure to improve efficiency, but this is abstracted away in most theoretic models.