A Polynomial-Time Algorithm for Detection of Uncovered Transitions in a Petri Net-Based Concurrent System
We propose a novel polynomial-time algorithm for detecting uncovered transitions in Petri net-based concurrent systems. The method leverages transition invariants to verify system correctness efficiently, even in large models. Experimental results on 386 benchmarks show that our algorithm significantly outperforms existing approaches in both speed and completeness. This solution is particularly useful during early design stages of control systems.
Jan 9, 2025