are the traces model, the stable failures model, and the failures/divergences model. Semantic mappings from process expressions to each of these three models provide the denotational semantics for CSP. The traces model defines the meaning of a process expression as the set of sequences of events (traces) that the process can be observed to perform. For example, since performs no events since the process can be observed to have performed no events, the event , or the sequence of events followed by More formally, the meaning of a process in the traces model is defined as such that: (i.e. contains the empty sequence) (i.e. is prefix-closed) where is the set of all possible finite sequences of events. The stable failures model extends the traces model with refusal sets, which are sets of events that a process can refuse to perform. A failure is a pair , consisting of a trace , and a refusal set which identifies the events that a process may refuse once it has executed the trace . The observed behavior of a process in the stable failures model is described by the pair . For example, The failures/divergence model further extends the failures model to handle divergence. The semantics of a process in the failures/divergences model is a pair where is defined as the set of all traces that can lead to divergent behavior and . Tools Over the years, a number of tools for analyzing and understanding systems described using CSP have been produced. Early tool implementations used a variety of machine-readable syntaxes for CSP, making input files written for different tools incompatible. However, most CSP tools have now standardized on the machine-readable dialect of CSP devised by Bryan Scattergood, sometimes referred to as CSPM. The CSPM dialect of CSP possesses a formally defined operational semantics, which includes an embedded functional programming language. The most well-known CSP tool is probably Failures/Divergence Refinement 2 (FDR2), which is a commercial product developed by Formal Systems (Europe) Ltd. FDR2 is often described as a model checker, but is technically a refinement checker, in that it converts two CSP process expressions into Labelled Transition Systems (LTSs), and then determines whether one of the processes is a refinement of the other within some specified semantic model (traces, failures, or failures/divergence). FDR2 applies various state-space compression algorithms to the process LTSs in order to reduce the size of the state-space that