Explicit Model Checking Engine for Reachability Analysis of Colored Petri Nets
摘要
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.