Counterexamples to "liveness-enforcing supervision of bounded ordinary Petri nets using partial-order methods"

This note shows by means of simple counterexamples that some key results presented by He and Lemmon in the above paper (Automat. Contr., vol. 47, pp. 1042-1055, July 2002) on the liveness verification and enforcing of Petri nets using unfolding are incorrect. As a result, the applicability of unfolding for Petri net supervision is still an open issue.