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 for analysis
of systems that use asynchronous communication. In particular,
we show that for many problems, multiple unbounded reliable channels
can be reduced to a single channel for verification purposes.