Tina Version 2.2.7

What is Tina ?

Tina is a toolbox for the analysis of Petri Nets and Time Petri Nets. At that time, it includes the tools:

nd (NetDraw):

Time Petri net and Automata editor, and graphic interface for tools.

tina:

Construction of reachability graphs. Depending upon the option retained, builds (references below):

• The coverability graph of a Petri net, by the Karp and Miller technique.

• The marking graph of a bounded Petri net.

• Partial marking graphs of a Petri net, preserving deadlocks, by the covering steps methods of (5,6), the method of pesistent sets, and several combinations of them.

• The graph of state classes of a Time Petri net, by the technique introduced in (1) and (2).

The graph of state classes allows verification of LTL formulas.
• As above, with interpretation of multi-enabledness (as in (3)).
• The graph of "atomic" classes, under two variants of the construction proposed in (4).
  The graph of atomic state classes allows verification of CTL or HML formulas.

struct:

Structural analysis of Petri nets.

• Determines the invariance and consistence properties for a net;
  computes the generator sets for semi-flows on places and transitions.

References

(1) B. Berthomieu, M. Menasche, An Enumerative Approach for Analyzing Time Petri Nets, IFIP Congress 1983, Paris, 1983.

(2) B. Berthomieu, M. Diaz, Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering, 17(3), 1991.

(3) B. Berthomieu, La méthode des Classes d'états pour l'Analyse des Réseaux Temporels - Mise en Oeuvre, Extension à la multi-sensibilisation. Modélisation des Systèmes Réactifs, MSR'2001, Hermes, 2001.

(4) T. Yoneda, H. Ryuba, CTL Model Checking of Time Petri Nets using Geometric Regions, IEICE Transactions on Inf. and Syst., vol E99-D, No 3, March 1998.

(5) F. Vernadat, P. Azéma, F. Michel, Covering Step Graph, 17th Int. Conf. on Application and Theory of Petri Nets 96, Osaka, Japan, Springer Verlag LNCS 1091, 1996.

(6) F. Vernadat, F. Michel, Covering Step Graph Preserving Failure Semantics, 18th Int. Conf on Application and Theory of Petri Nets 97, Toulouse, France, Springer-Verlag - LNCS 1248, 1997.

Bernard's Home Page