has a graphical state-transition diagram editor. The user can model the behavior of processes as not only CSP expressions but also state-transition diagrams. The result of checking are also reported graphically as computation-trees and can be analyzed interactively with peripheral inspecting tools. In addition to refinement checks, It can perform deadlock check and livelock check. Related formalisms Several other specification languages and formalisms have been derived from, or inspired by, the classic untimed CSP, including: Timed CSP, which incorporates timing information for reasoning about real-time systems Receptive Process Theory, a specialization of CSP that assumes an asynchronous (i.e. nonblocking) send operation CSPP HCSP TCOZ, an integration of Timed CSP and Object Z Circus, an integration of CSP and Z based on the Unifying Theories of Programming CML (COMPASS Modelling Language), a combination of Circus and VDM developed for the modelling of Systems of Systems (SoS) CspCASL, an extension of CASL that integrates CSP LOTOS, an international standard that incorporates features of CSP and CCS. PALPS, a probabilistic extension with locations for ecological models developed by Anna Philippou and Comparison with the actor model In as much as it is concerned with concurrent processes that exchange messages, the actor model is broadly similar to CSP. However, the two models make some fundamentally different choices with regard to the primitives they provide: CSP processes are anonymous, while actors have identities. CSP uses explicit channels for message passing, whereas actor systems transmit messages to named destination actors. These approaches may be considered duals of each other, in the sense that processes receiving through a single channel effectively have an identity corresponding to that channel, while the name-based coupling between actors may be broken by constructing actors that behave as channels. CSP message-passing fundamentally involves a rendezvous between the processes involved in sending and receiving the message, i.e. the sender cannot transmit a message until the receiver is ready to accept it. In contrast, message-passing in actor systems is fundamentally asynchronous, i.e. message transmission and reception do not have to happen at the same time, and senders may transmit messages before receivers are ready to accept them. These approaches may also be considered duals of each other, in the sense that rendezvous-based systems can be used to construct buffered communications that behave as asynchronous messaging systems, while asynchronous systems can be used to construct rendezvous-style communications by using a message/acknowledgement protocol to synchronize senders