  In this paper, we study the problem of non-blockingness verification by
tapping into the basis reachability graph (BRG). Non-blockingness is a property
that ensures that all pre-specified tasks can be completed, which is a
mandatory requirement during the system design stage. In this paper we develop
a condition of transition partition of a given net such that the corresponding
conflict-increase BRG contains sufficient information on verifying
non-blockingness of its corresponding Petri net. Thanks to the compactness of
the BRG, our approach possesses practical efficiency since the exhaustive
enumeration of the state space can be avoided. In particular, our method does
not require that the net is deadlock-free.
