Tina man pages
(included in Tina distributions)Tutorial on Time Petri Nets
An advanced tutorial on Time Petri Nets was given at the 29th International Conference on Application and Theory of Petri Nets (ICATPN 2008, Xi'an, China, June 2008), by L. Popova and B. Berthomieu. The slides can be found on that page.Papers and reports
[1] B. Berthomieu, M. Menasche, An Enumerative Approach for Analyzing Time Petri Nets, IFIP Congress 1983, Paris, 1983. [ps.gz] [pdf]
[2] B. Berthomieu, M. Diaz, Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering, 17(3), 1991. [pdf]
[3] B. Berthomieu, La méthode des Classes d'états pour l'Analyse des Réseaux Temporels - Mise en Oeuvre, Extension à la multi-sensibilisation, Modélisation des Systèmes Réactifs, MSR'2001, Hermes, 2001. [ps.gz] [pdf]
[4] B. Berthomieu, P.-O. Ribet, F. Vernadat, The tool TINA -- Construction of Abstract State Spaces for Petri Nets and Time Petri Nets, International Journal of Production Research, Vol. 42, No 14, July 2004. [?] [ps.gz] [pdf]
[5] B. Berthomieu, F. Vernadat, State class constructions for branching analysis of Time Petri nets, In Proceedings of TACAS 2003. Springer Verlag, LNCS 2619, ISBN 3-540-00898-5, p. 442. [ps.gz] [pdf]
[6] F. Vernadat, P. Azéma, F. Michel, Covering Step Graph, 17th Int. Conf. on Application and Theory of Petri Nets 96, Osaka, Japan, Springer Verlag LNCS 1091, 1996. [ps.gz] [pdf]
[7] F. Vernadat, F. Michel, Covering Step Graph Preserving Failure Semantics, 18th Int. Conf on Application and Theory of Petri Nets 97, Toulouse, France, Springer-Verlag - LNCS 1248, 1997. [ps.gz] [pdf]
[8] P-O. Ribet, F. Vernadat, B. Berthomieu, On Combining the Persistent Sets Method with the Covering Steps Graph Method, In Proceedings of FORTE 2002. Springer Verlag, LNCS 2529, ISBN 3-540-00141-7. [ps.gz] [pdf]
[9] B. Berthomieu, P.-O. Ribet, F. Vernadat, L'outil TINA -- Construction d'espaces d'états abstraits pour les réseaux de Petri et réseaux Temporels, Modélisation des Systèmes Réactifs, MSR'2003, Hermes, 2003. [ps.gz] [pdf]
[10] B. Berthomieu, D. Lime, O. H. Roux, F. Vernadat, Problèmes d'accessibilité et espaces d'états abstraits des réseaux de Petri temporels à chronomètres, Modélisation des Systèmes Réactifs -- MSR'2005, Journal européen des systèmes automatisés, RS JESA, Vol. 39, No 1-2-3, Hermes, 2005. [ps.gz] [pdf]
[11] B. Berthomieu, D. Lime, O. H. Roux, F. Vernadat, Reachability Problems and Abstract State Spaces for Time Petri Nets with Stopwatches. Journal of Discrete Event Dynamic Systems, 17:133-158, 2007 (A short version in French appeared as [10]). [ps.gz] [pdf]
[12] B. Berthomieu, F. Vernadat, Réseaux de Petri temporels : méthodes d'analyse et vérification avec TINA, Ecole d'été temps réel 2006, Nancy. Traité IC2 "Systèmes temps réel 1 -- techniques de description et de vérification", Ed. Nicolas Navet, Hermes 2006. [ps.gz] [pdf]
[13] B. Berthomieu, F. Vernadat, State Space Abstractions for Time Petri Nets, Handbook of Real Time Systems, 2006. [ps.gz] [pdf]
[14] B. Berthomieu, F. Vernadat, Time Petri Nets Analysis with TINA, tool paper, In Proceedings of 3rd Int. Conf. on The Quantitative Evaluation of Systems (QEST 2006), IEEE Computer Society, 2006. [ps.gz] [pdf]
[15] B. Berthomieu, F. Peres, F. Vernadat, Bridging the gap between Timed Automata and Bounded Time Petri Nets, In Proceedings of FORMATS 2006. Springer Verlag, LNCS 4202, 2006. [ps.gz] [pdf]
[16] B. Berthomieu, F. Peres, F. Vernadat, Model-checking Bounded Prioriterized Time Petri Nets, ATVA 2007. Springer LNCS 4762, 2007. [pdf]
[17] F. Peres, B. Berthomieu, F. Vernadat, On the composition of time petri nets. Discrete Event Dynamic Systems, 21(3), 395-424, 2011. [editor]
[18] B. Berthomieu, S. Dal Zilio, Ł. Fronc, F. Vernadat, Time petri nets with dynamic firing dates: Semantics and applications. In International Conference on Formal Modeling and Analysis of Timed Systems (pp. 85-99). Springer LNCS 8711. 2014. [editor] [pdf]
[19] P-A. Bourdil, B. Berthomieu, S. Dal Zilio, F. Vernadat, Symmetry reduction for time Petri net state classes. Science of Computer Programming, 132, 209-225, 2016. [editor] [pdf]
[20] B. Berthomieu, D. Le Botlan, S. Dal Zilio, Petri Net Reductions for Counting Markings. In International Symposium on Model Checking Software (SPIN 2018), Springer LNCS 10869, 2018. [editor] [pdf]
[21] B. Berthomieu, D. Le Botlan, S. Dal Zilio, Counting Petri net markings from reduction equations. International Journal on Software Tools for Technology Transfer, 22(2), 163-181, 2020. [editor] [pdf]
More papers and reports
[22] B. Berthomieu, M. Menasche, A state enumeration approach for analyzing Time Petri nets, In Proceedings of Application and Theory of Petri nets (ATPN) 1982, Varenna, Italy, 1982.[pdf]
[23] J-L. Roux, B. Berthomieu, Verification of a local area network protocol with Tina, a software package for Time Petri nets, In Proceedings of Application and Theory of Petri nets (ATPN) 1986, Oxford, UK, 1986.[pdf]
[24] B. Berthomieu, N. Choquet, C. Colin, B. Loyer, J-M. Martin, A. Mauboussin, Abstrat Data Nets -- Combining Petri nets and Abstract Data Types for high level specifications of distributed systems, In Proceedings of Application and Theory of Petri nets (ATPN) 1986, Oxford, UK, 1986.[pdf]
[25] B. Chezalviel-Pradin. Un outil graphique intéractif pour la vérification des systèmes à évolution parallèle décrits par reéseaux de Petri. Thèse de docteur-ingénieur. Université Paul Sabatier, Toulouse. 1979.
[26] M. Menasche, Analyse des Réseaux de Petri Temporisés et Application aux Systèmes Distribués, Thèse de docteur-ingénieur. Université Paul Sabatier, Toulouse. Nov. 1982.
[27] M. Menasche, B. Berthomieu, Time Petri Nets for Analyzing and Verifying Time Dependent Communication Protocols, Third IFIP/WG6.1 International Workshop on Protocol Specification, Testing and Verification, Zurich, Switzerland, May 1983.
[28] Jean Rénalier. Analyse et simulation en langage APL de systèmes de commande décrits par des réseaux de Petri. Thèse de l'Université Paul Sabatier - Toulouse III, Toulouse, 1977.
[29] B. Berthomieu. Analyse Structurelle des Réseaux de Petri, Concepts, Méthodes et Outils. Thèse de docteur-ingénieur. Université Paul Sabatier, Toulouse. 1979.