Computation of synchronizing sequences for a class of 1-place-unbounded synchronized Petri nets

Identification of a final state after red a test is one of the fundamental testing problems for discrete event systems and synchronizing sequences represents a conventional solution to this problem. In this paper, we consider systems modeled by a special class of synchronized Petri nets, called 1-place-unbounded, that contain a single unbounded place. The infinite reachability spaces of such nets can be characterized by two types of finite graphs, called improved modified coverability graph and weighted automata with safety conditions. In case these two finite graphs are deterministic, we develop novel computation algorithms for synchronizing sequences for this class of nets by decomposing the finite graphs into strongly connected components.