I have a simple Petri net like Fig.1 and I want to analyze behavioral properties like the rechability graph, boundedness, liveness, and coverability.
Originally the net isn't bounded since P3 takes more tokens in every cycle by firing transition T2.
There is a limitation about firing sequence so that every transition just can fire maximum two times that means that token can circulate into the net at most two times. then available firing sequences are {t1 t2 t1 t2; t1 t2 t3 t4; t3 t4 t1 t2; t3 t4 t3 t4} and reachability graph for this status is {1 0 0 0; 0 1 0 0; 1 0 1 0;0 1 1 0;1 0 2 0;0 0 0 1;0 0 1 1}. so rechability graph with limitation for firing transitions is bounded.
1.can we consider this net as a bounded net regarding firing limitation?
2.what we can say about the liveness of this net?
2.what we can say about the coverability of this net?
If every transition can fire only a limited number of times, you can only reach a finite number of states. Any Petri net with a finite number of reachable states is bounded. Just iterate over all states and get the maximum number of tokes for each place, those are your bounds.
With that firing limitation, the liveness is $~L_1~$. Each transition can fire at least once, but only a limited number of times.
Coverability graphs are a way to deal with Petri nets that have an infinite number of reachable states, or at least an unmanageable large number. With that firing limitation, your net reaches only a finite and rather low number of states.