论文标题
MCC：以PNML格式展开彩色培养皿网的工具
MCC: a Tool for Unfolding Colored Petri Nets in PNML Format
论文作者
论文摘要
MCC是一种针对非常特定的任务设计的工具：将PNML语法中给出的高级Petri网的模型转换为等效的位置/过渡网。该工具的名称源自年度模型检查竞赛，这是模型检查工具的竞赛，可提供大量多样的PNML模型。这种命名选择的选择强调了该工具的主要重点，该工具提供了一个开放有效的解决方案，可降低想要参与这项竞争的开发人员的访问成本。我们描述了工具的架构和功能，并展示了它与其他现有解决方案的比较。尽管我们针对的问题在文献中得到了很多涵盖，但我们表明仍然有可能进行创新。为了证实这一主张，我们特别强调了MCC的两个独特特征，这些特征在处理比赛中一些最具挑战性的有色模型时被证明有用，即使用有限的高级不变性概念，并支持Petri Net scripsing语言。
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.
