Unfolding colored Petri nets into place/transition (P/T) nets is a standard approach for model-checking, leveraging established tools and techniques for basic Petri nets. However, the unfolding process often leads to a combinatorial explosion in the number of places and transitions, creating a significant bottleneck in analyzing complex colored Petri nets. We introduce a new verification engine for Petri nets with finite color domains that bypasses the costly unfolding process. Our engine employs an explicit, on-the-fly state-space exploration, utilizing an optimized binding generator and linear programming-based approximation techniques to enhance performance. Integrated into the open-source TAPAAL model checker, our engine is evaluated on an extensive benchmark from the Model Checking Contest (MCC) 2024. It demonstrates superior performance over the state-of-the-art unfolding approaches.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Explicit Model Checking Engine for Reachability Analysis of Colored Petri Nets

  • Emil Normann Brandt,
  • Jens Emil Fink Højriis,
  • Kira Stæhr Pedersen,
  • Jiří Srba

摘要

Unfolding colored Petri nets into place/transition (P/T) nets is a standard approach for model-checking, leveraging established tools and techniques for basic Petri nets. However, the unfolding process often leads to a combinatorial explosion in the number of places and transitions, creating a significant bottleneck in analyzing complex colored Petri nets. We introduce a new verification engine for Petri nets with finite color domains that bypasses the costly unfolding process. Our engine employs an explicit, on-the-fly state-space exploration, utilizing an optimized binding generator and linear programming-based approximation techniques to enhance performance. Integrated into the open-source TAPAAL model checker, our engine is evaluated on an extensive benchmark from the Model Checking Contest (MCC) 2024. It demonstrates superior performance over the state-of-the-art unfolding approaches.