Modelli della concorrenza Lucia Pomello Re# di Petri: proprietà di comportamento e verifica stru6urale NOTA
Se tutti i posti di una rete P/T hanno capacità finita k,
allora la rete è k-limitata
(ogni posto conterrà al più k marche, in ogni marcatura raggiungibile).
La restrizione sulla capacità può essere eliminata aggiungendo il complemento
Ogni sistema elementare è equivalente a una rete P/T senza peso degli archi e con capacità K(s) = 1 per ogni posto s. Ogni sequenza di occorrenze di transizioni della rete
corrisponde a un cammino orientato nel grafo,
e viceversa.
Una rete P/T
non deadlock-free
e il suo “grafo delle marcature”
Una rete PT è deadlock-­‐free se e solo se il suo grafo delle marcature non ha ver#ci senza successori. Assenza di deadlock non implica vivezza Questa rete P/T è deadlock-free ma non viva
alcune transizioni sono morte in una marcatura raggiungibile
Assenza di deadlock non implica vivezza Questa rete P/T è deadlock-free ma non viva
Ogni rete viva è deadlock-­‐free Una rete P/T è viva se e solo se in nessuna marcatura raggiungibile una transizione è morta (può non essere abilitata di nuovo) Una rete P/T è limitata (bounded) se e solo se
il suo insieme di marcature raggiungibili è finito
(il suo grafo delle marcature è finito)
Rete P/T non limitata
Una rete P/T 1-­‐safe con n pos# ha al più 2n marcature raggiungibili reversibilità
Una rete P/T è reversibile se e solo se
il suo grafo delle marcature è strettamente connesso
Rete P/T 1-safe, non viva, non reversibile
Rete P/T non limitata e non reversibile
Rete P/T viva, 1-safe, non reversibile
Tecniche di analisi delle proprietà basate sulla struttura del grafo della rete
Condizione necessaria per la raggiungibilità di una marcatura Una marcatura m è raggiungibile da m0 solo se l’equazione ha una soluzione per x Invarian>: P-­‐invarian> e T-­‐invarian> Un P-­‐invariante (S-­‐invariante) è un ve6ore di pos# che soddisfa l’equazione: Vale così la legge di conservazione delle marche: per ogni marcatura raggiungibile m da m0 Un P-­‐invariante individua quindi un insieme di pos# in cui, comunque evolva il sistema, le marche opportunamente pesate rimangono costan#. La legge di conservazione può essere usata per provare la non raggiungibilità di m. U#lizzo dei P-­‐invarian# per provare proprietà: mutua esclusione, limitatezza,…. Una rete P/T è coperta da P-­‐invarian> sse per ogni posto s esiste un P-­‐invariante posi#vo i: i(s) >0 Condizione sufficiente per la limitatezza Se una rete P/T è coperta da P-­‐invarian# allora è limitata Condizione necessaria per la vivezza
Se una rete P/T, senza pos# isola#, è viva allora ogni P-­‐invariante deve essere marcato in m0. Invarian>: P-­‐invarian> e T-­‐invarian> Un T-­‐invariante è un ve6ore di transizioni che soddisfa l’equazione: Dall’equazione delle marcature raggiungibili: segue che un T-­‐invariante rappresenta un ve6ore di Parikh che individua una sequenza di transizioni che, se abilitata, perme6e di rio6enere la marcatura data. Esempio di T-­‐invarian> Ad esempio i seguen# ve6ori sono T-­‐invarian#: (1, 1, 0, 0) (0, 0, 1, 1) (2, 2, 1, 1) Condizione necessaria per la vivezza e la limitatezza
Ogni rete P/T viva e limitata è coperta da T-­‐invarian> (ha un T-­‐invariante j tale che per ogni transizione t: ) P-invarianti
Questa rete è coperta da P-invarianti monomarcati:
è quindi limitata (1-bounded o 1-safe)
T-­‐invarian# La rete è coperta da T-­‐invarian# Una rete viva è coperta da T-invarianti, ma non necessariamente vale il viceversa.
deadlock
Una rete coperta da P-invarianti è limitata, non vale in generale il viceversa:
Esempio di sistema P/T limitato ma non coperto da P-invarianti positivi
SIFONI E TRAPPOLE
Sia N = (P, T, F) una rete P/T.
•  Un SIFONE è un insieme di posti tali che se non sono marcati,
comunque evolva il sistema, rimangono non marcati
un sottoinsieme di posti S è un sifone se e solo se •S ≤ S•
Se S è un sifone allora: se t• ∩ S ≠ Ø allora •t ∩ S ≠ Ø.
•  Una TRAPPOLA è un insieme di posti tali che una volta
marcato, comunque evolva il sistema, rimane marcato
un sottoinsieme di posti Q è una trappola se e solo se Q• ≤ •Q,
Se Q è una trappola allora: se •t ∩ Q ≠ Ø allora t• ∩ Q ≠ Ø
{s1, s2} è un sifone
{s3, s4} è una trappola
Se una marcatura m è tale che :
- m(s1) = m( s2) = 0, allora lo stesso vale per tutte le marcature successive
- m(s3) + m(s4) > 0 , allora lo stesso vale per tutte le marcature successive
SIFONI E TRAPPOLE
Il seguente sistema P/T ∑ = (P, T, F, M0) non è reversibile.
Si consideri invece ∑ = (P, T, F, M1) con M1 = {p1}
{p1, p4, p5} è una trappola inizialmente marcata  M = {p2, p3} non è raggiungibile,
in M infatti i posti {p1, p4, p5} sono non marcati.
SIFONI E TRAPPOLE Se una rete P/T è viva, allora ogni sifone con#ene almeno un posto marcato in m0 Una rete P/T è deadlock-­‐free, se ogni sifone con#ene una trappola marcata in m0 Una rete free-­‐choice è viva se e solo se ogni sifone con#ene una trappola marcata in m0 Dove le re# free-­‐choice sono tali che: