Exploiting Symmetry for Analysis of Distributed Systems

Distributed systems are difficult to design and the simplest of them can have subtle errors. Conventional automatic analysis techniques to catch these errors may be infeasible because the system may have a large, or even an unknown, number of processes. These techniques, which are based on state space exploration, run into the state explosion problem. Since most distributed systems have one or more sets of identical processes, we exploit the symmetry to reduce the state space for automatic analysis techniques. We describe a model called Decomposed Petri Net that facilitates such analysis. We present symbolic and induction techniques to analyze concurrent systems described using Decomposed Petri Net. We illustrate our techniques by analyzing several examples: 2-out-of-3 problem, dining philosophers problem and mutual exclusion problem. These techniques are applicable to systems that are configured either in a star topology or a ring topology. We also show how to extend these techniques ..