Un réseau de Petri temporel (RPT, en anglais TPN pour time Petri net) est l'une des techniques permettant de spécifier et vérifier des systèmes dans lesquels le temps apparaît comme un paramètre quantifiable et continu. Il en existe deux types : le réseau de Petri P-temporel et le réseau de Petri T-temporel. Les sémantiques formelles de ces modèles ainsi qu'une comparaison de leurs expressivités en termes de bisimulation temporelle et d'acceptation de langage temporisé ont été proposées en 2008Boyer M and Roux OH. On the compared expressiveness of arc, place and transition time Petri nets. Fundamenta Informaticae, 88(3):225-249, 2008..
Histoire Il existe deux principales familles d'extensions temporelles de réseau de Petri : le réseau de Petri temporelMERLIN P. M., « A study of the recoverability of computing systems », PhD thesis, Department of Information and Computer Science, University of California, Irvine, CA, 1974. introduit par Philip Meir Merlin en 1974 et le réseau de Petri temporisé RAMCHANDANI C., « Analysis of asynchronous concurrent systems by timed Petri nets », PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, 1974. introduit par Chander Ramchandani en 1974.
Définition Un réseau de Petri temporel est un tuple dans lequel: est un réseau de Petri, avec pour places P, transitions T, marquage initial et , est une fonction appelée Intervalle Statique, est un ens. fini d’Actions, ou Labels, ne contenant pas l’action silencieuse , est une fonction d’Étiquetage des transitions.
Notes et références
Articles connexes Réseau de Petri Réseau de Petri P-temporel Réseau de Petri T-temporel
Catégorie:Méthode formelle