La raggiungibilità delle marcature in una rete di Petri
La raggiungibilità di una marcatura studia quali stati sono raggiungibili in una rete di Petri del tipo P/T a partire da una marcatura iniziale <N,M0>.
Mi permette di capire quali stati sono raggiungibili dalla macchina.
Per studiare la raggiungibilità di una rete utilizzo il grafo di raggiungibilità se lo spazio degli stati è finito.
Se invece lo spazio degli stati è infinito, utilizzo il grafo di copertura.
Nota. Il problema della raggiungibilità di una marcatura è un problema semi-decidibile perché se la marcatura è raggiungibile in uno spazio di stati infinito l'algoritmo termina la ricerca in k passi (problema decidibile). Se non è raggiungibile l'algoritmo non termine mai la ricerca.
E così via.
