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.

翻译：自治代理正被日益提议用于医疗保健、辅助护理、教育及其他受复杂人本规范约束的应用场景。为确保符合这些规范，由其衍生出的规则需要被无歧义地定义、进行一致性检查，并用于代理的验证。本文提出一个框架，用于对自治代理的社会、法律、伦理、共情与文化（SLEEC）规则进行形式化规约、验证与确认。该框架包含：（i）一种用于规约SLEEC规则及其规则失效条件（即规则不适用或需要替代规则形式的情形）的语言；（ii）该语言的形式化语义（在进程代数tock-CSP中定义）；以及（iii）用于检测规则集中的冲突与冗余，并验证自治代理符合此类规则的方法。我们通过两个不同领域的自治代理——消防无人机与辅助穿衣机器人——展示了该框架的适用性。