Petri Nets

Here are the Petri Net benchmarks. They have been elaborated in the context of the Model Checking Contest @ Petri net since 2011 and contain contributions from the Petri net Community. Even if they often refer to well known problems or their variants, the models of these benchmarks have been proposed by colleagues coming from the following institutions:

  • École Normale Supérieure de Cachan
  • Universidad de Zaragoza
  • Universität Rostock
  • Université d’Evry Val d’Essone
  • Université Geneva
  • Université Paris 13
  • Université Pierre & Marie Curie


You can get from this page the models for your usage. However, the full archive, as well as a disk image with a virtual machine that can be operated with BenchKit are available on the Model Checking Contest @ Petri Nets web site.

These models (except planning and ring) exist for several values of one (sometimes two) scaling parameter. Colored models also exist in their P/T equivalent form.

Model Name PN Class Introduced in Archive (PNML)
CSRepetitions Colored +
equivalent P/T
MCC’2012 CSRepetitions.bz2
Dekker P/T MCC’2013 Dekker.bz2
DotAndBoxes Colored MCC’2013 DotAndBoxes.bz2
DrinkVendingMachine Colored +
equivalent P/T
MCC’2013 DrinkVendingMachine.bz2
Echo P/T MCC’2012 Echo.bz2
Eratosthenes P/T MCC’2012 Eratosthenes.bz2
FMS P/T MCC’2011 FMS.bz2
GlobalRessAlloc Colored +
equivalent P/T
MCC’2012 GlobalRessAlloc.bz2
HouseConstruction P/T MCC’2013 - surprise HouseConstruction.bz2
IBMB2S565S3960 P/T MCC’2013 - surprise IBMB2S565S3960.bz2
Kanban P/T MCC’2011 Kanban.bz2
LamportFastMutEx Colored +
equivalent P/T
MCC’2012 LamportFastMutEx.bz2
MAPK P/T MCC’2011 MAPK.bz2
NeoElection Colored +
equivalent P/T
MCC’2012 NeoElection.bz2
PermAdmissibility Colored +
equivalent P/T
MCC’2013 PermAdmissibility.bz2
Peterson Colored +
equivalent P/T
MCC’2011 Peterson.bz2
Philosophers Colored +
equivalent P/T
MCC’2011 Philosophers.bz2
PhilosophersDyn Colored +
equivalent P/T
MCC’2012 PhilosophersDyn.bz2
Planning P/T MCC’2012 Planning.bz2
QuasiCertifProtocol Colored +
equivalent P/T
MCC’2013 - surprise QuasiCertifProtocol.bz2
Railroad P/T MCC’2012 Railroad.bz2
RessAllocation P/T MCC’2013 RessAllocation.bz2
Ring P/T MCC’2012 Ring.bz2
RwMutex P/T MCC’2012 RwMutex.bz2
SharedMemory Colored +
equivalent P/T
MCC’2011 SharedMemory.bz2
SimpleLoadBal Colored +
equivalent P/T
MCC’2012 SimpleLoadBal.bz2
TokenRing Colored +
equivalent P/T
MCC’2011 TokenRing.bz2
Vasy2003 P/T MCC’2013 - surprise Vasy2003.bz2