The traditional technique to generate a global state-graph representation for
a concurrent system is to calculate the product of state-graph representations
of the local processes. We develop new techniques, and prove their correctness,
to help condensing intermediate state-graphs in the iterative
product-calculation. Experiments with Fischer's timed mutual exclusion
protocol have been carried out to justify the approach.