A Polynomial-Time Algorithm for Detection of Uncovered Transitions in a Petri Net-Based Concurrent System
This paper introduces a novel algorithm for the efficient verification of a Petri net-based concurrent control system. The proposed method is based on the computation of transition invariant coverage to detect possible errors in the modelled system. Transition invariants play a crucial role in ensur...
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2025-01-01
|
| Series: | Applied Sciences |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2076-3417/15/2/680 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832589244443394048 |
|---|---|
| author | Marcin Wojnakowski Maxim Maliński Remigiusz Wiśniewski Andrzej Obuchowicz Zhiwu Li Dawid Konarczak |
| author_facet | Marcin Wojnakowski Maxim Maliński Remigiusz Wiśniewski Andrzej Obuchowicz Zhiwu Li Dawid Konarczak |
| author_sort | Marcin Wojnakowski |
| collection | DOAJ |
| description | This paper introduces a novel algorithm for the efficient verification of a Petri net-based concurrent control system. The proposed method is based on the computation of transition invariant coverage to detect possible errors in the modelled system. Transition invariants play a crucial role in ensuring the correctness and reliability of such systems; however, existing methods often struggle with high computational demand, especially in the case of large and complex systems. The proposed approach addresses this challenge by performing a fast polynomial-time analysis to identify uncovered transitions, thereby streamlining the verification process. The effectiveness and efficiency of the proposed technique is verified experimentally with a set of 386 test modules (benchmarks) and compared against two well-known established methods: the classical method proposed by Martínez–Silva (as a reference algorithm) and PIPE (Platform Independent Petri Net Editor) tool. The results of the experiments confirm high performance of the presented algorithm, which was able to compute results for all the tested cases. In contrast, both the reference algorithm as well as the PIPE tool failed to deliver results for all examined models within one hour. The proposed algorithm is especially useful in early design stages, offering system designers timely insights into potential issues. |
| format | Article |
| id | doaj-art-287bc9359f624ceb99f01892084a77a5 |
| institution | Kabale University |
| issn | 2076-3417 |
| language | English |
| publishDate | 2025-01-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Applied Sciences |
| spelling | doaj-art-287bc9359f624ceb99f01892084a77a52025-01-24T13:20:25ZengMDPI AGApplied Sciences2076-34172025-01-0115268010.3390/app15020680A Polynomial-Time Algorithm for Detection of Uncovered Transitions in a Petri Net-Based Concurrent SystemMarcin Wojnakowski0Maxim Maliński1Remigiusz Wiśniewski2Andrzej Obuchowicz3Zhiwu Li4Dawid Konarczak5Institute of Control and Computation Engineering, University of Zielona Góra, ul. prof. Z. Szafrana 2, 65-516 Zielona Góra, PolandDoctoral School of Exact and Technical Sciences, University of Zielona Góra, al. Wojska Polskiego 69, 65-762 Zielona Góra, PolandInstitute of Control and Computation Engineering, University of Zielona Góra, ul. prof. Z. Szafrana 2, 65-516 Zielona Góra, PolandInstitute of Control and Computation Engineering, University of Zielona Góra, ul. prof. Z. Szafrana 2, 65-516 Zielona Góra, PolandInstitute of Systems Engineering, University of Science and Technology, Taipa, Macau, ChinaComputer Centre, University of Zielona Góra, ul. Podgórna 50a, 65-246 Zielona Góra, PolandThis paper introduces a novel algorithm for the efficient verification of a Petri net-based concurrent control system. The proposed method is based on the computation of transition invariant coverage to detect possible errors in the modelled system. Transition invariants play a crucial role in ensuring the correctness and reliability of such systems; however, existing methods often struggle with high computational demand, especially in the case of large and complex systems. The proposed approach addresses this challenge by performing a fast polynomial-time analysis to identify uncovered transitions, thereby streamlining the verification process. The effectiveness and efficiency of the proposed technique is verified experimentally with a set of 386 test modules (benchmarks) and compared against two well-known established methods: the classical method proposed by Martínez–Silva (as a reference algorithm) and PIPE (Platform Independent Petri Net Editor) tool. The results of the experiments confirm high performance of the presented algorithm, which was able to compute results for all the tested cases. In contrast, both the reference algorithm as well as the PIPE tool failed to deliver results for all examined models within one hour. The proposed algorithm is especially useful in early design stages, offering system designers timely insights into potential issues.https://www.mdpi.com/2076-3417/15/2/680Petri netspreliminary verificationtransition invariantsconcurrent systemsuncovered transitionsalgorithm |
| spellingShingle | Marcin Wojnakowski Maxim Maliński Remigiusz Wiśniewski Andrzej Obuchowicz Zhiwu Li Dawid Konarczak A Polynomial-Time Algorithm for Detection of Uncovered Transitions in a Petri Net-Based Concurrent System Applied Sciences Petri nets preliminary verification transition invariants concurrent systems uncovered transitions algorithm |
| title | A Polynomial-Time Algorithm for Detection of Uncovered Transitions in a Petri Net-Based Concurrent System |
| title_full | A Polynomial-Time Algorithm for Detection of Uncovered Transitions in a Petri Net-Based Concurrent System |
| title_fullStr | A Polynomial-Time Algorithm for Detection of Uncovered Transitions in a Petri Net-Based Concurrent System |
| title_full_unstemmed | A Polynomial-Time Algorithm for Detection of Uncovered Transitions in a Petri Net-Based Concurrent System |
| title_short | A Polynomial-Time Algorithm for Detection of Uncovered Transitions in a Petri Net-Based Concurrent System |
| title_sort | polynomial time algorithm for detection of uncovered transitions in a petri net based concurrent system |
| topic | Petri nets preliminary verification transition invariants concurrent systems uncovered transitions algorithm |
| url | https://www.mdpi.com/2076-3417/15/2/680 |
| work_keys_str_mv | AT marcinwojnakowski apolynomialtimealgorithmfordetectionofuncoveredtransitionsinapetrinetbasedconcurrentsystem AT maximmalinski apolynomialtimealgorithmfordetectionofuncoveredtransitionsinapetrinetbasedconcurrentsystem AT remigiuszwisniewski apolynomialtimealgorithmfordetectionofuncoveredtransitionsinapetrinetbasedconcurrentsystem AT andrzejobuchowicz apolynomialtimealgorithmfordetectionofuncoveredtransitionsinapetrinetbasedconcurrentsystem AT zhiwuli apolynomialtimealgorithmfordetectionofuncoveredtransitionsinapetrinetbasedconcurrentsystem AT dawidkonarczak apolynomialtimealgorithmfordetectionofuncoveredtransitionsinapetrinetbasedconcurrentsystem AT marcinwojnakowski polynomialtimealgorithmfordetectionofuncoveredtransitionsinapetrinetbasedconcurrentsystem AT maximmalinski polynomialtimealgorithmfordetectionofuncoveredtransitionsinapetrinetbasedconcurrentsystem AT remigiuszwisniewski polynomialtimealgorithmfordetectionofuncoveredtransitionsinapetrinetbasedconcurrentsystem AT andrzejobuchowicz polynomialtimealgorithmfordetectionofuncoveredtransitionsinapetrinetbasedconcurrentsystem AT zhiwuli polynomialtimealgorithmfordetectionofuncoveredtransitionsinapetrinetbasedconcurrentsystem AT dawidkonarczak polynomialtimealgorithmfordetectionofuncoveredtransitionsinapetrinetbasedconcurrentsystem |