A COMPACT PETRI-NET REPRESENTATION AND ITS IMPLICATIONS FOR ANALYSIS

This paper explores a property-independent, coarsened, multilevel repr esentation for supporting state reachability analysis for a number of different properties. This multilevel representation comprises a reach ability graph derived from a highly optimized Petri net representation that is based on task interaction graphs and associated property-spec ific summary information. This highly optimized representation reduces the size of the reachability graph but may increase the cost of the a nalysis algorithm for some types of analyses. This paper explores this tradeoff. To this end, we have developed a framework for checking a v ariety of properties of concurrent programs using this optimized repre sentation and present empirical results that compare the cost to an al ternative Petri net representation. In addition, we present reduction techniques that can further improve the performance and yet still pres erve analysis information. Although worst-case bounds for most concurr ency analysis techniques are daunting, we demonstrate that the techniq ues that we propose significantly broaden the applicability of reachab ility analyses.