tina logo

TIme petri
Net Analyzer

laas logo

About Tina

TINA (TIme petri Net Analyzer) is a toolbox for the editing and analysis of Petri Nets, with possibly inhibitor and read arcs, Time Petri Nets, with possibly priorities and stopwatches, and an extension of Time Petri Nets with data handling called Time Transition Systems. TINA has been developed in the OLC, then VerTICS, research groups of LAAS/CNRS. General Petri nets information can be found on the Petri Nets World site.

The TINA toolbox includes the tools:

nd (NetDraw): Editor and GUI for Petri nets, Time Petri Nets and Automata.

tina: Construction of reachability graphs.

sift: Construction and checking of reachability graphs.

struct: Structural analysis of nets.

plan: Path analysis.

selt: A State/Event LTL model checker.

muse: A modal mu-calculus model checker.

play: Stepper simulator.

pathto: Path finder.

ndrio: Conversion tool for Time Petri nets.

ktzio: Conversion tool for Kripke transition systems.

tedd: Construction of symbolic reachability graphs.

reduce: State space preserving reductions of Place/Transition nets.

walk: Constrained ramdon walker.

frac: Fiacre to tina tts compiler.