Skip to Main content Skip to Navigation
Conference papers

MCC: a Tool for Unfolding Colored Petri Nets in PNML Format

Silvano Dal Zilio 1
1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
LAAS - Laboratoire d'analyse et d'architecture des systèmes
Abstract : MCC is a tool designed for a very specific task: to transform the models of High-Level Petri nets, given in the PNML syntax, into equivalent Place/Transition nets. The name of the tool derives from the annual Model-Checking Contest, a competition of model-checking tools that provides a large and diverse collection of PNML models. This choice in naming serves to underline the main focus of the tool, which is to provide an open and efficient solution that lowers the access cost for developers wanting to engage in this competition. We describe the architecture and functionalities of our tool and show how it compares with other existing solutions. Despite the fact that the problem we target is abundantly covered in the literature, we show that it is still possible to innovate. To substantiate this assertion, we put a particular emphasis on two distinctive features of MCC that have proved useful when dealing with some of the most challenging colored models in the contest, namely the use of a restricted notion of higher-order invariant, and the support of a Petri net scripting language.
Document type :
Conference papers
Complete list of metadata
Contributor : Silvano Dal Zilio <>
Submitted on : Thursday, March 19, 2020 - 10:37:42 AM
Last modification on : Thursday, June 10, 2021 - 3:06:48 AM


Files produced by the author(s)


  • HAL Id : hal-02511881, version 1
  • ARXIV : 2003.09134


Silvano Dal Zilio. MCC: a Tool for Unfolding Colored Petri Nets in PNML Format. 41st International Conference on Application and Theory of Petri Nets and Concurrency, Jun 2020, Paris, France. ⟨hal-02511881⟩



Record views


Files downloads