On the analysis of Petri nets with static priorities (Q1901713)

Priority specifications offer a convenient description technique to resolve conflicts in favour of particular actions. Apart from being employed for the specification of the functional behaviour of a system, priorities have also become important in the field of performance analysis using stochastic Petri nets. Here they are implicitly given due to the separation of transitions into immediate and timed. In the performance analysis of such stochastic Petri nets specific properties, like liveness and existence of home states, are of major interest, because they ensure the applicability of a Markovian based analysis. Since several efficient analysis techniques have been developed for Petri nets without priorities, our interest is in using these techniques also for the priority case. This paper shows that positive properties of a net such as liveness and the existence of home states do also hold for the net with static priorities, if a simple condition is imposed on the priority relation.