Analysis of distributed systems with many identical processes
Vijay K. Garg · 2003
The symmetry of distributed systems that have one or more sets of identical processes, is used to reduce the state space for automatic analysis techniques. A model called the Synchronous Token-based Communicating State Model (STOCS) is proposed to facilitate specification and analysis of symmetric distributed systems. Symbolic and inductive techniques to analyze the STOCS are described. The techniques are demonstrated by analyzing the 2-out-of-3, readers-writers, dining philosophers, and mutual exclusion problems.>