An efficient well-specified check

A long-standing problem with generalized stochastic Petri nets and extensions is that of what to do when more than one zero-timed event is scheduled to occur at the same time. If the order is left unspecified, it could lead to ambiguity that affects reward variables. Stochastic activity nets (SANs) have used the well-specified condition to avoid this problem. However, the existing algorithm to perform the well-specified check is computationally complex, proportional to the number of paths through unstable markings. We provide some theoretical results that allow us to make use of a much more efficient algorithm, with complexity proportional to the number of arcs between unstable markings