  This paper presents the notion of AND-OR reduction, which reduces a WF net to
a smaller net by iteratively contracting certain well-formed subnets into
single nodes until no more such contractions are possible. This reduction can
reveal the hierarchical structure of a WF net, and since it preserves certain
semantical properties such as soundness, it can help with analysing and
understanding why a WF net is sound or not. The reduction can also be used to
verify if a WF net is an AND-OR net. This class of WF nets was introduced in
earlier work, and arguably describes nets that follow good hierarchical design
principles. It is shown that the AND-OR reduction is confluent up to
isomorphism, which means that despite the inherent non-determinism that comes
from the choice of subnets that are contracted, the final result of the
reduction is always the same up to the choice of the identity of the nodes.
Based on this result, a polynomial-time algorithm is presented that computes
this unique result of the AND-OR reduction. Finally, it is shown how this
algorithm can be used to verify if a WF net is an AND-OR net.
