A Polynomial-Time Algorithm for Detecting Potentially Unbounded Places in a Petri Net-Based Concurrent System

This paper deals with the preliminary verification of the Petri net-based concurrent system. In particular, a novel algorithm aimed at the identification of the potentially unbounded places in a system is proposed. The idea is based on the structural analysis of the system, and it involves the linear algebra technique. Contrary to the most popular techniques, which are exponential in the general case, the proposed algorithm is bounded by a polynomial with the number of places and transitions of a Petri net. The efficiency and effectiveness of the presented solution were examined through the experimental setup performed on 247 test cases (benchmarks). The obtained results were compared with the most popular Petri net-oriented tools, such as GreatSPN and PIPE.