The Modelling and Analysis of Security Protocols: the CSP Approach

1.5. Process behaviour

Concurrent systems seem to be inherently more difficult to understand than sequential ones. Rather than having a single process that works through its program in a linear fashion a step at a time, we may have many that interact in ways that are less predictable and create the potential for

• deadlock, in which, though each individual node may well be willing to do something, the system as a whole cannot agree on any action;

• livelock, in which an infinite sequence of hidden internal communications occur between components, so that the external appearance is much like a deadlocked system;

• nondeterminism, which though it appears in CSP from various angles, arises most naturally – and unavoidably – in the situation where two processes ...