Entry last updated: 2005/4/26
Entry last validated: 2005/4/26

Tool homepage: http://www.laas.fr/tina

Tool availability: Free of charge

Tool Features

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


Tool Description

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

nd: An editor for Petri nets, Time Petri nets, and automata, in textual or graphical form, interfaced with drawing tools and the analysis tools below. A stepper/simulator operating both in graphical and textual modes is packed with the editor.

tina: Builds various reachability graphs or state space abstractions for Petri nets and Time Petri nets. For Petri Nets: coverability graphs, markings graphs, and various partial graphs using Covering steps, Stubborn or Persistent sets, or Persistent steps. For Time Petri nets: various state class graph constructions, preserving markings, states, linear time properties, or branching time properties. Results may be produced in several popular formats.

struct: Computes semiflows (invariants) or flows on places and/or transitions, with various options.

Contact Information

7, avenue du Colonel Roche
31077 Toulouse CEDEX

Phone:  +33/(0)5 61 33 63 63
Fax:    +33/(0)5 61 33 64 11
E-mail: Bernard.Berthomieu@laas.fr

Other Remarks

Modelcheckers for LTL and the mu-calculus are forthcoming. No direct support is currently provided for performance or timeliness analysis, but many of such requirements can be checked by composing the Time Petri net models with "observer" nets that assert or contradict the properties to be proven.
[PN Home][*]
The maintainers of this page