A Rewriting Logic Based Tool for ECATNets Coverability Analysis

N. Boudiaf(1*), A. Chaoui(2)

(1) Laboratoire LIRE, Université de Constantine, Algeria
(2) Laboratoire LIRE, Université de Constantine, Algeria
(*) Corresponding author

DOI's assignment:
the author of the article can submit here a request for assignment of a DOI number to this resource!
Cost of the service: euros 10,00 (for a DOI)


To analyze the behavior of Petri nets, the reachability graph allows verifying qualitative properties. However, even for small nets, the reachability graph can become infinite if the analyzed Petri net is unbounded. To deal with the state space explosion problem, lazy construction methods to consider only reduced state spaces have been elaborated. For example, the stubborn set reduced reachability graph is usually much smaller than the complete one, but it exhibits all dead states, if any. For unbounded nets, coverability graphs must be used. ECATNets are a category of algebraic Petri nets based on a sound combination of algebraic abstract types and high level Petri nets. The most distinctive feature of ECATNets is that their semantics is defined in terms of rewriting logic and its language Maude, allowing us to built models by formal reasoning. In this paper, we propose a rewriting logic based tool that implements an algorithm aiming the construction of coverability graph for ECATNet. Some qualitative properties such as the absence of deadlock can be checked using the constructed coverability graph. The development of this tool is facilitated thanks to the concept of the reflectivity of rewriting logic : the self-interpretation of this logic allows us both the modelling of an ECATNet and acting on it. The tool is illustrated through an example.
Copyright © 2015 Praise Worthy Prize - All rights reserved.


Coverability Graph; ECATNets; Rewriting Logic; Maude; Dynamic Analysis; Finite-state Systems; Infinite-state Systems

Full Text:



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.

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), American Mathematical Society, 1992, pp. 43-55.

N. Boudiaf, A. Chaoui, Dynamic Analysis Algorithm for ECATNets, Proceedings of MOCA’04, October 11-13, 2004, ISSN 0105-8517, Daniel Moldt (Ed.), Aarhus, University, Denmark, pp. 47-63.

N. Boudiaf, A. Chaoui, A Rewriting Logic Based Tool for Automated Support of ECATNets Reachability Analysis, Proc. of CSITeA’04, December 27-29, 2004, Cairo, EGYPT, ISBN 0.9742059.1.5, (Organized by: Winona State University, USA).

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and C. Talcott, The Maude 2.0 System, Proc. Rewriting Techniques and Applications (RTA), Volume 2706 of LNCS, Spring-Verlag , 2003, pp. 76-87.

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.

C. Girault and P. Estraillier, CPN-AMI. MASI Lab, University Paris VI, France.

T. Lindner, Formal Development of Reactive Systems : Case Study Production Cell, Volume 891 of LNCS, Spring-Verlag, 1995, pp. 7-15.

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, p. 417-424., 1997.

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.

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), p. 89-117, 2000.

V. Pinci and L. Zand, DESIGN/CPN, USA, 1993.

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.

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.


  • There are currently no refbacks.

Please send any question about this web site to info@praiseworthyprize.com
Copyright © 2005-2022 Praise Worthy Prize