Specification, validation and verification of social, legal, ethical, empathetic and cultural requirements for autonomous agents

TY - JOUR

T1 - Specification, validation and verification of social, legal, ethical, empathetic and cultural requirements for autonomous agents

AU - Getir Yaman, Sinem

AU - Ribeiro, Pedro

AU - Cavalcanti, Ana

AU - Calinescu, Radu

AU - Paterson, Colin

AU - Townsend, Beverley

N1 - © 2024 The Authors

PY - 2025/2/1

Y1 - 2025/2/1

N2 - Autonomous agents are increasingly being proposed for use in healthcare, assistive care, education, and other applications governed by complex human-centric norms. To ensure compliance with these norms, the rules they induce need to be unambiguously defined, checked for consistency, and used to verify the agent. In this paper, we introduce a framework for formal specification, validation and verification of social, legal, ethical, empathetic and cultural (SLEEC) rules for autonomous agents. Our framework comprises: (i) a language for specifying SLEEC rules and rule defeaters (that is, circumstances in which a rule does not apply or an alternative form of the rule is required); (ii) a formal semantics (defined in the process algebra tock-CSP) for the language; and (iii) methods for detecting conflicts and redundancy within a set of rules, and for verifying the compliance of an autonomous agent with such rules. We show the applicability of our framework for two autonomous agents from different domains: a firefighter UAV, and an assistive-dressing robot.

AB - Autonomous agents are increasingly being proposed for use in healthcare, assistive care, education, and other applications governed by complex human-centric norms. To ensure compliance with these norms, the rules they induce need to be unambiguously defined, checked for consistency, and used to verify the agent. In this paper, we introduce a framework for formal specification, validation and verification of social, legal, ethical, empathetic and cultural (SLEEC) rules for autonomous agents. Our framework comprises: (i) a language for specifying SLEEC rules and rule defeaters (that is, circumstances in which a rule does not apply or an alternative form of the rule is required); (ii) a formal semantics (defined in the process algebra tock-CSP) for the language; and (iii) methods for detecting conflicts and redundancy within a set of rules, and for verifying the compliance of an autonomous agent with such rules. We show the applicability of our framework for two autonomous agents from different domains: a firefighter UAV, and an assistive-dressing robot.

KW - Autonomous agents

KW - Formal methods

KW - Social, legal, ethical, empathetic and cultural requirements

KW - Sociotechnical systems

KW - Verification and validation

UR - http://www.scopus.com/inward/record.url?scp=85208655817&partnerID=8YFLogxK

U2 - 10.1016/j.jss.2024.112229

DO - 10.1016/j.jss.2024.112229

M3 - Article

AN - SCOPUS:85208655817

SN - 0164-1212

VL - 220

JO - Journal of Systems and Software

JF - Journal of Systems and Software

M1 - 112229

ER -