×

zbMATH — the first resource for mathematics

The tool TINA – construction of abstract state spaces for Petri nets and time Petri nets. (English) Zbl 1060.68695
Summary: 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.

MSC:
68W30 Symbolic computation and algebraic computation
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
TINA
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] DOI: 10.1142/9789814343459
[2] Bérard B, Systems and Software Verification Model-Checking Techniques and Tools (2001) · Zbl 1002.68029
[3] Berthomieu B 2001 La méthode des classes d’états pour l’analyse des réseaux temporels – mise en oeuvre, extension à la multi-sensibilisation Proceedings of Modélisation des Systèmes Réactifs, Toulouse, France
[4] DOI: 10.1109/32.75415 · Zbl 05113493
[5] Berthomieu B, Springer (2003)
[6] Diaz M, In Les Réseaux de Petri. Modéles fondamentaux (2001)
[7] Fernandez J-C, Springer (1996)
[8] Fernandez J-C, Springer (1991)
[9] Fribourg L, Springer (1999)
[10] Godefroid P, Partial-Order Methods for the Verification of Concurrent Systems (1996) · Zbl 1293.68005
[11] Godefroid P, Springer (1991)
[12] DOI: 10.1016/S0022-0000(69)80011-5 · Zbl 0198.32603
[13] Mazurkiewicz A, Springer (1986)
[14] DOI: 10.1109/TCOM.1976.1093424 · Zbl 0362.68096
[15] Milner R, Communication and Concurrency (1985)
[16] DOI: 10.1137/0216062 · Zbl 0654.68072
[17] Peled D, Springer (1998)
[18] Ribet P-O, Springer (2002)
[19] Ribet P-O Vernadat F Berthomieu B 2003 Graphe de pas couvrant préservantLTL-XReport 03053. LAAS-CNRS
[20] Tripakis S, Springer (1996)
[21] Valmari A, Springer (1989)
[22] Van Glabbeek RJ, Springer (1990)
[23] Vernadat F, Springer (1996)
[24] Vernadat F, Springer (1997)
[25] Vernadat F, In Vérification et mise en oeuvre des réseaux de Petri, Hermes Science (2003)
[26] Yoneda T, IEEE Transactions on Information and Systems 99 pp 1– (1998)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.