More Web Proxy on the site http://driver.im/

research-article

A deontic logic analysis of autonomous systems' safety

Authors:

Colin Shea-Blymyer,

Houssam AbbasAuthors Info & Claims

HSCC '20: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control

Article No.: 26, Pages 1 - 11

https://doi.org/10.1145/3365365.3382203

Published: 22 April 2020 Publication History

Abstract

We consider the pressing question of how to model, verify, and ensure that autonomous systems meet certain obligations (like the obligation to respect traffic laws), and refrain from impermissible behavior (like recklessly changing lanes). Temporal logics are heavily used in autonomous system design; however, as we illustrate here, temporal (alethic) logics alone are inappropriate for reasoning about obligations of autonomous systems. This paper proposes the use of Dominance Act Utilitarianism (DAU), a deontic logic of agency, to encode and reason about obligations of autonomous systems. We use DAU to analyze Intel's Responsibility-Sensitive Safety (RSS) proposal as a real-world case study. We demonstrate that DAU can express well-posed RSS rules, formally derive undesirable consequences of these rules, illustrate how DAU could help design systems that have specific obligations, and how to model-check DAU obligations.

References

[1]

Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. 2002. Alternating-time Temporal Logic. J. ACM 49, 5 (Sept. 2002), 672--713.

Digital Library

[2]

Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, and Orna Kupferman. 2014. Temporal Specifications with Accumulative Values. ACM Trans. Comput. Logic 15, 4, Article 27 (July 2014), 25 pages.

Digital Library

[3]

Jan Broersen and Julien Brunel. 2008. `What I fail to do Today, I Have to Do Tomorrow': A Logical Study of the Propagation of Obligations. In Computational Logic in Multi-Agent Systems, Fariba Sadri and Ken Satoh (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 82--99.

[4]

Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. 2008. Quantitative Languages. In Computer Science Logic, Michael Kaminski and Simone Martini (Eds.). Springer Berlin Heidelberg, 385--400.

[5]

B.F. Chellas. 1968. The Logical Form of Imperatives. Department of Philosophy, Stanford University.

[6]

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, Massachusetts.

Digital Library

[7]

Dov Gabbay, John Horty, and Xavier Parent (Eds.). 2013. Handbook of deontic logic and normative systems. College Publications.

[8]

J. Christian Gerdes and Sarah M. Thornton. 2015. Implementable Ethics for Autonomous Vehicles. Springer Berlin Heidelberg, Berlin, Heidelberg, 87--102.

[9]

Laura Giordano, Alberto Martelli, and Daniele Theseider Dupré. 2013. Temporal Deontic Action Logic for the Verification of Compliance to Norms in ASP. In Proc. of the 14th Intl. Conf. on Artificial Intelligence and Law (ICAIL '13). ACM, New York, NY, USA, 53--62.

Digital Library

[10]

Andrew Hawkins. [n. d.]. Waymo's self-driving cars are now available on Lyft's app in Phoenix. The Verge ([n. d.]).

[11]

Risto Hilpinen and Paul McNamara. 2013. Deontic Logic: A historical survey and introduction.

[12]

John Horty. 2001. Agency and Deontic Logic. Cambridge University Press.

[13]

R. Koymans. 1990. Specifying Real-Time Properties with Metric Temporal Logic. Real-Time Systems 2, 4 (1990), 255--299.

Digital Library

[14]

Alessio Lomuscio, Hongyang Qu, and Franco Raimondi. 2017. MCMAS: an open-source model checker for the verification of multi-agent systems. Intl. Jrnl. on Software Tools for Technology Transfer 19, 1 (01 Feb 2017), 9--30.

[15]

Zohar Manna and Amir Pnueli. 1992. The Temporal Logic of Reactive and Concurrent Systems --- Specification. Springer.

[16]

Paul McNamara. 2018. Deontic Logic. The Stanford Encyclopedia of Philosophy (Fall 2018).

[17]

Amir Pnueli. 1977. The Temporal Logic of Programs. In Proceedings of the 18th IEEE Symposium Foundations of Computer Science. 46--57.

Digital Library

[18]

Cristian Prisacariu and Gerardo Schneider. 2012. A dynamic deontic logic for complex contracts. The Journal of Logic and Algebraic Programming 81, 4 (2012), 458 -- 490. Special Issue: NWPT 2009.

[19]

Franco Raimondi and Alessio Lomuscio. 2004. Automatic Verification of Deontic Interpreted Systems by Model Checking via OBDD's. In Procs. of the 16th European Conf. on Artificial Intelligence.

Digital Library

[20]

A. Rizaldi and M. Althoff. 2015. Formalising Traffic Rules for Accountability of Autonomous Vehicles. In 2015 IEEE 18th International Conference on Intelligent Transportation Systems. 1658--1665.

[21]

Shai Shalev-Shwartz, Shaked Shammah, and Amnon Shashua. 2018. On a Formal Model of Safe and Scalable Self-driving Cars. (October 2018). arXiv:1708.06374v6.

[22]

Wiebe van der Hoek and Michael Wooldridge. 2003. Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications. Studia Logica 75, 1 (01 Oct 2003), 125--157.

[23]

Georg H. von Wright. 1951. Deontic Logic. Mind 60, 237 (January 1951).

[24]

Shakiba Yaghoubi and Georgios Fainekos. 2019. Gray-box Adversarial Testing for Control Systems with Machine Learning Components (HSCC '19). ACM, New York, NY, USA, 6.

Cited By

Kharraz KAzzopardi SSchneider GLeucker M(2023)Synchronous Agents, Verification, and Blame—A Deontic ViewTheoretical Aspects of Computing – ICTAC 202310.1007/978-3-031-47963-2_20(332-350)Online publication date: 4-Dec-2023
https://dl.acm.org/doi/10.1007/978-3-031-47963-2_20
Shea-Blymyer CAbbas H(2021)Algorithmic Ethics: Formalization and Verification of Autonomous Vehicle ObligationsACM Transactions on Cyber-Physical Systems10.1145/34609755:4(1-25)Online publication date: 31-Oct-2021
https://dl.acm.org/doi/10.1145/3460975
Shea-Blymyer CAbbas H(2021)Learning a Robot's Social Obligations from Comparisons of Observed Behavior2021 IEEE International Conference on Advanced Robotics and Its Social Impacts (ARSO)10.1109/ARSO51874.2021.9542846(15-20)Online publication date: 8-Jul-2021
https://doi.org/10.1109/ARSO51874.2021.9542846

Index Terms

A deontic logic analysis of autonomous systems' safety
1. Computer systems organization
  1. Embedded and cyber-physical systems
    1. Robotics
      1. Robotic autonomy
2. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
  2. Modeling and simulation
    1. Model development and analysis
      1. Model verification and validation
      2. Modeling methodologies

Recommendations

Towards an Intuitionistic Deontic Logic Tolerating Conflicting Obligations
Logic, Language, Information, and Computation
Abstract
We propose a minimal deontic logic, called MIND, based on intuitionistic logic. This logic gives a very simple solution to handling conflicting obligations: the presence of two conflicting obligations does not entail the triviality of the set of ...
Extending a Defeasible Reasoner with Modal and Deontic Logic Operators
WI-IAT '08: Proceedings of the 2008 IEEE/WIC/ACM International Conference on Web Intelligence and Intelligent Agent Technology - Volume 03

Defeasible logic is a non-monotonic formalism that deals with incomplete and conflicting information. Modal logic deals with necessity and possibility, exhibiting defeasibility; thus, it is possible to combine defeasible logic with modal operators. This ...
Obligations and prohibitions in Talmudic deontic logic
Special issue on Deontic Logic and Normative Systems

This paper examines the deontic logic of the Talmud. We shall find, by looking: at examples, that at first approximation we need deontic logic with several connectives: O_TA Talmudic obligation F_TA Talmudic prohibition F_DA Standard deontic prohibition O_D...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '20: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control

April 2020

324 pages

ISBN:9781450370189

DOI:10.1145/3365365

Program Chairs:
Aaron Ames
California Institute of Technology
,
Sanjit A. Seshia
University of California, Berkeley
,
Publications Chair:
Jyotirmoy Deshmukh
University of Southern California

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 April 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Conference

HSCC '20

Sponsor:

SIGBED

HSCC '20: 23rd ACM International Conference on Hybrid Systems: Computation and Control

April 22 - 24, 2020

New South Wales, Sydney, Australia

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
195
Total Downloads

Downloads (Last 12 months)21
Downloads (Last 6 weeks)2

Reflects downloads up to 19 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kharraz KAzzopardi SSchneider GLeucker M(2023)Synchronous Agents, Verification, and Blame—A Deontic ViewTheoretical Aspects of Computing – ICTAC 202310.1007/978-3-031-47963-2_20(332-350)Online publication date: 4-Dec-2023
https://dl.acm.org/doi/10.1007/978-3-031-47963-2_20
Shea-Blymyer CAbbas H(2021)Algorithmic Ethics: Formalization and Verification of Autonomous Vehicle ObligationsACM Transactions on Cyber-Physical Systems10.1145/34609755:4(1-25)Online publication date: 31-Oct-2021
https://dl.acm.org/doi/10.1145/3460975
Shea-Blymyer CAbbas H(2021)Learning a Robot's Social Obligations from Comparisons of Observed Behavior2021 IEEE International Conference on Advanced Robotics and Its Social Impacts (ARSO)10.1109/ARSO51874.2021.9542846(15-20)Online publication date: 8-Jul-2021
https://doi.org/10.1109/ARSO51874.2021.9542846

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents