TY - GEN
T1 - Efficiency and Effectiveness Analysis of Invariant Coverage Verification Methods for Petri net-based Concurrent Systems
AU - Wojnakowski, M.
AU - Wisniewski, R.
AU - Zhou, M.
AU - Li, Z.
AU - Malinski, M.
AU - Obuchowicz, A.
AU - Konarczak, D.
N1 - Publisher Copyright:
© 2025 IEEE.
PY - 2025
Y1 - 2025
N2 - This work aims to analyze the efficiency and effectiveness of two invariant coverage verification methods for Petri net-based concurrent systems. The first algorithm is based on the classical approach, where the complete analysis of a Petri net's incidence matrix is performed. This technique assures the correctness of results, but it may be inefficient due to the exponential computational complexity. The second algorithm applies an innovative idea of a Petri net's incidence matrix transformation and examination. The main advantage of such an approach is its polynomial computational complexity. On the other hand, the method may not always be accurate and may not detect all errors in the examined system. This paper exhaustively verifies the efficiency (run-time) and effectiveness (correctness of the achieved results) of both methods. The theoretical analysis resutls are supported by the experimental ones via 386 benchmarks (Petri net models). In addition, besides the examination of the run-time of both methods, the number of iterations performed by them is computed and analysed.
AB - This work aims to analyze the efficiency and effectiveness of two invariant coverage verification methods for Petri net-based concurrent systems. The first algorithm is based on the classical approach, where the complete analysis of a Petri net's incidence matrix is performed. This technique assures the correctness of results, but it may be inefficient due to the exponential computational complexity. The second algorithm applies an innovative idea of a Petri net's incidence matrix transformation and examination. The main advantage of such an approach is its polynomial computational complexity. On the other hand, the method may not always be accurate and may not detect all errors in the examined system. This paper exhaustively verifies the efficiency (run-time) and effectiveness (correctness of the achieved results) of both methods. The theoretical analysis resutls are supported by the experimental ones via 386 benchmarks (Petri net models). In addition, besides the examination of the run-time of both methods, the number of iterations performed by them is computed and analysed.
UR - https://www.scopus.com/pages/publications/105033158119
UR - https://www.scopus.com/pages/publications/105033158119#tab=citedBy
U2 - 10.1109/SMC58881.2025.11342612
DO - 10.1109/SMC58881.2025.11342612
M3 - Conference contribution
AN - SCOPUS:105033158119
T3 - Conference Proceedings - IEEE International Conference on Systems, Man and Cybernetics
SP - 1190
EP - 1195
BT - 2025 IEEE International Conference on Systems, Man, and Cybernetics
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 2025 IEEE International Conference on Systems, Man, and Cybernetics, SMC 2025
Y2 - 5 October 2025 through 8 October 2025
ER -