Entry last updated: 2007/3/22
Entry last validated: 2007/3/22

Tool homepage:

Tool availability: Free of charge

Tool Features

Petri Nets Supported (see also help on terminology) Components (see also help on terminology)


Tool Description

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.

Contact Information

Kimmo Varpaaniemi

Koivukyl„n puistotie 14 A 5
FI-01360 Vantaa

Phone:  +358 9 871 4976

Other Remarks

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.

[PN Home][*]
The maintainers of this page