Abstract: To analyze the behavior of Petri nets, the accessibility
graph and Model Checking are widely used. However, if the
analyzed Petri net is unbounded then the accessibility graph becomes
infinite and Model Checking can not be used even for small Petri
nets. ECATNets [2] are a category of algebraic Petri nets. The main
feature of ECATNets is their sound and complete semantics based on
rewriting logic [8] and its language Maude [9]. ECATNets analysis
may be done by using techniques of accessibility analysis and Model
Checking defined in Maude. But, these two techniques supported by
Maude do not work also with infinite-states systems. As a category
of Petri nets, ECATNets can be unbounded and so infinite systems.
In order to know if we can apply accessibility analysis and Model
Checking of Maude to an ECATNet, we propose in this paper an
algorithm allowing the detection if the ECATNet is bounded or not.
Moreover, we propose a rewriting logic based tool implementing this
algorithm. We show that the development of this tool using the
Maude system is facilitated thanks to the reflectivity of the rewriting
logic. Indeed, the self-interpretation of this logic allows us both the
modelling of an ECATNet and acting on it.