Diagnosability analysis of unbounded Petri nets

In this paper we consider the property of diagnosability for labeled unbounded Petri nets, namely Petri nets where the number of tokens in one or more places can grow indefinitely. We give necessary and sufficient conditions for diagnosability and we present a test to study diagnosability based on the analysis of the coverability graph of a particular net, called verifier net, that is built starting from the initial system. To the best of our knowledge, this is the first available test for diagnosability analysis of labeled unbounded Petri nets. We also discuss existing methods to perform diagnosis of unbounded Petri nets.