RGA is an interpreter for a special language designed for the analysis of reachability graphs, or control flow graphs, generated from Petri nets. Although in some cases the reachability graph can become too large to be tractable, or can even be infinite, many interesting problems exist whose reachability graphs are of reasonable size. In RGA, the user has access to the names of the places in the net, and to the states of the reachability graph. The structure of the graph is also available through functions which return the sets of successor or predecessor states of a state and the transition-firings connecting the states. The RGA language allows dynamic typing of identifiers, recursion, and function and operator overloading. Rather than providing a number of predefined analysis functions, RGA provides primitive functions which allow the user to conduct complex analyses with little programming effort. RGA is part of a suite of tools, called P-NUT, intended to facilitate the analysis of concurrent systems described by Petri nets.

RGA is an interpreter for a special language designed for the analysis of reachability graphs, or control flow graphs, generated from Petri nets. Although in some cases the reachability graph can become too large to be tractable, or can even be infinite, many interesting problems exist whose reachability graphs of reasonable size. In RGA, the user has access to the names of the places in the net, and to the states of the reachability graph. The structure of the graph is also available through functions which return the sets of successor or predecessor states of a state, and the transition-firings connecting the states. The RGA language allows dynamic typing of identifiers, recursion, and function and operator overloading. Rather than providing a number of predefined analysis functions, RGA provides primitive functions which allow the user to conduct complex analyses with little programming effort. RGA is part of a suite of took intended to make the analysis of concurrent systems described by Petri nets easier.

The availability of low-cost powerful processors has made distributed computer systems a reality. Currently, the major stumbling block in the design of these systems is the difficulty of designing and validating concurrent software which is to control and execute on the new processors. There is a need for new techniques and tools for modeling and evaluating designs of distributed computer systems during early stages of design. The Distributed Systems Project at UCI has been investigating Petri Net-based modeling techniques and has developed a suite of tools, named P-NUT, for constructing and analyzing complex Petri Net models. This paper describes the motivation behind the selection of the Petri Net model, and describes the tools which currently exist.

The introduction of concurrency into programs has added to the complexity of the software design process. This is most evident in the design of communications protocols where concurrency is inherent to the behavior of the system. The complexity exhibited by such software systems makes more evident the needs for computer-aided tools for automatically analyzing behavior.

The Distributed Systems project at UCI has been developing a suite of tools, based on Petri nets, which support the design and evaluation of concurrent software systems. This paper focuses attention on one of the tools: the reachability graph analyzer (RGA). This tool provides mechanisms for proving general system properties (e.g., deadlock-freeness) as well as system-specific properties. The tool is sufficiently general to allow a user to apply complex user-defined analysis algorithms to reachability graphs. The alternating-bit protocol with a bounded channel is used to demonstrate the power of the tool and to point to future extensions.