Sartomiki.net

Reti di Petri
Le reti di Petri permettono di descrivere in maniera dettagliata sia gli stati, che le attività. In più è possibile avere un collegamento con i dati. Esistono diverse tipologie di reti:
-ordinarie, che permettono di esprimere la concorrenza e la sincronizzazione. Modellazione e analisi.
-colorate, che permettono di collegare gli schemi con i dati.
-dipendenti dal tempo, permettono di gestire la temporizzazione (simulazione…)
-operazionali, che permettono di implementare dei veri e propri sistemi, mediante un linguaggio di alto livello.

Reti ordinarie
Esistono diversi simboli:
-posti (cerchi).
-transizioni (rettangoli schiacciati). Una transazione è abilitata quando tutti i token in ingresso sono abilitati. Se è abilitata una transazione può scattare se si verifica un evento e provoca che i token in ingresso vengano tolti e che essi vengano riempiti tutti i i token in uscita.
-precedenze (archi) collegano posti con transizioni.
-token (pallini) permettono di rappresentare lo stato iniziale e i movimenti. I token complessivi nella rete possono variare per numero.
Una rete di Petri risulta essere un grafo connesso. Posti e transizioni hanno dei nomi associati.
L'insieme degli stati è dato dall'insieme di combinazioni di token che si possono avere nella rete (reachability graph).
E' possibile avere grafi illimitati, nel caso in cui ci siano cicli. In questo caso ci sono posti illimitati (unbounded). In questo caso si utilizza una rappresentazione approssimata mediante coverability graph. Uno stato copre strettamente un altro stato quando tutti i suoi elementi sono uguali allo stato coperto a parte quelli diversi che sono maggiori. In questo caso è possibile approssimare il valore che cresce con un valore illimitato, segnalabile con omega.
Una rete di Petri è una 4-tupla (Posti P, Transizioni T, archi F, peso W). E' possibile dare dei pesi agli archi (quando il peso è 1, esso si omette). Il peso influisce sul numero di token generati da una transizione.

Definizioni
I grafi marcati sono tutte le reti di Petri in cui tutti i posti hanno esattamente un input ed esattamente un output (non si possono usare scelte o confluenze, ma si può utilizzare la sincronizzazione).
Due marcature sono raggiungibili (direttamente o indirettamente), se una o più transazioni portano da una marcatura all'altra (non è detto che la proprietà sia vicendevole).
Una marcatura copre strettamente un'altra marcatura se i campi corrispondenti sono uguali, mentre quelli diversi sono maggiori nella marcatura coprente.

Proprietà delle reti di Petri
-Limitatezza (boundedness). Una rete è bounded se il numero dei token in ogni marcatura è finito. Il limite massimo delimita il k-bounded della rete.
--Safeness è una rete in cui il massimo numero di token per ogni marcatura è uguale a 1 (1-bounded).
-Vitalità (liveness). Una rete è live se tutte le transizioni sono live, cioè se per ogni marcatura M' è possibile raggiungere M'', che può portare a un'altra transazione. Una transizione che non è raggiungibile è detta dead. Una transizione è detta L1-live se almeno una marcatura comporta il raggiungimento della transazione.
-deadlock-freedom, è una rete in cui ogni transazione attiva almeno un'altra transazione. Non esistono quindi posti senza uscite.
-Reversibilità (reversibilità), per ogni marcatura è possibile raggiungere la marcatura iniziale. Una rete è home state se ogni marcatura è raggiungibile da tutte le altre.
Queste proprietà sono indipendenti (ortogonali).
Per analizzare le proprietà  si può costruire l'albero/grafo di marking, oppure analizzare se la rete fa parte di qualche sottoclasse (market graphs o free chioce nets).

Costruzione dell'albero/grafo di raggiungibilità (copertura)
-si calcola il marking iniziale (new).
-per tutti i nodi new non ancora analizzati.
-se non ci sono transizioni abilitate (dead-end).
-altrimenti per ogni transazione, si calcola la marcatura M' e si va a vedere se esiste una marcatura M'' <= M'. In questo caso si sostituiscono i valori > con omega (rete unbounded).
-se la marcatura è già stata ottenuta si marca come old.
-altrimenti la marcatura diventa new.
-terminato il processo il nodo viene messo a esaminato.
E' possibile convertire un albero in un grafo, non introducendo nodi old, ma collegando direttamente il nodo di partenza a quello che già esiste.