Preface

The Integrated Net Analyzer INA is a program with whose help Petri nets of very different kinds can be investigated under different firing rules (in particular timing) with regard to their general properties. Typical properties which can be verified through the analysis are boundedness of places, liveness of transitions, and reachability of markings or states.

When modelling an existing or projected system in the language of Petri nets, the underlying abstraction process assigns certain properties of the system to properties of the net, e.g. the absence of deadlocks in the system can correspond to the non-reachability of a dead marking.

The life cycle of a net model can be roughly sketched out as follows:

• Design
• Analysis
• Interpretation
• Re-design

Therein the interpretation of the analytical results is not to be underestimated.

INA was developed by Prof. Dr. Peter H. Starke. With this interactive, menu-driven program you can edit, reduce, execute and analyze nets. It comprises the analytical procedures offered in the earlier toolkits ``Petri-Net-Machine'', ``PAN'', ``CPNA'', and ``ATNA'' and was essentially expanded upon by Dr. Karsten Schmidt, Dipl.-Inf. Lutz Pogrell, Dipl.-Inf. Karsten Lüttke and Dipl.-Inf. Stephan Roch.

This manual describes the functionality of version 2.2 of INA . It was written by Stephan Roch in collaboration with Prof. Peter H. Starke, and translated by Dirk Schlatter with the help of Stefan Haar and Mathew O'Breigh (partially supported by the Deutsche Forschungsgemeinschaft in the ``PEP''-project).

A certain knowledge of net theory - at least of its fundamental definitions - is necessary to understand this program. For that purpose we refer to the book ``Analyse von Petri-Netz-Modellen'' published 1990 in the series ``Leitfäden und Monographien der Informatik'' by B. G. Teubner, Stuttgart [Sta90]. Many of the algorithms implemented in INA are described there in greater detail.

No responsibility is assumed for any mistakes in this manual or in the program.

Berlin, April 1999

Peter H. Starke and Stephan Roch