Iterative Refinement and Condensation for State-Graph Construction

Farn Wang and Pao-Ann Hsiung
Institute of Information Science
Academia Sinica, Taipei, Taiwan.
( IIS Technical Reports, TR-IIS-98-009, 1998.)


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.