{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T04:33:25Z","timestamp":1782966805454,"version":"3.54.5"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"9","license":[{"start":{"date-parts":[[2021,8,24]],"date-time":"2021-08-24T00:00:00Z","timestamp":1629763200000},"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":["Commun. ACM"],"published-print":{"date-parts":[[2021,9]]},"abstract":"<jats:p>As robots begin to interact closely with humans, we need to build systems worthy of trust regarding the safety and quality of the interaction.<\/jats:p>","DOI":"10.1145\/3433637","type":"journal-article","created":{"date-parts":[[2021,8,24]],"date-time":"2021-08-24T14:28:46Z","timestamp":1629815326000},"page":"78-84","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["Formalizing and guaranteeing human-robot interaction"],"prefix":"10.1145","volume":"64","author":[{"given":"Hadas","family":"Kress-Gazit","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, NY"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kerstin","family":"Eder","sequence":"additional","affiliation":[{"name":"University of Bristol, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guy","family":"Hoffman","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, NY"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Henny","family":"Admoni","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Brenna","family":"Argall","sequence":"additional","affiliation":[{"name":"Northwestern University, Evanston, IL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"R\u00fcdiger","family":"Ehlers","sequence":"additional","affiliation":[{"name":"Clausthal University of Technology in Clausthal-Zellerfeld, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoffer","family":"Heckman","sequence":"additional","affiliation":[{"name":"University of Colorado, Boulder, CO"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, The Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ross","family":"Knepper","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[{"name":"Technical University of Munich, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shelly","family":"Levy-Tzedek","sequence":"additional","affiliation":[{"name":"Ben-Gurion University, Beersheba, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jamy","family":"Li","sequence":"additional","affiliation":[{"name":"Ryerson University in Toronto, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Todd","family":"Murphey","sequence":"additional","affiliation":[{"name":"Northwestern University in Evanston, IL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laurel","family":"Riek","sequence":"additional","affiliation":[{"name":"University of California San Diego"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dorsa","family":"Sadigh","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, CA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,8,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.4230\/DagRep.9.2.91"},{"key":"e_1_2_1_2_1","volume-title":"et al. Coverage-driven verification---An approach to verify code for robots that directly interact with humans. Hardware and Software: Verification and Testing","author":"Araiza-Illan D.","year":"2015","unstructured":"Araiza-Illan , D. et al. Coverage-driven verification---An approach to verify code for robots that directly interact with humans. Hardware and Software: Verification and Testing ( 2015 ), 69--84. Araiza-Illan, D. et al. Coverage-driven verification---An approach to verify code for robots that directly interact with humans. Hardware and Software: Verification and Testing (2015), 69--84."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40379-3_3"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2010.07.002"},{"key":"e_1_2_1_5_1","volume-title":"et al. Social robotics","author":"Breazeal C.","year":"2016","unstructured":"Breazeal , C. et al. Social robotics . Springer Handbook of Robotics , Springer , ( 2016 ), 1935--1972. Breazeal, C. et al. Social robotics. Springer Handbook of Robotics, Springer, (2016), 1935--1972."},{"key":"e_1_2_1_6_1","volume-title":"et al. Socio-cyber-physical systems: Models, opportunities, open challenges. 2019 IEEE\/ACM 5th Intern. Wkshp. Soft. Eng. for Smart Cyber-Physical Systems","author":"Calinescu R.","year":"2019","unstructured":"Calinescu , R. et al. Socio-cyber-physical systems: Models, opportunities, open challenges. 2019 IEEE\/ACM 5th Intern. Wkshp. Soft. Eng. for Smart Cyber-Physical Systems ( 2019 ), 2--6. Calinescu, R. et al. Socio-cyber-physical systems: Models, opportunities, open challenges. 2019 IEEE\/ACM 5th Intern. Wkshp. Soft. Eng. for Smart Cyber-Physical Systems (2019), 2--6."},{"key":"e_1_2_1_7_1","volume-title":"Intern. Conf. Robotics and Automation","author":"Campos T.","year":"2019","unstructured":"Campos , T. et al. SMT-based control and feedback for social navigation . Intern. Conf. Robotics and Automation , 2019 , Montreal, QC, Canada, 5005--5011. Campos, T. et al. SMT-based control and feedback for social navigation. Intern. Conf. Robotics and Automation, 2019, Montreal, QC, Canada, 5005--5011."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/3264692"},{"key":"e_1_2_1_9_1","volume-title":"Academic Press. (1975) 41--58.","author":"Grice H.P.","unstructured":"Grice , H.P. Logic and conversation. Syntax and Semantics , Vol. 3 : Speech Acts. P. Cole and J.L. Morgan, eds. Academic Press. (1975) 41--58. Grice, H.P. Logic and conversation. Syntax and Semantics, Vol. 3: Speech Acts. P. Cole and J.L. Morgan, eds. Academic Press. (1975) 41--58."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/THMS.2019.2904558"},{"key":"e_1_2_1_12_1","volume-title":"Human-robot teaming: Approaches from joint action and dynamical systems","author":"Iqbal T.","year":"2019","unstructured":"Iqbal , T. and Riek , L.D . Human-robot teaming: Approaches from joint action and dynamical systems . Humanoid Robotics : A Reference ( 2019 ), 2293--2312. Iqbal, T. and Riek, L.D. Human-robot teaming: Approaches from joint action and dynamical systems. Humanoid Robotics: A Reference (2019), 2293--2312."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1126\/scirobotics.aat1587"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1146\/annurev-control-060117-104838"},{"key":"e_1_2_1_15_1","volume-title":"Survey of statistical verification of linear unbounded properties: Model checking and distances. Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"Kret\u00ednsk\u00fd J.","year":"2016","unstructured":"Kret\u00ednsk\u00fd , J. Survey of statistical verification of linear unbounded properties: Model checking and distances. Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques ( 2016 ), 27--45. Kret\u00ednsk\u00fd, J. Survey of statistical verification of linear unbounded properties: Model checking and distances. Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (2016), 27--45."},{"key":"e_1_2_1_16_1","volume-title":"Proc. of the IEEE\/RSJ Intern. Conf. on Intelligent Robots and Systems","author":"Kshirsagar A.","year":"2019","unstructured":"Kshirsagar , A. et al. Specifying and synthesizing human-robot handovers . In Proc. of the IEEE\/RSJ Intern. Conf. on Intelligent Robots and Systems ( 2019 ). Kshirsagar, A. et al. Specifying and synthesizing human-robot handovers. In Proc. of the IEEE\/RSJ Intern. Conf. on Intelligent Robots and Systems (2019)."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.neubiorev.2019.07.014"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ROMAN.2012.6343850"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"e_1_2_1_21_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems---20th Intern. Conf.","author":"Li W.","year":"2014","unstructured":"Li , W. et al. Synthesis for human-in-the-loop control systems . Tools and Algorithms for the Construction and Analysis of Systems---20th Intern. Conf. ( 2014 ), 470--484. Li, W. et al. Synthesis for human-in-the-loop control systems. Tools and Algorithms for the Construction and Analysis of Systems---20th Intern. Conf. (2014), 470--484."},{"key":"e_1_2_1_22_1","volume-title":"et al. Assurance in reinforcement learning using quantitative verification. Advances in Hybridization of Intelligent Methods: Models, Systems and Applications","author":"Mason G.","unstructured":"Mason , G. et al. Assurance in reinforcement learning using quantitative verification. Advances in Hybridization of Intelligent Methods: Models, Systems and Applications . I. Hatzilygeroudis and V. Palade, eds. Springer International Publishing , 71--96. Mason, G. et al. Assurance in reinforcement learning using quantitative verification. Advances in Hybridization of Intelligent Methods: Models, Systems and Applications. I. Hatzilygeroudis and V. Palade, eds. Springer International Publishing, 71--96."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-32552-1_73"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ROMAN.2017.8172354"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242587.3242634"},{"key":"e_1_2_1_26_1","volume-title":"Mental models and the control of action in complex environments. Selected Papers of the 6th Interdisciplinary Wkshp. on Informatics and Psychology: Mental Models and Human-Computer Interaction 1 (NLD","author":"Rasmussen J.","year":"1987","unstructured":"Rasmussen , J. Mental models and the control of action in complex environments. Selected Papers of the 6th Interdisciplinary Wkshp. on Informatics and Psychology: Mental Models and Human-Computer Interaction 1 (NLD , 1987 ), 41--69. Rasmussen, J. Mental models and the control of action in complex environments. Selected Papers of the 6th Interdisciplinary Wkshp. on Informatics and Psychology: Mental Models and Human-Computer Interaction 1 (NLD, 1987), 41--69."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127874"},{"key":"e_1_2_1_28_1","volume-title":"et al. Planning for cars that coordinate with people: Leveraging effects on human actions for planning and active information gathering over human internal state. Autonomous Robots (AURO) 42, 7 (Oct","author":"Sadigh D.","year":"2018","unstructured":"Sadigh , D. et al. Planning for cars that coordinate with people: Leveraging effects on human actions for planning and active information gathering over human internal state. Autonomous Robots (AURO) 42, 7 (Oct . 2018 ), 1405--1426. Sadigh, D. et al. Planning for cars that coordinate with people: Leveraging effects on human actions for planning and active information gathering over human internal state. Autonomous Robots (AURO) 42, 7 (Oct. 2018), 1405--1426."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1561\/2300000049"},{"key":"e_1_2_1_30_1","volume-title":"Test generation with inputs, outputs and repetitive quiescence","author":"Tretmans G.J.","unstructured":"Tretmans , G.J. Test generation with inputs, outputs and repetitive quiescence . Centre for Telematics and Information Technology (CTIT) . Tretmans, G.J. Test generation with inputs, outputs and repetitive quiescence. Centre for Telematics and Information Technology (CTIT)."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1177\/0278364919883338"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0749-596X(92)90010-U"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3433637","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3433637","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:10Z","timestamp":1750195690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3433637"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,24]]},"references-count":32,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2021,9]]}},"alternative-id":["10.1145\/3433637"],"URL":"https:\/\/doi.org\/10.1145\/3433637","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,24]]},"assertion":[{"value":"2021-08-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}