Rete di Petri colorata

Una rete di Petri colorata (CPN, acronimo inglese per Coloured Petri Net) sono una estensione del concetto di rete di Petri, di cui ne conserva le proprietà ed estende il formalismo per permettere la distinzione tra token^[1].

Una rete è definita da: N = (P, T, A, Σ, C, N, E, G, I ) dove:

P è un insieme di posti
T è un insieme di transizioni
A è un insieme di archi

L'insieme dei posti, transizioni ed archi sono a coppie disgiunti P ∩ T=P ∩ A=T ∩ A=∅

C è una funzione di colore. Mappa i posti in P in colori in Σ.
N è una funzione nodo. Mappa A in (P × T)∪(T × P).
E è una funzione d'espressione d'arco. Mappa ogni arco a∈A nell'espressione e.
G è una funzione guardia. Mappa ogni transizione t∈T in un'espressione di guardia g. L'uscita dell'espressione ha un valore booleano.
I è una funzione d'inizializzazione. Mappa ogni posto p in una espressione di inizializzazione i. L'espressione di inizializzazione deve valutare un insieme di token con un colore che corrisponde al colore del posto C(p).