The tool TINA – construction of abstract state spaces for Petri nets and time Petri nets. (English) Zbl 1060.68695

Berthomieu, B.; Ribet, P.-O.; Vernadat, F.

Int. J. Prod. Res. 42, No. 14, 2741-2756 (2004).

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

References:

[1]	DOI: 10.1142/9789814343459 · doi:10.1142/9789814343459
[2]	Bérard B, Systems and Software Verification Model-Checking Techniques and Tools (2001) · Zbl 1002.68029 · doi:10.1007/978-3-662-04558-9
[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 · doi:10.1109/32.75415
[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 · doi:10.1007/3-540-60761-7
[11]	Godefroid P, Springer (1991)
[12]	DOI: 10.1016/S0022-0000(69)80011-5 · Zbl 0198.32603 · doi:10.1016/S0022-0000(69)80011-5
[13]	Mazurkiewicz A, Springer (1986)
[14]	DOI: 10.1109/TCOM.1976.1093424 · Zbl 0362.68096 · doi:10.1109/TCOM.1976.1093424
[15]	Milner R, Communication and Concurrency (1985)
[16]	DOI: 10.1137/0216062 · Zbl 0654.68072 · doi:10.1137/0216062
[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)