{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:13:03Z","timestamp":1760044383707,"version":"3.41.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660 TRR 248"],"award-info":[{"award-number":["389792660 TRR 248"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/T006544\/1, EP\/K011715\/1, EP\/K034413\/1, EP\/L00058X\/1, EP\/N027833\/1, EP\/N028201\/1, EP\/T006544\/1, EP\/T014709\/1 and EP\/V000462\/1"],"award-info":[{"award-number":["EP\/T006544\/1, EP\/K011715\/1, EP\/K034413\/1, EP\/L00058X\/1, EP\/N027833\/1, EP\/N028201\/1, EP\/T006544\/1, EP\/T014709\/1 and EP\/V000462\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"name":"NCSS\/EPSRC","award":["VeTSS"],"award-info":[{"award-number":["VeTSS"]}]},{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["610150"],"award-info":[{"award-number":["610150"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>\n            We present a programming model and typing discipline for complex multi-robot coordination programming. Our model encompasses both synchronisation through message passing and continuous-time dynamic motion primitives in physical space. We specify\n            <jats:italic>continuous-time motion primitives<\/jats:italic>\n            in an assume-guarantee logic that ensures compatibility of motion primitives as well as collision freedom. We specify global behaviour of programs in a\n            <jats:italic>choreographic<\/jats:italic>\n            type system that extends multiparty session types with jointly executed motion primitives, predicated refinements, as well as a\n            <jats:italic>separating conjunction<\/jats:italic>\n            that allows reasoning about subsets of interacting robots. We describe a notion of\n            <jats:italic>well-formedness<\/jats:italic>\n            for global types that ensures motion and communication can be correctly synchronised and provide algorithms for checking well-formedness, projecting a type, and local type checking. A well-typed program is\n            <jats:italic>communication safe<\/jats:italic>\n            ,\n            <jats:italic>motion compatible<\/jats:italic>\n            , and\n            <jats:italic>collision free<\/jats:italic>\n            . Our type system provides a compositional approach to ensuring these properties.\n          <\/jats:p>\n          <jats:p>We have implemented our model on top of the ROS framework. This allows us to program multi-robot coordination scenarios on top of commercial and custom robotics hardware platforms. We show through case studies that we can model and statically verify quite complex manoeuvres involving multiple manipulators and mobile robots---such examples are beyond the scope of previous approaches.<\/jats:p>","DOI":"10.1145\/3428202","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Multiparty motion coordination: from choreographies to robotics programs"],"prefix":"10.1145","volume":"4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3925-8557","authenticated-orcid":false,"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3197-8736","authenticated-orcid":false,"given":"Damien","family":"Zufferey","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"R. Alur C. Courcoubetis N. Halbwachs T.A. Henzinger P.-H. Ho X. Nicollin A. Olivero J. Sifakis and S. Yovine. 1995. The algorithmic analysis of hybrid systems. Theoretical Computer Science 138 ( 1995 ) 3-34.  R. Alur C. Courcoubetis N. Halbwachs T.A. Henzinger P.-H. Ho X. Nicollin A. Olivero J. Sifakis and S. Yovine. 1995. The algorithmic analysis of hybrid systems. Theoretical Computer Science 138 ( 1995 ) 3-34.","DOI":"10.1016\/0304-3975(94)00202-T"},{"volume-title":"Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida.","year":"2016","author":"Ancona Davide","key":"e_1_2_2_3_1"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302509.3311052"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1561\/1000000053"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.04.019"},{"key":"e_1_2_2_7_1","first-page":"283","volume-title":"Meeting Deadlines Together. In 26th International Conference on Concurrency Theory (LIPIcs)","volume":"42","author":"Bocchi Laura","year":"2015"},{"key":"e_1_2_2_8_1","first-page":"583","volume-title":"Asynchronous Timed Session Types. In 28th European Symposium on Programming (LNCS)","volume":"11423","author":"Bocchi Laura","year":"2019"},{"key":"e_1_2_2_9_1","first-page":"419","volume-title":"Timed Multiparty Session Types. In 25th International Conference on Concurrency Theory (LNCS)","volume":"8704","author":"Bocchi Laura","year":"2014"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192406"},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Giuseppe Castagna Mariangiola Dezani-Ciancaglini and Luca Padovani. 2012. On Global Types and Multi-Party Session. Logical Methods in Computer Science 8 1 ( 2012 ).  Giuseppe Castagna Mariangiola Dezani-Ciancaglini and Luca Padovani. 2012. On Global Types and Multi-Party Session. Logical Methods in Computer Science 8 1 ( 2012 ).","DOI":"10.2168\/LMCS-8(1:24)2012"},{"key":"e_1_2_2_12_1","unstructured":"K.M. Chandy and J. Misra. 1988. Parallel Program Design: A Foundation. Addison-Wesley Publishing Company.  K.M. Chandy and J. Misra. 1988. Parallel Program Design: A Foundation. Addison-Wesley Publishing Company."},{"key":"e_1_2_2_13_1","first-page":"272","volume-title":"Nested Protocols in Session Types. In 23rd International Conference on Concurrency Theory (LNCS)","volume":"7454","author":"Demangeon Romain","year":"2012"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_10"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3055004.3055022"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.203.3"},{"volume-title":"Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday (LNCS)","author":"Dezani-Ciancaglini Mariangiola","key":"e_1_2_2_17_1"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_36"},{"volume-title":"Clarke","year":"2013","author":"Gao Sicun","key":"e_1_2_2_19_1"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3126513"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Simon Gay and Antonio Ravera (Eds.). 2017. Behavioural Types: from Theory to Tools. River Publishers.  Simon Gay and Antonio Ravera (Eds.). 2017. Behavioural Types: from Theory to Tools. River Publishers.","DOI":"10.13052\/rp-9788793519817"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Silvia Ghilezan Svetlana Jaksic Jovanka Pantovi Alceste Scalas and Nobuko Yoshida. 2019a. Precise subtyping for synchronous multiparty sessions. Journal of Logical and Algebraic Methods in Programming ( 2019 ). To appear.  Silvia Ghilezan Svetlana Jaksic Jovanka Pantovi Alceste Scalas and Nobuko Yoshida. 2019a. Precise subtyping for synchronous multiparty sessions. Journal of Logical and Algebraic Methods in Programming ( 2019 ). To appear.","DOI":"10.1016\/j.jlamp.2018.12.002"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2018.12.002"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561342"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45351-2_24"},{"volume-title":"Henzinger and Joseph Sifakis","year":"2007","author":"Thomas","key":"e_1_2_2_26_1"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","unstructured":"Kohei Honda Nobuko Yoshida and Marco Carbone. 2016. Multiparty Asynchronous Session Types. JACM 63 ( 2016 ) 1-67. Issue 1-9.  Kohei Honda Nobuko Yoshida and Marco Carbone. 2016. Multiparty Asynchronous Session Types. JACM 63 ( 2016 ) 1-67. Issue 1-9.","DOI":"10.1145\/2827695"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2873052"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Dimitrios Kouzapas and Nobuko Yoshida. 2015. Globally Governed Session Semantics. Logical Methods in Computer Science 10 4 ( 2015 ).  Dimitrios Kouzapas and Nobuko Yoshida. 2015. Globally Governed Session Semantics. Logical Methods in Computer Science 10 4 ( 2015 ).","DOI":"10.2168\/LMCS-10(4:20)2014"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676964"},{"volume-title":"Planning Algorithms","author":"LaValle Steven M.","key":"e_1_2_2_34_1"},{"volume-title":"Sensing and Filtering","author":"LaValle Steven M.","key":"e_1_2_2_35_1"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17164-2_1"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/PROC.1983.12681"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00067-1"},{"volume-title":"Proceedings of the 33rd European Conference on Object-Oriented Programming (ECOOP '19 ) (LIPIcs). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.","year":"2019","author":"Majumdar Rupak","key":"e_1_2_2_39_1"},{"volume-title":"Multiparty Motion Coordination: From Choreographies to Robotics Programs (Full version). arXiv:cs.RO\/","year":"2010","author":"Majumdar Rupak","key":"e_1_2_2_40_1"},{"volume-title":"Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","key":"e_1_2_2_41_1"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2453253"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0"},{"volume-title":"Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018. ACM, 819-828","year":"2018","author":"Platzer Andr\u00e9","key":"e_1_2_2_45_1"},{"volume-title":"ICRA workshop on open source software.","year":"2009","author":"Quigley Morgan","key":"e_1_2_2_46_1"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_48_1","first-page":"435","article-title":"The Phi-Calculus","author":"Rounds W.C.","year":"2003","journal-title":"In HSCC. Springer"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290343"},{"volume-title":"Illah Reza Nourbakhsh, and Davide Scaramuzza","year":"2011","author":"Siegwart Roland","key":"e_1_2_2_50_1"},{"key":"e_1_2_2_51_1","unstructured":"Sebastian Thrun Wolfram Burgard and Dieter Fox. 2006. Probabilistic Robotics. MIT.  Sebastian Thrun Wolfram Burgard and Dieter Fox. 2006. Probabilistic Robotics. MIT."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2510366"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25423-4_25"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360002"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-36987-3_5"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2351652"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428202","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428202","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:56Z","timestamp":1750197776000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428202"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":55,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428202"],"URL":"https:\/\/doi.org\/10.1145\/3428202","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}