{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T19:38:45Z","timestamp":1771270725126,"version":"3.50.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2021,9,22]],"date-time":"2021-09-22T00:00:00Z","timestamp":1632268800000},"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. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2021,10,31]]},"abstract":"<jats:p>In this article, we develop a formal framework for automatic reasoning about the obligations of autonomous cyber-physical systems, including their social and ethical obligations. Obligations, permissions, and prohibitions are distinct from a system's mission, and are a necessary part of specifying advanced, adaptive AI-equipped systems. They need a dedicated deontic logic of obligations to formalize them. Most existing deontic logics lack corresponding algorithms and system models that permit automatic verification. We demonstrate how a particular deontic logic, Dominance Act Utilitarianism (DAU)\u00a0[23], is a suitable starting point for formalizing the obligations of autonomous systems like self-driving cars. We demonstrate its usefulness by formalizing a subset of Responsibility-Sensitive Safety (RSS) in DAU; RSS is an industrial proposal for how self-driving cars should and should not behave in traffic. We show that certain logical consequences of RSS are undesirable, indicating a need to further refine the proposal. We also demonstrate how obligations can change over time, which is necessary for long-term autonomy. We then demonstrate a model-checking algorithm for DAU formulas on weighted transition systems and illustrate it by model-checking obligations of a self-driving car controller from the literature.<\/jats:p>","DOI":"10.1145\/3460975","type":"journal-article","created":{"date-parts":[[2021,9,22]],"date-time":"2021-09-22T21:36:34Z","timestamp":1632346594000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Algorithmic Ethics: Formalization and Verification of Autonomous Vehicle Obligations"],"prefix":"10.1145","volume":"5","author":[{"given":"Colin","family":"Shea-Blymyer","sequence":"first","affiliation":[{"name":"Oregon State University, Corvallis, OR, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Houssam","family":"Abbas","sequence":"additional","affiliation":[{"name":"Oregon State University, Corvallis, OR, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,9,22]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"A Temporal Logic of Normative Systems","author":"\u00c5gotnes Thomas","unstructured":"Thomas \u00c5gotnes , Wiebe van der Hoek , Juan A. Rodr\u00edguez-Aguilar , Carles Sierra , and Michael Wooldridge . 2009. A Temporal Logic of Normative Systems . Springer Netherlands , Dordrecht , 69\u2013106. https:\/\/doi.org\/10.1007\/978-1-4020-9084-4_5 10.1007\/978-1-4020-9084-4_5 Thomas \u00c5gotnes, Wiebe van der Hoek, Juan A. Rodr\u00edguez-Aguilar, Carles Sierra, and Michael Wooldridge. 2009. A Temporal Logic of Normative Systems. Springer Netherlands, Dordrecht, 69\u2013106. https:\/\/doi.org\/10.1007\/978-1-4020-9084-4_5"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the AAAI Fall Symposium on Machine Ethics.","author":"Arkoudas Konstantine","year":"2005","unstructured":"Konstantine Arkoudas , Selmer Bringsjord , and Paul Bello . 2005 . Toward ethical robots via mechanized deontic logic . In Proceedings of the AAAI Fall Symposium on Machine Ethics. Konstantine Arkoudas, Selmer Bringsjord, and Paul Bello. 2005. Toward ethical robots via mechanized deontic logic. In Proceedings of the AAAI Fall Symposium on Machine Ethics."},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 11th International Conference on Logic Programming (ICLP'94)","author":"Artosi Alberto","year":"1994","unstructured":"Alberto Artosi , Paola Cattabriga , and Guido Governatori . 1994 . KED: A deontic theorem prover . In Proceedings of the 11th International Conference on Logic Programming (ICLP'94) . 60\u201376. Alberto Artosi, Paola Cattabriga, and Guido Governatori. 1994. KED: A deontic theorem prover. In Proceedings of the 11th International Conference on Logic Programming (ICLP'94). 60\u201376."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.02.030"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1512\/iumj.1957.6.56038"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3359986.3361203"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 14th International Conference on Deontic Logic and Normative Systems (DEON'18)","author":"Benzmmuller Christoph","year":"2018","unstructured":"Christoph Benzmmuller , Ali Farjami , and Xavier Parent . 2018 . A dyadic deontic logic in HOL . In Proceedings of the 14th International Conference on Deontic Logic and Normative Systems (DEON'18) . Christoph Benzmmuller, Ali Farjami, and Xavier Parent. 2018. A dyadic deontic logic in HOL. In Proceedings of the 14th International Conference on Deontic Logic and Normative Systems (DEON'18)."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10588-006-9537-7"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629686"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/MIS.2006.82"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11786849_7"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88833-8_5"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_28"},{"key":"e_1_2_1_16_1","volume-title":"The Logical Form of Imperatives. Department of Philosophy","author":"Chellas B. F.","unstructured":"B. F. Chellas . 1968. The Logical Form of Imperatives. Department of Philosophy , Stanford University . B. F. Chellas. 1968. The Logical Form of Imperatives. Department of Philosophy, Stanford University."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/332656"},{"key":"e_1_2_1_18_1","unstructured":"Dov Gabbay John Horty and Xavier Parent (Eds.). 2013. Handbook of Deontic Logic and Normative Systems. College Publications.  Dov Gabbay John Horty and Xavier Parent (Eds.). 2013. Handbook of Deontic Logic and Normative Systems. College Publications."},{"key":"e_1_2_1_19_1","volume-title":"Thornton","author":"Christian Gerdes J.","year":"2015","unstructured":"J. Christian Gerdes and Sarah M . Thornton . 2015 . Implementable Ethics for Autonomous Vehicles. Springer , Berlin, Germany, 87\u2013102. J. Christian Gerdes and Sarah M. Thornton. 2015. Implementable Ethics for Autonomous Vehicles. Springer, Berlin, Germany, 87\u2013102."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2514601.2514608"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.trc.2004.07.008"},{"key":"e_1_2_1_22_1","volume-title":"Deontic Logic: A historical survey and introduction","author":"Hilpinen Risto","year":"2013","unstructured":"Risto Hilpinen and Paul McNamara . 2013 . Deontic Logic: A historical survey and introduction . College Publications , 3\u2013136. Risto Hilpinen and Paul McNamara. 2013. Deontic Logic: A historical survey and introduction. College Publications, 3\u2013136."},{"key":"e_1_2_1_23_1","volume-title":"Agency and Deontic Logic","author":"Horty John","unstructured":"John Horty . 2001. Agency and Deontic Logic . Cambridge University Press . John Horty. 2001. Agency and Deontic Logic. Cambridge University Press."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01306968"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9499-8"},{"key":"e_1_2_1_26_1","volume-title":"DEON 2018","author":"Kulicki Piotr","year":"2018","unstructured":"Piotr Kulicki , Robert Trypuz , and Michael P. Musielewicz . 2018. Towards a formal ethics for autonomous cars. In Deontic Logic and Normative Systems\u201414th International Conference , DEON 2018 , Utrecht, The Netherlands , July 3-6, 2018 , Jan M. Broersen, Cleo Condoravdi, Nair Shyam, and Gabriella Pigozzi (Eds.). College Publications, 193\u2013209. Piotr Kulicki, Robert Trypuz, and Michael P. Musielewicz. 2018. Towards a formal ethics for autonomous cars. In Deontic Logic and Normative Systems\u201414th International Conference, DEON 2018, Utrecht, The Netherlands, July 3-6, 2018, Jan M. Broersen, Cleo Condoravdi, Nair Shyam, and Gabriella Pigozzi (Eds.). College Publications, 193\u2013209."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2616404"},{"key":"e_1_2_1_28_1","volume-title":"Mally's deontic logic. Stanford Encyclopedia of Philosophy Archive (Summer 2019 Edition).Retrieved","author":"Lokhorst Gert-Jan","year":"2021","unstructured":"Gert-Jan Lokhorst . 2019. Mally's deontic logic. Stanford Encyclopedia of Philosophy Archive (Summer 2019 Edition).Retrieved July 9, 2021 from https:\/\/plato.stanford.edu\/archives\/sum2019\/entries\/mally-deontic\/. Gert-Jan Lokhorst. 2019. Mally's deontic logic. Stanford Encyclopedia of Philosophy Archive (Summer 2019 Edition).Retrieved July 9, 2021 from https:\/\/plato.stanford.edu\/archives\/sum2019\/entries\/mally-deontic\/."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0378-x"},{"key":"e_1_2_1_30_1","volume-title":"Grundgesetze des Sollens: Elemente der Logik des Willens","author":"Mally Ernst","unstructured":"Ernst Mally . 1926. Grundgesetze des Sollens: Elemente der Logik des Willens . Synthese Library, Vol . 152. Springer , 225\u2013248. Ernst Mally. 1926. Grundgesetze des Sollens: Elemente der Logik des Willens. Synthese Library, Vol. 152. Springer, 225\u2013248."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_2_1_32_1","volume-title":"Deontic logic. Stanford Encyclopedia of Philosophy. Retrieved","author":"McNamara Paul","year":"2021","unstructured":"Paul McNamara . 2018. Deontic logic. Stanford Encyclopedia of Philosophy. Retrieved July 9, 2021 from https:\/\/plato.stanford.edu\/entries\/logic-deontic\/. Paul McNamara. 2018. Deontic logic. Stanford Encyclopedia of Philosophy. Retrieved July 9, 2021 from https:\/\/plato.stanford.edu\/entries\/logic-deontic\/."},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 5th International Conference on Advances in Modal Logic (AiML'04)","author":"Murakami Yuko","year":"2004","unstructured":"Yuko Murakami . 2004 . Utilitarian deontic logic . In Proceedings of the 5th International Conference on Advances in Modal Logic (AiML'04) . 288\u2013302. Yuko Murakami. 2004. Utilitarian deontic logic. In Proceedings of the 5th International Conference on Advances in Modal Logic (AiML'04). 288\u2013302."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.03.003"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/528623"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/3000001.3000012"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/ITSC.2015.269"},{"key":"e_1_2_1_39_1","unstructured":"Shai Shalev-Shwartz Shaked Shammah and Amnon Shashua. 2018. On a formal model of safe and scalable self-driving cars. arXiv:1708.06374v6.  Shai Shalev-Shwartz Shaked Shammah and Amnon Shashua. 2018. On a formal model of safe and scalable self-driving cars. arXiv:1708.06374v6."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382203"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2015.41"},{"key":"e_1_2_1_42_1","first-page":"237","article-title":"Deontic logic","volume":"60","author":"von Wright Georg H.","year":"1951","unstructured":"Georg H. von Wright . 1951 . Deontic logic . Mind 60 , 237 (Jan. 1951), 1\u201315. Georg H. von Wright. 1951. Deontic logic. Mind 60, 237 (Jan. 1951), 1\u201315.","journal-title":"Mind"},{"key":"e_1_2_1_43_1","volume-title":"Encyclopedia of Machine Learning","author":"Wiewiora Eric","unstructured":"Eric Wiewiora . 2010. Reward shaping . In Encyclopedia of Machine Learning . Springer US , Boston, MA , 863\u2013865. https:\/\/doi.org\/10.1007\/978-0-387-30164-8_731 10.1007\/978-0-387-30164-8_731 Eric Wiewiora. 2010. Reward shaping. In Encyclopedia of Machine Learning. Springer US, Boston, MA, 863\u2013865. https:\/\/doi.org\/10.1007\/978-0-387-30164-8_731"}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460975","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460975","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:48:22Z","timestamp":1750193302000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460975"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,22]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,10,31]]}},"alternative-id":["10.1145\/3460975"],"URL":"https:\/\/doi.org\/10.1145\/3460975","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"value":"2378-962X","type":"print"},{"value":"2378-9638","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,9,22]]},"assertion":[{"value":"2020-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-09-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}