Towards Verifiably Ethical Robot Behaviour

Ensuring that autonomous systems work ethically is both complex and difficult. The idea of having an additional 'governor' that assesses the options the system has, and prunes them to select the most ethical choices, is well understood. Recent work has produced such a governor consisting of a 'consequence engine' that assesses the likely future outcomes of actions then applies a Safety/Ethical logic to select actions. Although this is appealing, it is impossible to be certain that the most ethical options are actually taken. The paper extends and applies a well-known agent verification approach to this consequence engine checking that, whenever the robot believes a human is in danger and a safe path exists, the human never comes to harm. The consequence engine is also verified in isolation, proving it captures the intended order of ethical priorities. This work lays the foundation for a declarative, executable language for expressing ethical consequence engines and thereby opens the path to a system for implementing verifiable ethical consequence engines which may be interfaced to arbitrary robotic systems. The language presented is simple, prioritising first over individuals and then over outcomes, unable to distinguish contexts or to reason that an action may lead into a situation where the only available subsequent actions are unethical, and presumes that suitable ethical priorities have already been externally decided.