On Analysis of Boundness Property for ECATNets by Using Rewriting Logic

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.

Authors:

• Noura Boudiaf
• Allaoua Chaoui

Keywords:

• ECATNets
• Rewriting Logic
• Maude
• Finite-stateSystems
• Infinite-state Systems
• Boundness Property Checking.

References:

[1] G. Berthelot, C. Johnen, and L. Petrucci. "PAPETRI : environment for
the analysis of Petri nets". Volume 3 of Series in Discrete Mathematics
and Theoretical Computer Science (DIMACS), p. 43-55. American
Mathematical Society, 1992.
[2] M. Bettaz, M. Maouche. "How to specify Non Determinism and True
Concurrency with Algebraic Term Nets". Volume 655 of LNCS, Spring-
Verlag, 1993, pp. 11-30.
[3] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer,
and C. Talcott. "The Maude 2.0 System". In Proc. Rewriting Techniques
and Applications (RTA), Volume 2706 of LNCS, Spring-Verlag , 2003,
pp. 76-87.
[4] A. Finkel. "The Minimal Coverability Graph for Petri Nets". In:
Rozenberg, G.: Volume 674 of LNCS,; Advances in Petri Nets 1993,
Springer-Verlag, 1993, pp. 210-243.
[5] C. Girault and P. Estraillier, "CPN-AMI". MASI Lab, University Paris
VI, France.
[6] T. Lindner. "Formal Development of Reactive Systems : Case Study
Production Cell". Volume 891 of LNCS, Spring-Verlag, 1995, pp. 7-15.
[7] M. Maouche, M. Bettaz, G. Berthelot and L. Petrucci. "Du vrai
Parallélisme dans les Réseaux Algébriques et de son Application dans
les Systèmes de Production". Conférence Francophone de Modélisation
et Simulation (MOSIM-97), Hermes, 1997, pp. 417-424.
[8] J. Meseguer. "Rewriting Logic as a Semantic Framework of
Concurrency: a Progress Report". Seventh International Conference on
Concurrency Theory (CONCUR'96), Volume 1119 of LNCS, Springer
Verlag, 1996, pp. 331-372.
[9] J. Meseguer. "Rewriting logic and Maude: a Wide-Spectrum Semantic
Framework for Object-based Distributed Systems". In S. Smith and C.L.
Talcott, editors, Formal Methods for Open Object-based Distributed
Systems, (FMOODS-2000), 2000, pp. 89-117.
[10] V. Pinci and L. Zand. "DESIGN/CPN". USA, 1993.
[11] S. Roch and P.H. Strake. "INA (Integrated Net Analyzer) : Version 2.2".
Manual, Humboldt-Universität zu Berlin Institut für Informatik,
Lehrstuhl f├╝r Automaten- und Systemtheorie, 1999.
[12] K. Varpaaniemi, J. Halme, K. Hiekkanen, and T. Pyssysalo. "PROD
reference manual". Technical Report B13, Helsinki University of
Technology, Digital Systems Labora tory, Espoo, Finland, August 1995.