Each Petri net type defi nes validity and soundness properties, whereas validity refers to a correct net structure (i.e. a net speci cation which makes sense somehow) and soundness typically refers to workflow-speci c properties of Petri nets. The soundness property implies a valid Petri net. A further typical net property is the boundedness of a net.
Validity and Soundness
We can check for validity in Wolfgang and get some topological information of the net. A P/T-Net is valid, if its structure makes sense, e.g. flow relations don’t connect two places or vice versa. A valid P/T-Net is also sound.
CPNs require flow relation eff ectiveness for validity. This means, that each relation must move at least one token from a place to a transition or vice versa. For the soundness property no more conditions must be met, s.th. a valid CPN is also sound.
Based on the fact that in both net types validity also implies soundness, the soundness check is omitted in Wolfgang.
Boundedness
A Petri net is bounded if and only if, for every reachable state and every place p the number of tokens in p is bounded. The boundedness property on a Petri net is checked by building the marking graph. If the number of possible sequences is finite or smaller than the maximum possible value for the integer data type, the Petri net is bounded. Otherwise the Petri net is assumed to be unbounded.