StrataGEM: A Generic Petri Net Verification Framework

  • Edmundo López Bóbeda
  • Maximilien Colange
  • Didier Buchs
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8489)


In this paperwe present the Strategy Generic Extensible Modelchecker (StrataGEM), a tool aimed at the analysis of Petri nets and other models of concurrency by means of symbolic model-checking techniques. StrataGEM marries the well know concepts of Term Rewriting (TR) to the efficiency of Decision Diagrams (DDs). TR systems are a great way to describe the semantics of a system, being readable and compact, but their direct implementation tends to be rather slow on large sets of terms. On the other hand, DDs have demonstrated their efficiency for model-checking, but translating a system semantics into efficient DDs operations is an expert’s matter. StrataGEM describes the semantics of a system in terms of strategies over a TR system, and automatically translates these rules into operations on DD to handle the model-checking. The ultimate goal of StrataGEM is to become a verification framework for the different variants of Petri nets by separating the semantics of the model from the computation that performs model-checking.


Cluster Detection Symbolic Model Check Term Rewrite System Term Rewrite Verification Framework 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.: Symbolic Model Checking: 1020 States and Beyond. Information and Computation 98(2), 142–170 (1992)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Ciardo, G., Marmorstein, R., Siminiceanu, R.: Saturation Unbound. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 379–393. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  3. 3.
    Wolper, P., Godefroid, P.: Partial-Order Methods for Temporal Verification. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 233–246. Springer, Heidelberg (1993)Google Scholar
  4. 4.
    Buchs, D., Hostettler, S.: Sigma Decision Diagrams. In: Corradini, A. (ed.) TERMGRAPH 2009: Preliminary Proceedings of the 5th International Workshop on Computing with Terms and Graphs. Number TR-09-05 in TERMGRAPH Workshops, Università di Pisa, pp. 18–32 (2009)Google Scholar
  5. 5.
    Goguen, J.A., Meseguer, J.: Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. Theor. Comput. Sci. 105, 217–273 (1992)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.E., Vittek, M.: ELAN: A Logical Framework Based on Computational Systems. Electronic Notes in Theoretical Computer Science 4, 35–50 (1996)CrossRefGoogle Scholar
  7. 7.
    Balland, E., Brauner, P., Kopetz, R., Moreau, P.-E., Reilles, A.: Tom: Piggybacking Rewriting on Java. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 36–47. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 8.
    Hamez, A., Thierry-Mieg, Y., Kordon, F.: Hierarchical Set Decision Diagrams and Automatic Saturation. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol. 5062, pp. 211–230. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    International Organization for Standardization: ISO/IEC. Software and Systems Engineering - High-Level Petri Nets, Part 1: Concepts, Definitions and Graphical Notation. International Standard ISO/IEC 15909 (December 2004)Google Scholar
  10. 10.
  11. 11.
    Pelánek, R.: BEEM: Benchmarks for Explicit Model Checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  12. 12.
    Kordon, F., Buchs, D.: Model Checking Contest Page,
  13. 13.
    MoVe Team: The PNXDD Home Page (2013),
  14. 14.
    Hong, S., Kordon, F., Paviot-Adet, E., Evangelista, S.: Computing a Hierarchical Static Order for Decision Diagram-Based Representation from P/T Nets. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) ToPNoC V. LNCS, vol. 6900, pp. 121–140. Springer, Heidelberg (2012)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Edmundo López Bóbeda
    • 1
  • Maximilien Colange
    • 1
  • Didier Buchs
    • 1
  1. 1.Centre Universitaire d’InformatiqueUniversité de GenèveCarougeSuisse

Personalised recommendations