{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:22:06Z","timestamp":1750306926480,"version":"3.41.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2013,3,1]],"date-time":"2013-03-01T00:00:00Z","timestamp":1362096000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Intell. Syst. Technol."],"published-print":{"date-parts":[[2013,3]]},"abstract":"<jats:p>A (business) protocol describes, in high-level terms, a pattern of communication between two or more participants, specifically via the creation and manipulation of the commitments between them. In this manner, a protocol offers both flexibility and rigor: a participant may communicate in any way it chooses as long as it discharges all of its activated commitments. Protocols thus promise benefits in engineering cross-organizational business processes. However, software engineering using protocols presupposes a formalization of protocols and a notion of the<jats:italic>refinement<\/jats:italic>of one protocol by another. Refinement for protocols is both intuitively obvious (e.g.,<jats:italic>PayViaCheck<\/jats:italic>is clearly a kind of<jats:italic>Pay<\/jats:italic>) and technically nontrivial (e.g., compared to<jats:italic>Pay<\/jats:italic>,<jats:italic>PayViaCheck<\/jats:italic>involves different participants exchanging different messages). This article formalizes protocols and their refinement. It develops Proton, an analysis tool for protocol specifications that overlays a model checker to compute whether one protocol refines another with respect to a stated mapping. Proton and its underlying theory are evaluated by formalizing several protocols from the literature and verifying all and only the expected refinements.<\/jats:p>","DOI":"10.1145\/2438653.2438656","type":"journal-article","created":{"date-parts":[[2013,4,1]],"date-time":"2013-04-01T19:39:32Z","timestamp":1364845172000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Formalizing and verifying protocol refinements"],"prefix":"10.1145","volume":"4","author":[{"given":"Scott N.","family":"Gerard","sequence":"first","affiliation":[{"name":"North Carolina State University, Raleigh, NC"}]},{"given":"Munindar P.","family":"Singh","sequence":"additional","affiliation":[{"name":"North Carolina State University, Raleigh, NC"}]}],"member":"320","published-online":{"date-parts":[[2013,4,3]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"volume-title":"Proceedings of the International Workshop on Agent Communication.10--29","author":"Baldoni M.","key":"e_1_2_2_2_1"},{"volume-title":"Proceedings of the 8th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS'09)","author":"Chopra A. K.","key":"e_1_2_2_3_1"},{"volume-title":"Proceedings of the 8th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS'09)","author":"Cohen M.","key":"e_1_2_2_4_1"},{"volume-title":"Proceedings of the International Workshop on Agent Communication. 53--72","author":"El-Menshawy M.","key":"e_1_2_2_5_1"},{"key":"e_1_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Fagin R. Halpern J. Y. Moses Y. and Vardi M. Y. 1995. Reasoning about Knowledge. MIT Press Cambridge MA. Fagin R. Halpern J. Y. Moses Y. and Vardi M. Y. 1995. Reasoning about Knowledge. MIT Press Cambridge MA.","DOI":"10.7551\/mitpress\/5803.001.0001"},{"volume-title":"Proceedings of the Colloquium on Temporal Logic in Specification","series-title":"Lecture Notes in Computer Science","author":"Gabbay D.","key":"e_1_2_2_7_1"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_55"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1160633.1160660"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-006-7232-1"},{"volume-title":"Eds","year":"2003","author":"Malone T. W.","key":"e_1_2_2_11_1"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015586128739"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/544741.544856"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-9833.1998.tb00120.x"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008319631231"},{"volume-title":"Proceedings of the 23rd Conference on Artificial Intelligence. AAAI Press, 176--181","year":"2008","author":"Singh M. P.","key":"e_1_2_2_16_1"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11355-0_12"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/IAT.2006.53"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1329125.1329283"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.datak.2006.12.001"},{"key":"e_1_2_2_21_1","first-page":"235","article-title":"Commitment machines. In Proceedings of the 8th International Workshop on Agent Theories, Architectures, and Languages (ATAL'01)","volume":"2333","author":"Yolum P.","year":"2002","journal-title":"Lecture Notes in Artificial Intelligence"}],"container-title":["ACM Transactions on Intelligent Systems and Technology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2438653.2438656","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2438653.2438656","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:35:29Z","timestamp":1750235729000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2438653.2438656"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,3]]}},"alternative-id":["10.1145\/2438653.2438656"],"URL":"https:\/\/doi.org\/10.1145\/2438653.2438656","relation":{},"ISSN":["2157-6904","2157-6912"],"issn-type":[{"type":"print","value":"2157-6904"},{"type":"electronic","value":"2157-6912"}],"subject":[],"published":{"date-parts":[[2013,3]]},"assertion":[{"value":"2010-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-04-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}