The tool TINA – Construction of abstract state spaces for Petri nets and Time Petri nets

In addition to the graphic-editing facilities, the software tool Tina proposes the construction of a number of representations for the behaviour of Petri nets or Time Petri nets. Various techniques are used to extract views of the behaviour of nets, preserving certain classes of properties of their state spaces. For Petri nets, these abstractions help prevent combinatorial explosion, relying on so-called partial order techniques such as covering steps and/or persistent sets. For Time Petri nets, which have, in general, infinite state spaces, they provide a finite symbolic representation of their behaviour in terms of state classes.