Animation and exchanges in the Petri Nets community

[Fabrice Kordon <address@concealed>]

GOALS

   The Model Checking Contest (MCC) is a yearly event that assesses existing
   verification tools for concurrent systems on a set of models (i.e.,
   benchmarks) proposed by the scientific community. All tools are compared on
   the same benchmarks and using the same computing platform, so that the
   fairest comparison possible can be made, contrary to most scientific
   publications, in which different benchmarks are executed on different
   platforms.

   The Model Checking Contest is organized in three steps: 
   - the present Call for Models (http://mcc.lip6.fr/cfm.html),
   - the Call for Tools (http://mcc.lip6.fr/cft.html),
   - and the Contest itself.

CALL FOR MODELS

   At the core of the Model Checking Contest is a collection of models
   (http://mcc.lip6.fr/models.html) accumulated from the previous editions of
   the contest. This collection currently comprises 132 different models, 
which
   have been already used and cited in more than 180 scientific publications.

   For the 2025 edition, we kindly ask the scientific community (beyond the
   developers of verification tools) to propose novel models. Each model 
should
   be representative of a non-trivial academic or industrial problem that
   involves concurrency aspects, and may belong to very diverse fields such as
   software or hardware design, networking, biology, etc.

   All submitted models will be reviewed by the Model Board and we expect a
   dozen new models to be selected and added to the MCC collection. The 
authors
   of the selected models will be acknowledged on the Model Checking Contest
   web site.

   All submitted models should be kept confidential until the list of selected
   models has been published. This is to ensure that the 2025 models are not
   known in advance by the tool developers participating in the Model Checking
   Contest.

   By submitting a model, you explicitly allow the organizers of the Model
   Checking Contest to freely use this model and publish it on the web.
   Submitted models are expected to become part of the public domain. If your
   model is proprietary, do not submit it. Detailed information is available
   from http://mcc.lip6.fr/rules.html.

SUBMISSION DETAILS
 
   A model can be either a "classical" P/T net [1], a Nested-Unit Petri net
   [2,3], or a colored Petri net [4,5,6] (with/without guards on transitions,
   cartesian product on colors, and successor/predecessor functions). For a
   colored net, an equivalent "unfolded" P/T net [7] may be provided as well.

   A model may depend on one or many parameters that enable scaling (e.g., in
   the number of places, transitions, tokens, colors, etc.). To each
   parameterized model are associated as many "instances" (typically, between 
2
   and 20) as there are different combinations of values considered for the
   parameters of this model; each non-parameterized model has a single
   associated instance.

   Detailed instructions for submission are given in the model submission kit
   available from http://mcc.lip6.fr/2025/archives/ModelSubmissionKit.tar.gz.

   To submit a model, four types of files should be provided, two of which are
   required.


Required files:

   - A PNML [8,9] file describing the model. If the model is parameterized and
     exists in different instances, or if it is colored and has an equivalent
     P/T net, then several PNML files are provided. For information about the
     PNML format, please refer to the web site http://www.pnml.org and contact
     address@concealed if help is needed. For information about
     Nested-Unit Petri nets, please refer to http://mcc.lip6.fr/nupn.html and
     contact address@concealed or address@concealed if help is
     needed.
   - A LaTeX form that must be filled in to provide summary information about
     the model, its origin, its size, etc. See http://mcc.lip6.fr/models.html
     for examples of such a form.

Recommended files:

   - If possible, a picture of the model to be included in the LaTeX form.
   - If possible, a set of relevant properties (typically, invariants, bounds,
     reachability, LTL or CTL formulas) that can be evaluated on this model.
     These properties can be expressed informally in English or given as XML
     files. Submitted properties, which are most useful to produce meaningful
     benchmarks, will be reviewed by the Formula Board.

IMPORTANT DATES

   - January 6, 2025: publication of the present Call for Models
   - May 15, 2025: deadline for model submission (for the MCC'2025)
   - June 1st, 2025: individual notification of model acceptance/rejection
   - June 15, 2025: on-line publication of the selected MCC'2025 models
   - June 24, 2025: announcement of MCC'2025 results during the Petri Net
     Conference conference (Geneva, Switzerland)

COMMITTEES

   General Chair
      Fabrice Kordon - Sorbonne Université/LIP6, France

   Model Board
      Quentin Nivon - Inria/LIG, France

   Execution Board
      Francis Hulin-Hubard - CNRS, France
      Fabrice Kordon - Sorbonne Université, France     

   Formula Board
      Loïg Jezequel - Univ. Nantes, France
      Emmanuel Paviot-Adet - Univ. Paris 5, France
        
REFERENCES

   [1] C. A. Petri and W. Reisig. Petri net. Scholarpedia, 3(4):6477, 2008.
       Online. http://www.scholarpedia.org/article/Petri_net

   [2] H. Garavel. Nested-unit Petri nets. Journal of Logical and Algebraic
       Methods in Programming, vol. 104, pages 60-85, April 2019.

   [3] NUPN manual page. Online. http://cadp.inria.fr/man/nupn.html

   [4] G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad. Stochastic
       well-formed colored nets and symmetric modeling applications. IEEE 
Trans.
       Computers, 42(11):1343–1360, 1993.

   [5] ISO/IEC. Software and Systems Engineering - High-level Petri Nets, Part
       1: Concepts, definitions and graphical notation. ISO/IEC 15909-1:2004,
       2004.

   [6] ISO/IEC. Software and Systems Engineering - High-level Petri Nets, Part
       1: Concepts, definitions and graphical notation, AMENDMENT 1: Symmetric
       Nets. ISO/IEC 15909-1:2004/Amd.1:2010, 2010.

   [7] F. Kordon, A. Linard, and E. Paviot-Adet. Optimized colored nets
       unfolding. In FORTE, volume 4229 of Lecture Notes in Computer Science, 
           pages 339–355. Springer, 2006.

   [8] ISO/IEC. Software and Systems Engineering - High-level Petri Nets, Part
       2: Transfer format. ISO/IEC 15909-2:2011, 2011.

   [9] L. M. Hillah, E. Kindler, F. Kordon, L. Petrucci, and N. Trèves. A
       primer on the Petri Net Markup Language and ISO/IEC 15909-2. Petri Net
       Newsletter, 76:9–28, Oct. 2009.