One thread of research related to reachability analysis involves extracting models from program texts. This paper shows that the nature of the translation from source code to a modeling formalism is of greater practical importance than the underlying formalism. (With respect to the underlying formalisms we present algorithms for translating Taylor's reduced flowgraph model and Long and Clarke's task interaction graph model into a common labeled flowgraph formalism, and for translating labeled flowgraphs into Petri nets, while preserving the reachability graph structure.)
Features identified as pragmatically important are the representation of internal choice, selection of a dynamic or static matching rule, and the ease of applying reductions. Since combinatorial explosion is the primary impediment to application of reachability analysis, a particular concern in choosing a model is facilitating divide-and-conquer analysis of large programs. Recently, much interest in finite-state verification systems has centered on algebraic theories of concurrency. Algebraic structure can be used to decompose reachability analysis based on a flowgraph model. The semantic equivalence of graph and Petri net based models suggests that one ought to be able to apply a similar strategy for decomposing Petri nets. We show this is indeed possible through application of category theory.