Reasoning about Networks with Many Identical Finite-State Processes.

If we consider a distributed mutual exclusion algorithm for processes arranged in a ring network in which mutual exclusion is guaranteed by means of a token that is passed around the ring. A first attempt might be to consider a reduced system with with one or two processes. If the reduced system can be shown to be correct and of the individual processes are really identical, then we are tempted to conclude that the entire system will be correct. This type of informal argument is used quite frequently by designers in constructing systems that contain large numbers of identical processing elements. It is easy to contrive an example in which some pathological behavior only occurs when, say, 100 processes are connected together. By examining a system with only one or two processes it might be quite difficult to determine that this behavior is possible. One has the feeling that in many cases this kind of intuitive reasoning does lead to correct results. The question addressed is whether it is possible to provide a solid theoretical basis that will prevent fallacious conclusions in arguments of this type. Besides providing a firm basis for a common type of informal reasoning, our results are crucial for the success of automatic verification methods that involve temporal logic model checking. These techniques check that a finite-state concurrent system satisfies a temporal logic formula by searching all possible paths in the global state graph determined by the concurrent system. They have been used successfully to find subtle errors in tricky self-timed circuits--errors apparently unknown to the circuit designers. By using these results, model checking may become feasible for networks with large numbers of identical processes.