Macchine a stati e reti di Petri (SMs)
Una rete di Petri a macchina stati è una rete in cui ogni transazione ha esattamente un posto in input e uno in output. Non c'è parallelismo e sincronizzazione. Sono permesse invece free-choice e confluenze. Se è presente un token iniziale e siccome il numero di token non varia nella rete, il token continua a girare nella rete. La rete è fortemente connessa e risulta che se c'è almeno un token iniziale la rete è live, e se ne ha esattamente uno la rete di Petri è anche safe.
Grafi marcati (MGs)
Sono reti di Petri in cui ogni posto ha esattamente un input ed esattamente un output. E' possibile avere parallelismo e sincronizzazione (sistemi concorrenti).
E' possibile definire i circuiti, come serie di transizioni (i circuiti non passano mai due volte per un nodo intermedio, ma vanno da un nodo di partenza, passano per altri nodi e tornano in quello di partenza). Aggiungiamo ad ogni sequenza in posizione finale la transazione iniziale e andiamo ad individuare le parti di percorso marcate da più percorsi.
Se tutti i circuiti contengono almeno un arco marcato allora la rete è live.
Gli MGs fortemente connessi sono sempre boundedness e i posti unbounded sono quelli che non stanno in nessun circuito. Il bound per ogni posto è pari al minimo numero di token di ogni circuito.
Se tutti i posti hanno token count uguale a 1, la rete è live.
Reti free-choice (FCs)
Sono reti di Petri che contengono sia MGs, che SMs. Esse permettono sincronizzazione e scelte libere. Bisogna analizzare i sifoni e le trappole. Queste reti per ogni transazione si possono avere più posti in uscita, ma ogni posto è collegato ad una sola transazione.
Un sottoinsieme ha un sifone se ha alcune transazioni in free-choice che lasciano i token all'interno di un sottoinsieme, mentre altre che le mandano all'esterno. Le transazioni che lasciano all'interno del sottoinsieme di stati si dicono neutre. Se c'è un sifone, un sottoinsieme vuoto rimane vuoto.
Un sottoinsieme ha una trappola se si hanno alcune transazioni neutre ed almeno una transazione che dall'esterno mette all'interno del sottoinsieme (in confluenza). Se c'è una trappola, un token che entra all'interno di un sottoinsieme non lo perde più.
Il teorema di Commoner afferma che una rete FC è live se e solo se tutti i sifoni includono tutte le trappole marcate inizialmente (si garantisce che i sifoni non siano mai vuoti).
L'unione di più sifoni/trappole è un sifone/trappola. Si possono avere dei sottinsiemi che contengono sia sifoni che trappole.
Extended free-choice (EFC)
Queste reti di Petri hanno la caratteristica di avere ogni posto che è collegato a transazioni in output in comune con un altro posto deve avere tutte le transazioni in output in comune. E' possibile trasformare una rete EFC in FCs con una sincronizzazione e una free-choice. Sono quindi applicabili gli algoritmi alla rete FC equivalente.
Reti Asymmetric-choice (AC)
Queste reti di Petri prevedono che se due posti hanno in comune una stessa transizione in output, allora anche tutto l'insieme delle transazioni di uno dei due stati sono un sottoinsieme delle transazioni dell'altra. Questa situazione di asimmetria si dice confusione.
Si può dimostrare che tutte le reti che contengono solo sifoni marcati inizialmente sono live, ma non il contrario (condizione sufficiente ma non necessaria).
Reti complesse
Quando la complessità è alta, bisogna applicare alcune regole di riduzione. La riduzione consente di avere reti più semplici equivalenti a quelle di partenza:
-fusione di posti in serie.
-fusione di transizioni in serie.
-fusione di posti in parallelo.
-fusione di transizioni in parallelo.
-rimozione di posti con loop su sé stessi.
-rimozione di transizioni con loop su sé stessi.
| < Prec. | Succ. > |
|---|
