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. Includes interfaces for analysis tools below and drawing facilities.tina: Construction of reachability graphs. Inputs nets in textual or graphical format. Outputs graphs in textual form or Aldebaran automata format. Depending on options retained, builds (references below):
struct: Structural analysis of Petri nets (preliminary).
- 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, by the covering steps methods of [6,7], the method of persistent sets,
or several combinations of them explained in [8]. These constructions preserve deadlocks.- The graph of state classes of a Time Petri net, by the technique introduced in [1], and further described in [2,3].
The graph of state classes allows reachability analysis and verification of LTL formulas.- As above, with interpretation of multi-enabledness, as in [3].
- The graph of "atomic" classes of a Time Petri net, under an improvement of the construction proposed in [4], explained in [5].
The graph of atomic state classes allows liveness analysis and verification of CTL or HML formulas.
- Determines the invariance and consistence properties for a net;
computes the generator sets for semi-flows on places and transitions.
[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] B. Berthomieu, F. Vernadat, State class constructions for branching analysis of Time Petri nets, LAAS Report 02130, March 2002. (to appear at TACAS'03)
[6] 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.
[7] 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.
[8] P-O. Ribet, F. Vernadat, B. Berthomieu, On Combining the Persistent Sets Method with the Covering Steps Graph Method, LAAS Report 02388, November 2002. (to appear at FORTE'02)
Bernard's Home Page