Réseau de Petri temporel
# Réseau de Petri temporel

Un réseau de Petri temporel (RdP) (en anglais, time Petri net - TPN) 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 existe deux types de réseaux de Petri temporels: 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 2008.

## Histoire

Il existe deux principales familles d'extensions temporelles de réseau de Petri : le réseau de Petri temporel introduit par Philip Meir Merlin en 1974 et le réseau de Petri temporisé introduit par Chander Ramchandani en 1974.

## Définition

Un Réseau de Petri temporel (ou TPN) est un tuple $(P,T,Pre,Post,M^{0},I_{s},\Sigma ^{z},L)$ dans lequel:

* $(P,T,Pre,Post,M^{0})$ est un réseau de Petri, avec pour places P, transitions T, marquage initial $m^{0}:P\to \mathbb {N^{+}}$ et $Pre,Post:T\to P\to \mathbb {N^{+}}$,
* $Is:T\to \mathbb {I^{+}}$ est une fonction appelée Intervalle Statique,
* $\Sigma$ est un ens. fini d’Actions, ou Labels, ne contenant pas l’action silencieuse $\sigma$,
* $L:T\to \Sigma ^{z}$ est une fonction d’Étiquetage des transitions.
