Grafo di copertura della rete di Petri
Cos'è il grafo di copertura
Il grafo di copertura è la rappresentazione sintetica di una rete marcata di Petri con duplicazioni. E' la sintesi di un albero di copertura.
A cosa serve?
Mi consente di rappresentare una rete marcata che presenta cammini duplicati, altrimenti impossibili da disegnare con un grafo di raggiungibilità.
Nota. Se la rete marcata non ha nodi duplicati, l'albero di copertura coincide con l'albero di raggiungibilità.
Un esempio pratico
Ho una rete di Petri composta da tre posti e due transizioni.
Per ridurre al minimo la spiegazione, prendo come riferimento un albero di copertura.
Alcune foglie dell'albero hanno l'etichetta "duplicato".
Per trasformare l'albero in un grafo di copertura
- Sostituisco ogni arco verso i nodi duplicati con un arco verso il nodo originale. Può anche trattarsi di un cappio.
- Elimino i nodi duplicati e le etichette "duplicato" dal grafo.
Il risultato è il grafo di copertura della rete di Petri.
Ha le stesse proprietà dell'albero di copertura ma è senza dubbio più sintetico.
Nota. Il grafo di copertura può essere disposto anche in orizzontale o in qualsiasi altro modo. Non deve necessariamente seguire la disposizione top-down degli alberi logici.
La differenza tra il grafo di raggiungibilità e il grafo di copertura
A differenza del grafo di raggiungibilità, il grafo di copertura si può usare anche se l'insieme di raggiungibilità è infinito. Non va in loop.
Per il resto il grafo di copertura ha le stesse proprietà di un grafo di raggiungibilità.
- Se esiste un nodo M nel grafo, allora la marcatura M è raggiungibile dalla marcatura iniziale. E viceversa.
- Se esiste un cammino orientato dal nodo M0 al nodo M nel grafo, allora la sequenza di transizioni σ=t1t2t3... appartiene al linguaggio L(N,M)
Se non ci sono nodi duplicati il grafo di copertura coincide con il grafo di raggiungibilità.
E così via.
