{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:24:09Z","timestamp":1779074649021,"version":"3.51.4"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,7,31]],"date-time":"2017-07-31T00:00:00Z","timestamp":1501459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"University Research Board (URB) at the American University of Beirut"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2017,7,31]]},"abstract":"<jats:p>We present a criterion for checking local and global deadlock freedom of finite state systems expressed in BIP: a component-based framework for constructing complex distributed systems. Our criterion is evaluated by model-checking a set of subsystems of the overall large system. If satisfied in small subsystems, it implies deadlock-freedom of the overall system. If not satisfied, then we re-evaluate over larger subsystems, which improves the accuracy of the check. When the subsystem being checked becomes the entire system, our criterion becomes complete for deadlock-freedom. Hence our criterion only fails to decide deadlock freedom because of computational limitations: state-space explosion sets in when the subsystems become too large. Our method thus combines the possibility of fast response together with theoretical completeness. Other criteria for deadlock freedom, in contrast, are incomplete in principle, and so may fail to decide deadlock freedom even if unlimited computational resources are available. Also, our criterion certifies freedom from local deadlock, in which a subsystem is deadlocked while the rest of the system executes. Other criteria only certify freedom from global deadlock. We present experimental results for dining philosophers and for a multi-token-based resource allocation system, which subsumes several data arbiters and schedulers, including Milner\u2019s token-based scheduler.<\/jats:p>","DOI":"10.1145\/3152910","type":"journal-article","created":{"date-parts":[[2018,1,4]],"date-time":"2018-01-04T16:27:31Z","timestamp":1515083251000},"page":"1-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Global and Local Deadlock Freedom in BIP"],"prefix":"10.1145","volume":"26","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1989-0974","authenticated-orcid":false,"given":"Paul C.","family":"Attie","sequence":"first","affiliation":[{"name":"American University of Beirut, Lebanon"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[{"name":"UJF-Grenoble 1\/CNRS VERIMAG, France, Saddek"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[{"name":"UJF-Grenoble 1\/CNRS VERIMAG, France, Marius"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamad","family":"Jaber","sequence":"additional","affiliation":[{"name":"American University of Beirut, Lebanon"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joseph","family":"Sifakis","sequence":"additional","affiliation":[{"name":"Ecole Polytechnique Federale, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fadi A.","family":"Zaraket","sequence":"additional","affiliation":[{"name":"American University of Beirut, Lebanon"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,1,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_28"},{"key":"e_1_2_1_2_1","first-page":"658","article-title":"A general approach to deadlock freedom verification for software architectures","volume":"2805","author":"Aldini Alessandro","year":"2003","unstructured":"Alessandro Aldini and Marco Bernardo . 2003 . A general approach to deadlock freedom verification for software architectures . FME 2805 (2003), 658 -- 677 . Alessandro Aldini and Marco Bernardo. 2003. A general approach to deadlock freedom verification for software architectures. FME 2805 (2003), 658--677.","journal-title":"FME"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_22"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.11.032"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0252-9"},{"key":"e_1_2_1_6_1","volume-title":"Zaraket","author":"Attie Paul C.","year":"2013","unstructured":"Paul C. Attie , Saddek Bensalem , Marius Bozga , Mohamad Jaber , Joseph Sifakis , and Fadi A . Zaraket . 2013 . An abstract framework for deadlock prevention in BIP. In Proceedings of the Formal Techniques for Distributed Systems - Joint IFIP WG 6.1 International Conference, FMOODS\/FORTE 2013, held as part of the 8th International Federated Conference on Distributed Computing Techniques (DisCoTec\u201913). Springer-Verlag , 161--177. Paul C. Attie, Saddek Bensalem, Marius Bozga, Mohamad Jaber, Joseph Sifakis, and Fadi A. Zaraket. 2013. An abstract framework for deadlock prevention in BIP. In Proceedings of the Formal Techniques for Distributed Systems - Joint IFIP WG 6.1 International Conference, FMOODS\/FORTE 2013, held as part of the 8th International Federated Conference on Distributed Computing Techniques (DisCoTec\u201913). Springer-Verlag, 161--177."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_30"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/271510.271519"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02242712"},{"key":"e_1_2_1_10_1","volume-title":"Automation and Test in Europe Conference and Exposition (DATE\u201904)","author":"Baumgartner Jason","year":"2004","unstructured":"Jason Baumgartner and Andreas Kuehlmann . 2004 . Enhanced diameter bounding via structural transformation. In Design , Automation and Test in Europe Conference and Exposition (DATE\u201904) . IEEE, 36--41. Jason Baumgartner and Andreas Kuehlmann. 2004. Enhanced diameter bounding via structural transformation. In Design, Automation and Test in Europe Conference and Exposition (DATE\u201904). IEEE, 36--41."},{"key":"e_1_2_1_11_1","volume-title":"Abraham","author":"Baumgartner Jason","year":"2002","unstructured":"Jason Baumgartner , Andreas Kuehlmann , and Jacob A . Abraham . 2002 . Property checking via structural analysis. In Computer Aided Verification (CAV\u201902). Springer-Verlag , 151--165. Jason Baumgartner, Andreas Kuehlmann, and Jacob A. Abraham. 2002. Property checking via structural analysis. In Computer Aided Verification (CAV\u201902). Springer-Verlag, 151--165."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_18"},{"key":"e_1_2_1_13_1","volume-title":"NASA Formal Methods","author":"Bensalem Saddek","unstructured":"Saddek Bensalem , Andreas Griesmayer , Axel Legay , Thanh-Hung Nguyen , Joseph Sifakis , and Rongjie Yan . 2011. D-finder 2: Towards efficient correctness of incremental design . In NASA Formal Methods . Springer-Verlag , Pasadena, CA , 453--458. Saddek Bensalem, Andreas Griesmayer, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, and Rongjie Yan. 2011. D-finder 2: Towards efficient correctness of incremental design. In NASA Formal Methods. Springer-Verlag, Pasadena, CA, 453--458."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2008.26"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1879021.1879049"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30564-1_1"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784721"},{"key":"e_1_2_1_18_1","volume-title":"Time for Verification, Essays in Memory of Amir Pnueli","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke , Robert P. Kurshan , and Helmut Veith . 2010. The localization reduction and counterexample-guided abstraction refinement . In Time for Verification, Essays in Memory of Amir Pnueli . Springer-Verlag , New York, NY , 61--71. Edmund M. Clarke, Robert P. Kurshan, and Helmut Veith. 2010. The localization reduction and counterexample-guided abstraction refinement. In Time for Verification, Essays in Memory of Amir Pnueli. Springer-Verlag, New York, NY, 61--71."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0063-8"},{"key":"e_1_2_1_20_1","volume-title":"Introduction to Lattices and Order","author":"Davey Brian","unstructured":"Brian Davey and Hilary Priestly . 2002. Introduction to Lattices and Order . Cambridge University Press , Cambridge, UK . Brian Davey and Hilary Priestly. 2002. Introduction to Lattices and Order. Cambridge University Press, Cambridge, UK."},{"key":"e_1_2_1_21_1","volume-title":"Component-based construction of deadlock-free systems","author":"G\u00f6ssler Gregor","unstructured":"Gregor G\u00f6ssler and Joseph Sifakis . 2003. Component-based construction of deadlock-free systems . In FSTTCS. Springer ,420--433. Gregor G\u00f6ssler and Joseph Sifakis. 2003. Component-based construction of deadlock-free systems. In FSTTCS. Springer,420--433."},{"key":"e_1_2_1_22_1","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-theoretic Approach","author":"Kurshan Robert P.","unstructured":"Robert P. Kurshan . 1994. Computer-Aided Verification of Coordinating Processes: The Automata-theoretic Approach . Princeton University Press , Princeton, NJ . Robert P. Kurshan. 1994. Computer-Aided Verification of Coordinating Processes: The Automata-theoretic Approach. Princeton University Press, Princeton, NJ."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0160-6"},{"key":"e_1_2_1_25_1","volume-title":"Communication and Concurrency","author":"Milner Robin","unstructured":"Robin Milner . 1989. Communication and Concurrency . Prentice Hall , New Jersey . Robin Milner. 1989. Communication and Concurrency. Prentice Hall, New Jersey."},{"key":"e_1_2_1_26_1","volume-title":"Computational Complexity","author":"Papadimitriou Christos H.","unstructured":"Christos H. Papadimitriou . 1994. Computational Complexity . Addison-Wesley , Boston, MA . Christos H. Papadimitriou. 1994. Computational Complexity. Addison-Wesley, Boston, MA."},{"key":"e_1_2_1_27_1","first-page":"59","article-title":"Fixpoint induction and proofs of program properties","volume":"5","author":"Park David","year":"1969","unstructured":"David Park . 1969 . Fixpoint induction and proofs of program properties . Mach. Intell. 5 (1969), 59 -- 78 . David Park. 1969. Fixpoint induction and proofs of program properties. Mach. Intell. 5 (1969), 59--78.","journal-title":"Mach. Intell."},{"key":"e_1_2_1_28_1","volume-title":"Zuck","author":"Pnueli Amir","year":"2001","unstructured":"Amir Pnueli , Sitvanit Ruah , and Lenore D . Zuck . 2001 . Automatic deductive verification with invisible invariants. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS. Springer-Verlag , Genova, Italy, 82--97. Amir Pnueli, Sitvanit Ruah, and Lenore D. Zuck. 2001. Automatic deductive verification with invisible invariants. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS. Springer-Verlag, Genova, Italy, 82--97."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90004-6"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_2_1_31_1","first-page":"4","article-title":"Computation tree logic with deadlock detection","volume":"5","author":"van Glabbeek Rob J.","year":"2009","unstructured":"Rob J. van Glabbeek , Bas Luttik , and Nikola Trcka . 2009 . Computation tree logic with deadlock detection . Log. Methods Comp. Sci. 5 , 4 (Oct. 2009), 1--24. Rob J. van Glabbeek, Bas Luttik, and Nikola Trcka. 2009. Computation tree logic with deadlock detection. Log. Methods Comp. Sci. 5, 4 (Oct. 2009), 1--24.","journal-title":"Log. Methods Comp. Sci."}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3152910","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3152910","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:20Z","timestamp":1750212680000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3152910"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,31]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,7,31]]}},"alternative-id":["10.1145\/3152910"],"URL":"https:\/\/doi.org\/10.1145\/3152910","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,7,31]]},"assertion":[{"value":"2016-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-01-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}