On Analysis of Boundness Property for ECATNets by Using Rewriting Logic

Authors: Noura Boudiaf, Allaoua Chaoui

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.

Keywords: ECATNets, Rewriting Logic, Maude, Finite-stateSystems, Infinite-state Systems, Boundness Property Checking.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1074453

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.