{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T22:53:03Z","timestamp":1773355983148,"version":"3.50.1"},"reference-count":51,"publisher":"MDPI AG","issue":"3","license":[{"start":{"date-parts":[[2021,2,28]],"date-time":"2021-02-28T00:00:00Z","timestamp":1614470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62002328"],"award-info":[{"award-number":["62002328"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Zhejiang Provincial Natural Science Foundation of China","award":["LQ20F020002"],"award-info":[{"award-number":["LQ20F020002"]}]},{"name":"Key Laboratory of Embedded System and Service Computing (Ministry of Education)","award":["ESSCKF2019\u221202"],"award-info":[{"award-number":["ESSCKF2019\u221202"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Symmetry"],"abstract":"<jats:p>The unfolding technique of Petri net can characterize the real concurrency and alleviate the state space explosion problem. Thus, it is greatly suitable to analyze\/check some potential errors in concurrent systems. During the unfolding process of a Petri net, the calculations of configurations, cuts, and cut-off events are the key factors for the unfolding efficiency. However, most of the unfolding methods do not specify a highly efficient calculations on them. In this paper, we reveal some recursive relations and structural properties of these factors. Subsequently, we propose an improved method for computing configurations and cuts. Meanwhile, backward conflicts are used to guide the calculations of cut-off events. Moreover, a case study and a series of experiments are done to illustrate the effectiveness and application scenarios of our methods.<\/jats:p>","DOI":"10.3390\/sym13030392","type":"journal-article","created":{"date-parts":[[2021,2,28]],"date-time":"2021-02-28T01:51:43Z","timestamp":1614477103000},"page":"392","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["An Incremental and Backward-Conflict Guided Method for Unfolding Petri Nets"],"prefix":"10.3390","volume":"13","author":[{"given":"Dongming","family":"Xiang","sequence":"first","affiliation":[{"name":"The School of Information Science and Technology, Zhejiang Sci-Tech University, Hangzhou 310018, China"}]},{"given":"Xiaoyan","family":"Tao","sequence":"additional","affiliation":[{"name":"MoE Key Lab of Embedded System &amp; Service Computing, Tongji University, Shanghai 201804, China"}]},{"given":"Yaping","family":"Liu","sequence":"additional","affiliation":[{"name":"The School of Transportation Management, Zhejiang Institute of Communications, Hangzhou 310018, China"}]}],"member":"1968","published-online":{"date-parts":[[2021,2,28]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"2024","DOI":"10.1109\/TII.2014.2341933","article-title":"Asynchronous-channels within Petri net-based GALS distributed embedded systems modeling","volume":"10","author":"Moutinho","year":"2014","journal-title":"IEEE Trans. Ind. Inform."},{"key":"ref_2","unstructured":"Zhou, M.C., and Wu, N. (2009). System Modeling and Control with Resource-Oriented Petri Nets, CRC Press, Inc."},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1109\/TITS.2016.2625324","article-title":"A two-level traffic light control strategy for preventing incident-based urban traffic congestion","volume":"19","author":"Qi","year":"2016","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"ref_4","first-page":"231","article-title":"Unfolding based algorithms for the reachability problem","volume":"47","author":"Esparza","year":"2001","journal-title":"Fundam. Inform."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"4104","DOI":"10.1109\/ACCESS.2016.2597061","article-title":"A Branching-process-based method to check soundness of workflow systems","volume":"4","author":"Liu","year":"2016","journal-title":"IEEE Access"},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1016\/j.ins.2017.08.014","article-title":"Deadlock and liveness characterization for a class of generalized Petri nets","volume":"420","author":"Liu","year":"2017","journal-title":"Inf. Sci."},{"key":"ref_7","unstructured":"Franco, A., and Baldan, P. (2015). True Concurrency and Atomicity: A Model Checking Approach with Contextual Petri Nets, LAP LAMBERT Academic Publishing."},{"key":"ref_8","doi-asserted-by":"crossref","unstructured":"McMillan, K.L. (1992). Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. Computer Aided Verification, Springer.","DOI":"10.1007\/3-540-56496-9_14"},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1023\/A:1020321222420","article-title":"Hierarchical Reachability Graph Generation for Petri Nets","volume":"21","author":"Buchholz","year":"2002","journal-title":"Form. Methods Syst. Des."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1109\/TCST.2017.2692204","article-title":"Prototyping of Concurrent Control Systems with Application of Petri Nets and Comparability Graphs","volume":"26","author":"Wisniewski","year":"2017","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"13510","DOI":"10.1109\/ACCESS.2019.2893284","article-title":"C-exact hypergraphs in concurrency and sequentiality analyses of cyber-physical systems specified by safe Petri nets","volume":"7","author":"Jarnut","year":"2019","journal-title":"IEEE Access"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1016\/j.tcs.2014.07.003","article-title":"Recent advances in unfolding technique","volume":"551","author":"Bonet","year":"2014","journal-title":"Theor. Comput. Sci."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1023\/A:1014746130920","article-title":"An improvement of McMillan\u2019s unfolding algorithm","volume":"20","author":"Esparza","year":"2002","journal-title":"Form. Methods Syst. Des."},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/s00236-006-0023-y","article-title":"Merged processes: A new condensed representation of Petri net behaviour","volume":"43","author":"Khomenko","year":"2006","journal-title":"Acta Inform."},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Bonet, B., Haslum, P., Hickmott, S., and Thi\u00e9baux, S. (2008). Directed unfolding of petri nets. Transactions on Petri Nets and Other Models of Concurrency I, Springer.","DOI":"10.1007\/978-3-540-89287-8_11"},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"2310","DOI":"10.1109\/TAC.2010.2063490","article-title":"Types of asynchronous diagnosability and the reveals-relation in occurrence nets","volume":"55","author":"Haar","year":"2010","journal-title":"IEEE Trans. Autom. Control"},{"key":"ref_17","unstructured":"Hickmott, S.L., Rintanen, J., Thi\u00e9baux, S., and White, L.B. (2007, January 6\u201312). Planning via Petri Net Unfolding. Proceedings of the International Joint Conference on Artificial Intelligence, Hyderabad, India."},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Leon, H.P.d., Saarikivi, O., Kahkonen, K., Heljanko, K., and Esparza, J. (2015, January 21\u201326). Unfolding Based Minimal Test Suites for Testing Multithreaded Programs. Proceedings of the 15th International Conference on Application of Concurrency to System Design, Brussels, Belgium.","DOI":"10.1109\/ACSD.2015.12"},{"key":"ref_19","first-page":"371","article-title":"Parallelisation of the Petri net unfolding algorithm","volume":"Volume 2280","author":"Heljanko","year":"2002","journal-title":"Proceedings of the 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), LNCS"},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Khomenko, V., and Mokhov, A. (2011, January 24\u201325). An algorithm for direct construction of complete merged processes. Proceedings of the International Conference on Application and Theory of Petri Nets and Concurrency, Paris, France.","DOI":"10.1007\/978-3-642-21834-7_6"},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"31","DOI":"10.3233\/FI-2013-782","article-title":"Branching processes of general Petri nets","volume":"122","author":"Couvreur","year":"2013","journal-title":"Fundam. Inform."},{"key":"ref_22","unstructured":"Rodr\u00edguez, C., Sousa, M., Sharma, S., and Kroening, D. (2015, January 1\u20134). Unfolding-based Partial Order Reduction. Proceedings of the 26th International Conference on Concurrency Theory (CONCUR 2015), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Madrid, Spain."},{"key":"ref_23","unstructured":"Chatain, T., and Paulev\u00e9, L. (2017, January 5\u20138). Goal-Driven Unfolding of Petri Nets. Proceedings of the 28th International Conference on Concurrency Theory (CONCUR 2017), Berlin, Germany."},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ins.2019.05.021","article-title":"Deadlock detection-oriented unfolding of unbounded Petri nets","volume":"497","author":"Lu","year":"2019","journal-title":"Inf. Sci."},{"key":"ref_25","unstructured":"Jiroveanu, G., Boel, R.K., and Schutter, B.D. (2006, January 10\u201312). Fault Diagnosis for Time Petri Nets. Proceedings of the International Workshop on Discrete Event Systems, Ann Arbor, MI, USA."},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Chatain, T., and Fabre, E. (2010, January 21\u201325). Factorization Properties of Symbolic Unfoldings of Colored Petri Nets. Proceedings of the International Conference on Applications & Theory of Petri Nets, Braga, Portugal.","DOI":"10.1007\/978-3-642-13675-7_11"},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Rodriguez, C., Schwoon, S., and Baldan, P. (2011, January 6\u20139). Efficient Contextual Unfolding. Proceedings of the International Conference on Concurrency Theory, Aachen, Germany.","DOI":"10.1007\/978-3-642-23217-6_23"},{"key":"ref_28","unstructured":"Lomazova, I.A., and Ermakova, V.O. (2016, January 20\u201321). Verication of Nested Petri Nets Using an Unfolding Approach. Proceedings of the International Workshop on Petri Nets & Software Engineering, Torun, Poland."},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Khomenko, V., and Koutny, M. (2000, January 22\u201325). LP deadlock checking using partial order dependencies. Proceedings of the International Conference on Concurrency Theory, State College, PA, USA.","DOI":"10.1007\/3-540-44618-4_30"},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Rodriguez, C., and Schwoon, S. (2012, January 4\u20137). Verification of Petri nets with read arcs. Proceedings of the International Conference on Concurrency Theory, Newcastle, UK.","DOI":"10.1007\/978-3-642-32940-1_33"},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/s10009-014-0353-y","article-title":"Model-based testing for concurrent systems: Unfolding-based test selection","volume":"18","author":"Haar","year":"2016","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"Jezequel, L., Madalinski, A., and Schwoon, S. (June, January 30). Distributed computation of vector clocks in Petri nets unfolding for test selection. Proceedings of the Workshop on Discrete Event Systems (WODES), Sorrento Coast, Italy.","DOI":"10.1007\/s10626-020-00310-4"},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"K\u00e4hk\u00f6nen, K., Saarikivi, O., and Heljanko, K. (2012, January 3\u20137). Using unfoldings in automated testing of multithreaded programs. Proceedings of the 27th IEEE\/ACM International Conference on Automated Software Engineering, Essen, Germany.","DOI":"10.1145\/2351676.2351698"},{"key":"ref_34","first-page":"45","article-title":"Minimizing test suites with unfoldings of multithreaded programs","volume":"16","author":"Saarikivi","year":"2017","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"1964","DOI":"10.1109\/TASE.2018.2830385","article-title":"Stability Analysis of Discrete Event Systems Modeled by Petri Nets Using Unfoldings","volume":"15","year":"2018","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"439","DOI":"10.3233\/FI-2009-138","article-title":"A practical approach to verification of mobile systems using net unfoldings","volume":"94","author":"Meyer","year":"2009","journal-title":"Fundam. Inform."},{"key":"ref_37","doi-asserted-by":"crossref","unstructured":"Ponce-de Le\u00f3n, H., Rodr\u00edguez, C., Carmona, J., Heljanko, K., and Haar, S. (2015, January 12\u201315). Unfolding-based process discovery. Proceedings of the International Symposium on Automated Technology for Verification and Analysis, Shanghai, China.","DOI":"10.1007\/978-3-319-24953-7_4"},{"key":"ref_38","doi-asserted-by":"crossref","unstructured":"Weidlich, M., Elliger, F., and Weske, M. (2010, January 16\u201317). Generalised computation of behavioural profiles based on petri-net unfoldings. Proceedings of the International Workshop on Web Services and Formal Methods, Hoboken, NJ, USA.","DOI":"10.1007\/978-3-642-19589-1_7"},{"key":"ref_39","doi-asserted-by":"crossref","first-page":"2995","DOI":"10.1109\/TII.2017.2698640","article-title":"Detecting data inconsistency based on the unfolding technique of petri nets","volume":"13","author":"Xiang","year":"2017","journal-title":"IEEE Trans. Ind. Inform."},{"key":"ref_40","unstructured":"R\u00f6mer, S. (2000). Theorie und Praxis der Netzentfaltungen als Grundlage F\u00fcr die Verifikation Nebenl\u00e4ufiger Systeme. [Ph.D. Thesis, Technical University]."},{"key":"ref_41","doi-asserted-by":"crossref","unstructured":"Dong, L., Liu, G., and Xiang, D. (2018, January 9\u201311). Verifying CTL with Unfoldings of Petri Nets. Proceedings of the International Conference on Algorithms and Architectures for Parallel Processing, Melbourne, Australia.","DOI":"10.1007\/978-3-030-05063-4_5"},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"43265","DOI":"10.1109\/ACCESS.2020.2976124","article-title":"Petri net based data-flow error detection and correction strategy for business processes","volume":"8","author":"Liu","year":"2020","journal-title":"IEEE Access"},{"key":"ref_43","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1109\/TSMCA.2011.2157136","article-title":"Process nets with channels","volume":"42","author":"Liu","year":"2012","journal-title":"IEEE Trans. Syst. Man Cybern. Part A Syst. Hum."},{"key":"ref_44","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/s00165-010-0161-4","article-title":"Soundness of workflow nets: Classification, decidability, and analysis","volume":"23","author":"Wynn","year":"2011","journal-title":"Form. Asp. Comput."},{"key":"ref_45","doi-asserted-by":"crossref","first-page":"86863","DOI":"10.1109\/ACCESS.2019.2920677","article-title":"A siphon-based deadlock prevention strategy for S 3 PR","volume":"7","author":"Guo","year":"2019","journal-title":"IEEE Access"},{"key":"ref_46","unstructured":"Zhou, M.C., and Fanti, M.P. (2004). Deadlock Resolution in Computer-Integrated Systems, CRC Press, Inc."},{"key":"ref_47","doi-asserted-by":"crossref","unstructured":"Hillah, L.M., Kordon, F., Petrucci, L., and Treves, N. (2010, January 21\u201325). PNML Framework: An extendable reference implementation of the Petri Net Markup Language. Proceedings of the International Conference on Applications and Theory of Petri Nets, Braga, Portugal.","DOI":"10.1007\/978-3-642-13675-7_20"},{"key":"ref_48","unstructured":"Xiang, D., Liu, G., Yan, C.G., and Jiang, C. (2019). A Guard-driven Analysis Approach of Workflow Net With Data. IEEE Trans. Serv. Comput., 1."},{"key":"ref_49","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/s10515-012-0109-4","article-title":"JRF-E: Using model checking to give advice on eliminating memory model-related bugs","volume":"19","author":"Kim","year":"2012","journal-title":"Autom. Softw. Eng."},{"key":"ref_50","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1109\/JAS.2017.7510766","article-title":"Detecting data-flow errors based on Petri nets with data operations","volume":"5","author":"Xiang","year":"2017","journal-title":"IEEE\/CAA J. Autom. Sin."},{"key":"ref_51","doi-asserted-by":"crossref","first-page":"899","DOI":"10.1109\/TSE.2016.2531666","article-title":"A Lightweight System for Detecting and Tolerating Concurrency Bugs","volume":"42","author":"Zhang","year":"2016","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Symmetry"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-8994\/13\/3\/392\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T05:30:16Z","timestamp":1760160616000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-8994\/13\/3\/392"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2,28]]},"references-count":51,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2021,3]]}},"alternative-id":["sym13030392"],"URL":"https:\/\/doi.org\/10.3390\/sym13030392","relation":{},"ISSN":["2073-8994"],"issn-type":[{"value":"2073-8994","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,2,28]]}}}