Decidability Of Strong Equivalences For Finite Petri Nets

Tra i vari modelli di sistemi concorrenti e distribuiti proposti, le reti di Petri finite sono uno dei più studiati ed adatti alla descrizione di questo tipo di sistemi, poiché ne ricalcano le qualità distintive. Infatti, lo stato globale di una rete di Petri è formato da una collezione (detta marking) di stati locali (detti token). L'esecuzione di una transizione è una trasformazione locale che riguarda solo una parte dei token in un marking. Pertanto, si può interpretare un token come un processo sequenziale ed un marking come un sistema distribuito che porta avanti una computazione più complessa all'interno della quale i processi possono cooperare o competere. Le equivalenze interessanti su reti di Petri quindi devono considerare vari aspetti del modello, quali concorrenza (e relazioni di causalità), scelte e ramificazioni, invarianti. Nella prima parte del lavoro, si studiano equivalenze su reti Place/Transition (finite) safe e bounded. Sono riportati o provati alcuni risultati riguardanti due relazioni simili tra loro, che posseggono buona parte delle proprietà elencate sopra e considerano ogni esecuzione come un oggetto matematico a sè stante, detto processo. Le prove sono basate su una generalizzazione, per mezzo di indici, della tecnica di prova a marking ordinati usata da Vogler per dimostrare la decidibilità di fully-concurrent bisimilarity su reti safe. Nella seconda parte del lavoro, si studiano equivalenze su reti Place/Transition (finite) ma con archi inibitori e senza limiti al numero di token che possono occupare un posto, dette reti PTI. In questo modello, i token possono non solo permettere l'esecuzione di una transizione, ma anche bloccarla. Si formula una equivalenza, pti-place bisimilarity, che estende conservativamente place-bisimilarity e se ne prova la decidibilità. Questa è la prima volta che una equivalenza è provata essere decidibile per reti PTI. Tuttavia, rispetto alle altre equivalenze note, non è coinduttiva.