Specification, Validation and Verification of Social, Legal, Ethical, Empathetic and Cultural Requirements for Autonomous Agents

TL;DR

This paper presents a comprehensive framework for formally specifying, validating, and verifying social, legal, ethical, empathetic, and cultural requirements in autonomous agents to ensure their compliance with complex human norms.

Contribution

It introduces a novel language, formal semantics, and methods for conflict detection and verification of SLEEC rules in autonomous agents.

Findings

Framework successfully applied to firefighter UAV and assistive-dressing robot

Effective detection of rule conflicts and redundancies

Verification of agent compliance with complex norms

Abstract

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.