A Compact Petri Net Representation for Concurrent Programs

This paper presents a compact Petri net representation that is e cient to construct for concurrent programs that use explicit tasking and rendezvous style communication. These Petri nets are based on task interaction graphs and are called TIG-based Petri nets (TPN)s. They form a compact representation by abstracting large regions of program execution with associated summary information that is necessary for performing program analysis. We present a flexible framework for checking a variety of properties of concurrent programs using the reachability graph generated from a TPN. We present experimental results that demonstrate the benefit of TPNs over alternate Petri net representations and discuss the applicability ofPetri net reduction techniques to TPNs