{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T12:40:04Z","timestamp":1749645604045,"version":"3.41.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"3","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61872232 and 61672340"],"award-info":[{"award-number":["61872232 and 61672340"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,9,30]]},"abstract":"<jats:p>\n            Due to the general undecidable results, verification of concurrent programs is a big challenge. Most existing verifiers adopt Petri net and its extensions based on abstraction and approximation as their verification models, which yet suffer from intractable complexity and are thus challenging to be efficient and complete. We choose\n            <jats:italic>Basic Parallel Process (BPP)<\/jats:italic>\n            , a subclass of Petri nets, as the backbone verification model for verifying concurrent programs due to its lower complexity. We propose BPPChecker, the first model checker for verifying a subclass of CTL on BPP. A constraint-based algorithm is given in which formulas are handled by SMT solver Z3. Our approach involves introducing a\n            <jats:italic>k<\/jats:italic>\n            -step semantics for the\n            <jats:bold>EG<\/jats:bold>\n            operator. By doing so, we reduce the problem of deciding the satisfiability of\n            <jats:bold>EG<\/jats:bold>\n            -formulas and\n            <jats:bold>EF<\/jats:bold>\n            <jats:sub>1<\/jats:sub>\n            -formulas to the problem of deciding the satisfiability of linear integer arithmetic formulas. Besides, we encode the\n            <jats:italic>Actor Communicating System (ACS)<\/jats:italic>\n            , a program model for asynchronously communicating programs, to BPP. Experimental results show that BPPChecker performs more efficiently than the existing tools for a series of branching-time property verification problems of Erlang programs.\n          <\/jats:p>","DOI":"10.1145\/3721141","type":"journal-article","created":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T10:11:03Z","timestamp":1741169463000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["BPPChecker: An SMT-based Model Checker on Basic Parallel Processes"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9005-7112","authenticated-orcid":false,"given":"Guoqiang","family":"Li","sequence":"first","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-9010-5364","authenticated-orcid":false,"given":"Qizhe","family":"Yang","sequence":"additional","affiliation":[{"name":"Shanghai Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-5779-8409","authenticated-orcid":false,"given":"Jinhao","family":"Tan","sequence":"additional","affiliation":[{"name":"The University of Hong Kong, Hong Kong, Hong Kong"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-4891-6854","authenticated-orcid":false,"given":"Ying","family":"Zhao","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,11]]},"reference":[{"key":"e_1_3_3_2_1","first-page":"101","volume-title":"Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation","author":"Amat Nicolas","year":"2023","unstructured":"Nicolas Amat, Silvano Dal Zilio, and Didier Le Botlan. 2023. Project and conquer: Fast quantifier elimination for checking petri net reachability. In Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 101\u2013123."},{"key":"e_1_3_3_3_1","first-page":"107","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Atig Mohamed Faouzi","year":"2009","unstructured":"Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. 2009. Context-bounded analysis for concurrent programs with dynamic creation of threads. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 107\u2013123."},{"key":"e_1_3_3_4_1","volume-title":"Proceedings of the PLI\u201901 Erlang Workshop","author":"Carlsson Richard","year":"2001","unstructured":"Richard Carlsson. 2001. An introduction to core erlang. In Proceedings of the PLI\u201901 Erlang Workshop. Citeseer."},{"key":"e_1_3_3_5_1","unstructured":"S\u00f8ren Christensen. 1993. Decidability and decomposition in process algebras.(1993)."},{"issue":"1","key":"e_1_3_3_6_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3422822","article-title":"The reachability problem for Petri nets is not elementary","volume":"68","author":"Czerwi\u0144ski Wojciech","year":"2020","unstructured":"Wojciech Czerwi\u0144ski, S\u0142awomir Lasota, Ranko Lazi\u0107, J\u00e9r\u00f4me Leroux, and Filip Mazowiecki. 2020. The reachability problem for Petri nets is not elementary. Journal of the ACM 68, 1 (2020), 1\u201328.","journal-title":"Journal of the ACM"},{"key":"e_1_3_3_7_1","doi-asserted-by":"crossref","first-page":"1229","DOI":"10.1109\/FOCS52979.2021.00120","volume-title":"Proceedings of the 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science","author":"Czerwi\u0144ski Wojciech","year":"2022","unstructured":"Wojciech Czerwi\u0144ski and \u0141ukasz Orlikowski. 2022. Reachability in vector addition systems is Ackermann-complete. In Proceedings of the 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science. IEEE, 1229\u20131240."},{"key":"e_1_3_3_8_1","doi-asserted-by":"crossref","first-page":"492","DOI":"10.1007\/978-3-642-28756-5_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems: 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24\u2013April 1, 2012. Proceedings 18","author":"David Alexandre","year":"2012","unstructured":"Alexandre David, Lasse Jacobsen, Morten Jacobsen, Kenneth Yrke J\u00f8rgensen, Mikael H. M\u00f8ller, and Ji\u0159\u00ed Srba. 2012. TAPAAL 2.0: Integrated development environment for timed-arc Petri nets. In Tools and Algorithms for the Construction and Analysis of Systems: 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24\u2013April 1, 2012. Proceedings 18. Springer, 492\u2013497."},{"key":"e_1_3_3_9_1","first-page":"1","volume-title":"Proceedings of the 2023 IEEE International Conference on Networking, Sensing and Control","author":"Ding Zhijun","year":"2023","unstructured":"Zhijun Ding, Cong He, and Shuo Li. 2023. Enpac: Petri net model checking for linear temporal logic. In Proceedings of the 2023 IEEE International Conference on Networking, Sensing and Control. IEEE, 1\u20136."},{"key":"e_1_3_3_10_1","doi-asserted-by":"crossref","first-page":"454","DOI":"10.1007\/978-3-642-38856-9_24","volume-title":"Proceedings of the International Static Analysis Symposium","author":"D\u2019Osualdo Emanuele","year":"2013","unstructured":"Emanuele D\u2019Osualdo, Jonathan Kochems, and C.-H. Luke Ong. 2013. Automatic verification of Erlang-style concurrency. In Proceedings of the International Static Analysis Symposium. Springer, 454\u2013476."},{"key":"e_1_3_3_11_1","doi-asserted-by":"crossref","first-page":"535","DOI":"10.1007\/978-3-662-46669-8_22","volume-title":"Proceedings of the European Symposium on Programming Languages and Systems","author":"Emmi Michael","year":"2015","unstructured":"Michael Emmi, Pierre Ganty, Rupak Majumdar, and Fernando Rosa-Velardo. 2015. Analysis of asynchronous programs with event-based synchronization. In Proceedings of the European Symposium on Programming Languages and Systems. Springer, 535\u2013559."},{"key":"e_1_3_3_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-65306-6_20"},{"key":"e_1_3_3_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050074"},{"key":"e_1_3_3_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/263139.263146"},{"key":"e_1_3_3_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480895"},{"key":"e_1_3_3_16_1","first-page":"500","volume-title":"Proceedings of the International Conference on Concurrency Theory","author":"Kaiser Alexander","year":"2012","unstructured":"Alexander Kaiser, Daniel Kroening, and Thomas Wahl. 2012. Efficient coverability analysis by proof minimization. In Proceedings of the International Conference on Concurrency Theory. Springer, 500\u2013515."},{"key":"e_1_3_3_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"e_1_3_3_18_1","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/978-3-642-39799-8_10","volume-title":"Proceedings of the International Conference on Computer Aided Verification","author":"Kloos Johannes","year":"2013","unstructured":"Johannes Kloos, Rupak Majumdar, Filip Niksic, and Ruzica Piskac. 2013. Incremental, inductive coverability. In Proceedings of the International Conference on Computer Aided Verification. Springer, 158\u2013173."},{"key":"e_1_3_3_19_1","volume-title":"Verification of asynchronous concurrency and the shaped stack constraint","author":"Kochems Jonathan","year":"2014","unstructured":"Jonathan Kochems. 2014. Verification of asynchronous concurrency and the shaped stack constraint. Ph. D. Dissertation. Oxford University, UK."},{"key":"e_1_3_3_20_1","first-page":"288","volume-title":"Proceedings of the International Conference on Concurrency Theory","author":"Kochems Jonathan","year":"2013","unstructured":"Jonathan Kochems and C.-H. Luke Ong. 2013. Safety verification of asynchronous pushdown systems with shaped stacks. In Proceedings of the International Conference on Concurrency Theory. Springer, 288\u2013302."},{"key":"e_1_3_3_21_1","doi-asserted-by":"crossref","first-page":"1241","DOI":"10.1109\/FOCS52979.2021.00121","volume-title":"Proceedings of the 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science","author":"Leroux J\u00e9r\u00f4me","year":"2022","unstructured":"J\u00e9r\u00f4me Leroux. 2022. The reachability problem for Petri nets is not primitive recursive. In Proceedings of the 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science. IEEE, 1241\u20131252."},{"key":"e_1_3_3_22_1","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/3-540-62034-6_40","volume-title":"Proceedings of the International Conference on Foundations of Software Technology and Theoretical Computer Science","author":"Mayr Richard","year":"1996","unstructured":"Richard Mayr. 1996. Weak bisimulation and model checking for basic parallel processes. In Proceedings of the International Conference on Foundations of Software Technology and Theoretical Computer Science. Springer, 88\u201399."},{"key":"e_1_3_3_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_3_3_24_1","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/978-3-540-30476-0_11","volume-title":"Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31\u2013November 3, 2004. Proceedings 2","author":"Ogata Shougo","year":"2004","unstructured":"Shougo Ogata, Tatsuhiro Tsuchiya, and Tohru Kikuno. 2004. SAT-based verification of safe Petri nets. In Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31\u2013November 3, 2004. Proceedings 2. Springer, 79\u201392."},{"key":"e_1_3_3_25_1","unstructured":"C. A. Petri. 1966. Communication with Automata. Tech. Rep. Hamburg University. https:\/\/api.semanticscholar.org\/CorpusID:8420535"},{"key":"e_1_3_3_26_1","first-page":"93","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Qadeer Shaz","year":"2005","unstructured":"Shaz Qadeer and Jakob Rehof. 2005. Context-bounded model checking of concurrent software. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 93\u2013107."},{"key":"e_1_3_3_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_3_3_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349241"},{"key":"e_1_3_3_29_1","first-page":"300","volume-title":"Proceedings of the International Conference on Computer Aided Verification","author":"Sen Koushik","year":"2006","unstructured":"Koushik Sen and Mahesh Viswanathan. 2006. Model checking multithreaded programs with asynchronous atomic methods. In Proceedings of the International Conference on Computer Aided Verification. Springer, 300\u2013314."},{"key":"e_1_3_3_30_1","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/11532231_25","volume-title":"Proceedings of the International Conference on Automated Deduction","author":"Verma Kumar Neeraj","year":"2005","unstructured":"Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. 2005a. On the complexity of equational horn clauses. In Proceedings of the International Conference on Automated Deduction. Springer, 337\u2013352."},{"key":"e_1_3_3_31_1","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/11532231_25","volume-title":"Proceedings of the International Conference on Automated Deduction","author":"Verma Kumar Neeraj","year":"2005","unstructured":"Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. 2005b. On the complexity of equational horn clauses. In Proceedings of the International Conference on Automated Deduction. Springer, 337\u2013352."},{"key":"e_1_3_3_32_1","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/978-3-319-91268-4_18","volume-title":"Application and Theory of Petri Nets and Concurrency: 39th International Conference, PETRI NETS 2018, Bratislava, Slovakia, June 24\u201329, 2018, Proceedings 39","author":"Wolf Karsten","year":"2018","unstructured":"Karsten Wolf. 2018. Petri net model checking with LoLA 2. In Application and Theory of Petri Nets and Concurrency: 39th International Conference, PETRI NETS 2018, Bratislava, Slovakia, June 24\u201329, 2018, Proceedings 39. Springer, 351\u2013362."},{"issue":"8","key":"e_1_3_3_33_1","first-page":"2782","article-title":"Verification method and implementation of asynchronously communicating programs based on basic parallel processes","volume":"33","author":"Zhao Ying","year":"2022","unstructured":"Ying Zhao, Jinhao Tan, and Guoqiang Li. 2022. Verification method and implementation of asynchronously communicating programs based on basic parallel processes. Journal of Software (in Chinese) 33, 8 (2022), 2782\u20132796.","journal-title":"Journal of Software (in Chinese)"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3721141","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T12:00:46Z","timestamp":1749643246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3721141"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,11]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9,30]]}},"alternative-id":["10.1145\/3721141"],"URL":"https:\/\/doi.org\/10.1145\/3721141","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2025,6,11]]},"assertion":[{"value":"2024-03-04","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-25","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}