Analysis of Petri Nets with a Dynamic Priority Method

. In this paper we propose an efficient reachability set based Petri net analysis by introducing dynamic priorities which decreases the number of reachable markings in most cases. It is proved that for specific dynamic priority relations certain properties (especially liveness and the existence of home states) do hold if and only if these properties do also hold for the Petri net without priorities. We present an algorithm based on these priority relations additionally exploiting T-invariants thus being able to benefit from the structure of the net. 1 Introduction Analysis of Petri nets by exploring the set of reachable markings is a straightforward approach, since most properties are defined on the basis of the reachability graph[12]. Although this kind of analysis of Petri nets suffers from the well-known state space explosion problem, it is offered by most analysis tools[7], because it is easy to implement and in case of error detection appropriate traces (firing sequences)..