PROD 3.4.01
An Advanced Tool for Efficient Reachability Analysis

The Pr/T-net reachability analysis tool PROD implements several methods for efficient reachability analysis.

PROD is a text-based tool that can be used in UNIX (any system of that kind) and in Windows (3.1, 3.11, '95, NT, '98, 2000, XP). Currently no graphical user-interface exists. PROD supports the following reduced reachability graph generation methods that may also be combined:

PROD supports verification of CTL formulas from the reachability graph, and on-the-fly verification of LTL formulas using e.g. the stubborn set method.

PROD has been used e.g. in the Emma project and in the analysis of the Frame Synchronised Ring, a video on demand system, an authentication protocol (HUT-TCS Reports A29, A36, B14), the ISDN-DSS1 protocol, and a PLC-based railway traffic control system.

Documentation for PROD is available as HUT-TCS Report B13 with an up-to-date addendum. Those who download the tool get this documentation automatically.

Kimmo Varpaaniemi <>