Prognosability analysis and enforcement of bounded labeled Petri nets

In this article, we deal with two problems related to bounded labeled Petri nets (PNs), namely prognosability analysis and enforcement. The solution we propose is based on a single tool, called prognosability verifier. Such a tool uses the notion of basis marking that avoids the exhaustive enumeration of all the reachable markings. This leads to advantages in terms of computational complexity that may be enormous in certain real applications. Finally, the enforcement problem can be solved associating a cost with each sensor eventually added to the system. A systematic way to compute a solution that minimizes the total cost of the new sensors while guaranteeing prognosability of the resulting system, is computed using linear integer programming.