Introduction

The benchmark proposed for the MCC'2014 consists of P/T nets (1-bounded, k-bounded), and colored Nets (1 and k-bounded per color, with and without non-equal guards on transitions, with and without cartesian product on colors, with and without successor/predecessor functions). For colored Petri Nets, equivalent nets are provided in most of the cases.

Two classes of models will be provided:

• Academic models: these where designed in universities by researcher, to benchmark some tools, to illustrate a typical situation or within the context of academic projects and cooperations,
• Industrial models: these where designed within the context of industrial projects.

All models will be provided as PNML files. The two types of models will be provided with a detailed set of characteristics that tools can exploit when possible.

Models (both academic and industrial) are separated in two categories:

• «Known» models that groups the models presented in 2011, 2012 and 2013 and will be provided when the call for tool submission is out,
• «Surprise» models that groups the models submitted by the community and then selected for 2014.

Model Contributors

The section below list the people who provided models to the various editions of the Model Checking Contest. Sometime, they are authors of these models, otherwise, they have summarized or retrieved an existing model from the literature... thus, since hey champion these models, they are "responsible" for them and, since they were of great help for establishing the base of our benchmark, they are listed below:

• B. Barbot (ENS de Cachan, France): DatabaseWithMutex (surprise)
• J. Ezpeleta & F. Tricas García (Univ. Zaragoza, Spain): ResAllocation
• S. Evangelista (Univ. Paris 13, France): LamportFastMutEx, NeoElection, SimpleLoadBal
• H. Evrard and F. Lang (Inria, France): MultiwaySync (surprise)
• H. Garavel (Inria, France): Vasy2003
• H. Garavel and W. Serwe (Inria, France): ProductionCell (surprise)
• A. Graf-Brill (Univ. Saarland, Germany): EnergyBus (surprise)
• M. Heiner (Univ Cottbus, Germany): Diffusion2D (surprise), ParamProductionCell (surprise), Solitaire (surprise)
• L. Hillah (Univ. Paris Ouest Nanterre): DrinkVendingMachine, FMS, Kanban, MAPK, Philosopher, SharedMemory
• F. Kordon (Univ. P. & M. Curie, France): GlobalResAlloc, HouseConstruction, PermAdmissibility, QuasiCertifProtocol, CircularTrains (surprise), PolyORBLF (surprise), PolyORBNT (surprise)
• A. Kriouile and W. Serwe (ST and Inria, France): ARMCacheCoherence (surprise)
• A. Linard (ENS de Cachan, France): CSRepetition, PhilosophersDyn
• N. Lohmann (Univ. Rostock, Germany): Echo, IBMB2S565S3960, Planning, Ring, RwMutex
• A. Marechal (Univ. Geneva, Switzerland): TokenRing
• E. Paviot-Adet (Univ. René Descartes, France): DotAndBoxes, Peterson
• F. Pommereau (Univ. Evry Val d'Essone, France): Eratosthenes, Railroad
• C. Rodríguez (ENS de Cachan, France): Dekker
• C Rohr (Univ. Cottbus, Germany): Angiogenesis (surprise), CircadianClock (surprise), ERK (surprise)
• Z. Zhang and W. Serwe (Univ. Utah, USA): UtahNoC (surprise)

«Known» Models for 2014

The table below summarizes the «Known» models which has been enriched over the years during the past editions of the Model Checking Contest.

Name	PN Type	Scale Parameter(s)	Data on the Model	form	PNML
Proposed in 2013 (9 models)
Dekker A variant of Dekker's algorithm for mutual exclusion, proposed by Cesar Rodriguez A Place-Transition net representing a variant of the Dekker's mutual exclusion algorithm for N > 2 processes.	P/T	Yes	Places: 3*N, Transitions: N2+2*N, Arcs: O(N2)
DotAndBoxes Dot&Boxes, proposed by Emmanuel Paviot-Adet This Petri net models the Dot & Boxes game.	Colored	Yes	Places: 8, Transitions: 8, Arcs: 44
DrinkVendingMachine A hot drink vending machine, proposed by Lom Messan Hillah This net models a simple hot drink vending machine.	Colored + P/T equiv	Yes	Places: 6, Transitions: 7, Arcs: 28
HouseConstruction HouseConstruction, proposed by Fabrice Kordon This net models the construction of a house (seen as a workflow).	P/T	Yes	Places: 26, Transitions: 18, Arcs: 51
IBMB2S565S3960 IBMB2S565S3960, proposed by Niels Lohmann This net models a huge workflow structure derived from a problem described by IBM.	P/T	None	Places: 273, Transitions: 179, Arcs: 572
PermAdmissibility Permutation admissibility in multistage interconnection networks, proposed by Fabrice Kordon The model describes the possible permutations on a 8x8 4 stages shuffle-exchange network.	Colored + P/T equiv	Yes	Places: 40, Transitions: 16, Arcs: 83
QuasiCertifProtocol Quasi Certification Protocol over a DHT, proposed by Fabrice Kordon This net net models a quasi certification protocol on top of a Distributed Hash Table.	Colored + P/T equiv	Yes	Places: 30, Transitions: 26, Arcs: 77
ResAllocation Resource Allocation Model, proposed by Fernando Tricas Garcia and Joaquin Ezpeleta Mateo This net models a family of Resource Allocation Systems.	P/T	Yes	Places: 2 ... nR ... nC, Transitions: nC ... (nR+1), Arcs: 4 ... nR ... nC + 2 ... nR ... (nC-1)
Vasy2003 Vasy2003, proposed by Hubert Garavel This net is extracted from a benchmark sent on July 2003 and derived from a program described by means of: 8.5KLOC of LOTOS + 3KLOC of C.	P/T	None	Places: 485, Transitions: 776, Arcs: 2809
Proposed in 2012 (12 models)
CSRepetitions Client/Server with Repetitions, proposed by Alban Linard This Petri net models a client/server application where communication from clients to servers is not reliable and requests stored in a buffer of a given size.	Colored + P/T equiv	Yes	Places: 1 + 3*clients + servers + clients*servers, Transitions: 3*clients + 2*clients*servers, Arcs: 7*clients + 8*clients+servers
Echo Echo Algorithm, proposed by Niels Lohmann This net models the Echo Algorithm defined by Reisig in 1998.	P/T	Yes	For value (3,3) Places: 265, Transitions: 206, Arcs: 1252
Eratosthenes Eratosthenes' sieve, proposed by Franck Pommereau This model describes an Eratosthenes' sieve.	P/T	Yes	For value 500 Places: 499, Transitions: 2191, Arcs: 6573
GlobalResAllocation Global Allocation Resource Management, proposed by Fabrice Kordon This net models a resource management strategy that prevents deadlocks.	Colored + P/T equiv	Yes	Places: 5, Transitions: 8, Arcs: 29
LamportFastMutEx Lamport's fast mutual exclusion algorithm, proposed by Sami Evangelista This net models Lamport's fast mutual exclusion algorithm designed for multi-processor architectures with a shared memory.	Colored + P/T equiv	Yes	Places: 18, Transitions: 17, Arcs: 68
NeoElection Neo election protocol, proposed by Sami Evangelista This net models an election protocol between the master nodes of a distributed database designed by Nexedi.	Colored + P/T equiv	Yes	For value N=2 Places: 18, Transitions: 22, Arcs: 98
PhilosophersDyn Dynamic Philosophers, proposed by Alban Linard This net models a variation of the Dining Philosophers problem where philosophers can join or leave the table.	Colored + P/T equiv	Yes	Places: N2 + 7N, Transitions: 2*N3 + 3*N2 + N, Arcs: unknown
Planning AI Planning, proposed by Niels Lohmann This net models the equipment (displays, canvases, documents, and lamps) of a smart conference room of the University of Rostock.	P/T	None	Places: 126, Transitions: 128, Arcs: 652
Railroad Railroad crossing, proposed by Franck Pommereau This net models the Petri nets semantics of an ABCD specification of a railroad crossing system	P/T	Yes	Places: 5*n + 18, Transitions: 3*n + 10, Arcs: 13*n + 52
Ring Three-Module Ring, proposed by Niels Lohmann This net is derived from an example of hardware circuit.	P/T	None	Places: 139, Transitions: 87, Arcs: 410
RwMutex Reader/Writer Mutual Exclusion, proposed by Niels Lohmann The net models a system with readers and writers.	P/T	Yes	For value (10,10) Places: 50, Transitions: 40, Arcs: 300
SimpleLoadBal Simple load balancing system, proposed by Sami Evangelista This net models simple load balancing system composed of a set of clients, two servers supervised by a load balancer process.	Colored + P/T equiv	Yes	Places: 14, Transitions: 13, Arcs: 57
Proposed in 2011 (7 models)
FMS Flexible Manufacturing System (FMS), proposed by Lom-Messan Hillah This Net, extracted from the SMART benchmark, models a flexible manufacturing system.	P/T	Yes	Places: 22, Transitions: 20, Arcs: 50
Kanban Kanban, proposed by Lom-Messan Hillah This net, extracted from the SMART benchmark, models a kanban system.	P/T	Yes	Places: 16, Transitions: 16, Arcs: 40
MAPK MAPK, proposed by Lom-Messan Hillah This net models a biochemical reaction: Mitogen-activated protein kinase kaskade.	P/T	Yes	Places: 22, Transitions: 30, Arcs: 90
Peterson Peterson, proposed by Emmanuel Paviot-Adet This net models the Peterson's algorithm for the mutual exclusion problem, in its generalized version for N processes	Colored + P/T equiv	Yes	Places: 11, Transitions: 14, Arcs: 42
Philosophers Philosophers, proposed by Lom-Messan Hillah This net models the famous dining philosophers problem.	Colored + P/T equiv	Yes	Places: 4, Transitions: 5, Arcs: 15
SharedMemory SharedMemory, proposed by Lom-Messan Hillah This model, extracted from a greatSPN benchmark, models a sort of COMA (Cache Only Memory Access) system with P processors, each one having its local memory.	Colored + P/T equiv	Yes	Places: 6, Transitions: 5, Arcs: 16
TokenRing Token Ring, proposed by Alexis Marechal This net models a token ring-based system.	Colored + P/T equiv	Yes	Places: 1, Transitions: 2, Arcs: 4

«Surprise» Models for 2014

The «Surprise» models are the ones proposed by the community during the call for model phase of the 2014 edition.

We are happy to announce that there will be 15 new «surprise» models for 2014 (138 instances in total).

Name	PN Type	Scale Parameter(s)	Data on the Model	form	PNML
ARMCacheCoherence ARMCacheCoherency, proposed by Abderahman Kriouile and Wendelin Serwe This model is derived from a Lotos specification specifying the ACE specification from ARM that is a standard in cache coherence of heterogeneous systems on chip.	P/T	None	Places: 87, Transitions: 33676, Arcs: 246935
Angiogenesis Angiogenesis, proposed by Christian Rohr This Petri net models the formation of new vessels from the existing ones, is a topic of great interest in all areas of human biology.	P/T	Yes	Places: 39, Transitions: 64, Arcs: 185
CircadianClock CircadianClock, proposed by Christian Rohr This Petri net models circadian rhythms which are widely used in organisms to keep a sense of daily time.	P/T	Yes	Places: 14, Transitions: 16, Arcs: 58
CircularTrains Circular Trains, proposed by Fabrice Kordon A Place-Transition net representing a circular railways os S sections where S/3 trains circulate.	P/T	Yes	Places: 2*S, Transitions: S, Arcs: 4*S
DatabaseWithMutex DatabaseWithMutex, proposed by Benoît Barbot This model is an extension of the well-known distributed database example adds atomic transitions and global mutex for each file.	Colored + P/T equiv	None	Places: 11, Transitions: 8, Arcs: 22
Diffusion2D Diffusion2D, proposed by Monika Heiner This Petri net models diffusion in space, a process underlying many spatial (bio-) chemical processes.	P/T	Yes	Places: D2, Transitions: 8xD2 - 12xD + 4, Arcs: 2 ... |T|
ERK ERK, proposed by Christian Rohr This is the model of the "RKIP/MEK-ERK signalling pathway" (published in 2003).	P/T	Yes	Places: 11, Transitions: 11, Arcs: 34
EnergyBus EnergyBus, proposed by Alexander Graf-Brill This model derives from a Lotos specification modeling the EnergyBus, an upcoming industrial standard for electric power transmission and management, based on the CANopen field bus.	P/T	None	Places: 157, Transitions: 4430, Arcs: 63389
MultiwaySync MultiwaySync, proposed by Hugues Evrard and Frédéric Lang This model derives from a LOTOS specification of a multiway synchronization protocol.	P/T	None	Places: 222, Transitions: 472, Arcs: 1496
ParamProductionCell ParamProductionCell, proposed by Monika Heiner This Petri net models the "production cell", introduced in 1995 as a case study to compare different formal methods with respect to their modeling and analysis features.	P/T	Yes	Places: 198-231, Transitions: 176-202, Arcs: 730-846
PolyORBLF PolyORBLF, proposed by Fabrice Kordon This Petri nets models the microBroker component in the PolyORB middleware in its "leader-follower" implementation.	Colored + P/T equiv	Yes	Places: 81, Transitions: 65, Arcs: 258
PolyORBNT PolyORBNT, proposed by Fabrice Kordon This Petri nets models the microBroker component in the PolyORB middleware in its "no-thread" implementation.	Colored + P/T equiv	Yes	Places: 48, Transitions: 38, Arcs: 140
ProductionCell ProductionCell, proposed by Hubert Garavel and Wendelin Serwe This model derives from a LOTOS specification of a case study introduced in 1995 to assess various formal methods on one common example.	P/T	None	Places: 176, Transitions: 134, Arcs: 513
Solitaire Solitaire, proposed by Monika Heiner This Petri net models the solitaire, that is a popular board game requiring non-obvious solution strategies.	P/T	Yes	Places: 50-75, Transitions: 84-92, Arcs: 456-644
UtahNoC UtahNoc, proposed by Zhen Zhang and Wendelin Serwe This Petri net is derived from a LOTOS specification of a fault-tolerant wormhole routing algorithm for an asynchronous on-chip network communication.	P/T	None	Places: 216, Transitions: 977, Arcs: 2905