摘要：AbstractTesting is a fundamental technique for system design and verification to ensure security and reliability. However its application to discrete event systems modeled by unbounded synchronized Petri nets is not straightforward because there exists no finite exact representation for the infinite state space of these models. In this paper, we consider a special class of synchronized Petri nets, called 1-place-unbounded, that contain a single unbounded place. We show how a coverability graph that precisely describes the state space of such a model can be constructed extending to synchronized nets a technique previously presented for place/transition nets. In addition, this algorithm can also be used to verify whether a given synchronized Petri net contains exactly a single unbounded place. Next, we show that any net belonging to this special class can be converted into an equivalent weighted automaton. Based on this conversion, we observe that the testing of 1-place-unbounded synchronized Petri nets can be approached using the methods and results existing in the literature for the testing of weighted automata.
关键词：KeywordsSynchronized Petri netsunbounded netscoverability graphweighted automata
