Counterexamples to “Liveness-Enforcing Supervision of Bounded Ordinary Petri Nets Using Partial-Order Methods”
Xiaolan Xie, Alessandro Giua · IEEE Transactions on Automatic Control · 2004
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.