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

Models

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 NamePN ClassIntroduced inArchive (PNML)
CSRepetitionsColored +
equivalent P/T
MCC’2012CSRepetitions.bz2
DekkerP/TMCC’2013Dekker.bz2
DotAndBoxesColoredMCC’2013DotAndBoxes.bz2
DrinkVendingMachineColored +
equivalent P/T
MCC’2013DrinkVendingMachine.bz2
EchoP/TMCC’2012Echo.bz2
EratosthenesP/TMCC’2012Eratosthenes.bz2
FMSP/TMCC’2011FMS.bz2
GlobalRessAllocColored +
equivalent P/T
MCC’2012GlobalRessAlloc.bz2
HouseConstructionP/TMCC’2013 - surpriseHouseConstruction.bz2
IBMB2S565S3960P/TMCC’2013 - surpriseIBMB2S565S3960.bz2
KanbanP/TMCC’2011Kanban.bz2
LamportFastMutExColored +
equivalent P/T
MCC’2012LamportFastMutEx.bz2
MAPKP/TMCC’2011MAPK.bz2
NeoElectionColored +
equivalent P/T
MCC’2012NeoElection.bz2
PermAdmissibilityColored +
equivalent P/T
MCC’2013PermAdmissibility.bz2
PetersonColored +
equivalent P/T
MCC’2011Peterson.bz2
PhilosophersColored +
equivalent P/T
MCC’2011Philosophers.bz2
PhilosophersDynColored +
equivalent P/T
MCC’2012PhilosophersDyn.bz2
PlanningP/TMCC’2012Planning.bz2
QuasiCertifProtocol Colored +
equivalent P/T
MCC’2013 - surpriseQuasiCertifProtocol.bz2
RailroadP/TMCC’2012Railroad.bz2
RessAllocationP/TMCC’2013RessAllocation.bz2
RingP/TMCC’2012Ring.bz2
RwMutexP/TMCC’2012RwMutex.bz2
SharedMemoryColored +
equivalent P/T
MCC’2011SharedMemory.bz2
SimpleLoadBalColored +
equivalent P/T
MCC’2012SimpleLoadBal.bz2
TokenRingColored +
equivalent P/T
MCC’2011TokenRing.bz2
Vasy2003P/TMCC’2013 - surprise Vasy2003.bz2