ABSTRACT
Specific characteristics of the mCRL2 process algebra are local communication, multiactions, and communication-independent parallelism. Local communication
allows one to specify communications within subcomponents of the system without affecting the rest of the system. This makes the language particularly suitable for component-based and hierarchical systems. Global communication, which is typically used in other languages, only allows communication to be defined on a global level for the system as a whole. Multiactions enable the specification of (not necessarily related) actions that are to be executed together. Most process algebras only allow a single action to be executed atomically thus forcing an order on the execution of actions. By allowing multiple actions to be executed together, certain systems (such as low-level hardware) can be modeled in a more straightforward manner. These multiactions also allow the separation of parallelism and communication. When two actions can execute at the same time, a multiaction with those actions is the result. Communication can then be applied to these multiactions to make certain actions communicate with each other.
