The Modelling and Analysis of Security Protocols: the CSP Approach

4.3. Exploiting compositional structure

The classic problem in analyzing the behaviour of concurrent systems is the way the states of component processes combine to form the state of the whole. The best general bound on the number of states in the parallel composition of an M-state process with an N-state process is M × N, although this is not always achieved: the requirement for synchronization may make parts of the component state-spaces unreachable, and synchronization may also impose a large degree of correlation between their states. Nonetheless, systems that we want to analyze, including those arising in the present context, tend to be large; to the extent that keeping track of the visited states is the principal limiting factor on the ...