Trusted Autonomous Systems

完全自主的系统就在这里。在过去的50年里，我们已经迅速从操作员完全控制系统（例如，挖掘机）的控制系统，发展到遵循人类指令的监督系统（例如，自动缝纫机），再到在没有人类控制的情况下执行一系列复杂操作的自动系统（例如，今天的机器人汽车装配线），再到自主系统。自治系统（Autonomous systems， AS）是一种高度自适应的系统，能够感知环境并学会对自己的行为做出决策，在达到一定目标的过程中表现出高度的主动性。它们是自主的，因为它们不需要人类的存在来操作，尽管它们可能与人类或其他自主系统进行沟通、合作和协商，以达到它们的目标。该奖学金的目标是发展自主系统的科学和工程基础，使其成为我们日常生活的一部分。如果重复或危险的任务由机器来完成，对社会来说显然是有好处的。然而，在媒体和公众中，对于日益复杂的技术在我们生活的关键方面的帮助，存在着一种明显的抵制。这些担忧是有道理的。大多数人都有过软件和自动设备不能正常工作的亲身经历；为什么他们要愿意把他们需要的关键方面委托给他们？英国皇家工程院（Royal Academy of Engineering）在2009年8月发表了一份有影响力的报告，并在媒体上广泛讨论。报告认为，除非解决有关法律、伦理、社会和监管方面的紧迫问题，否则这些技术将不会投入使用，这是一种真正的危险。例如，该报告强调了无人驾驶汽车发生碰撞时的责任问题。谁应该对此负责？乘客?这个软件吗?老板吗?汽车制造商是谁？很明显，社会和政府需要就其中一些问题进行成熟的辩论。然而，该报告指出了一个更根本的问题：“谁将负责自动系统的认证？”[英国皇家学会，自治系统，2009年8月，第4页]虽然这个问题有复杂的监管方面，但其潜在的科学含义是，作为计算机科学家和工程师，我们迫切需要提供社会技术，以便能够验证和证明自治系统按照预期的方式运行。为了实现这一目标，确定了四个研究目标：1)为AS的原则规范制定基于逻辑的语言，包括关键属性，如容错性，可诊断性，弹性等。2)开发有效的模型检查技术，包括基于AS的抽象，参数化和并行模型检查，以验证AS。3)用于用例认证的自主系统的最先进模型检查器的构建和开源发布。4)这些技术在三个具有近期和中期社会重要性的关键领域得到验证：自动驾驶汽车、服务和电子医疗。该奖学金旨在追求计算逻辑中的新技术，以回答上述技术挑战。这些领域的成功将为AS的验证开辟道路，从而为其认证在社会上的主流使用开辟道路。

Fully autonomous systems are here. In the past 50 years we have quickly moved from controlled systems, where the operator has full control on the actions of the system (e.g., a digger), to supervised systems that follow human instructions (e.g., automated sewing machines), to automatic systems performing a series of sophisticated operations without human control (e.g., today's robotic car assembly lines), to autonomous systems. Autonomous systems (AS) are highly adaptive systems that sense the environment and learn to make decisions on their actions displaying a high degree of pro-activeness in reaching a certain objective. They are autonomous in the sense that they do not need the presence of a human to operate, although they may communicate, cooperate, and negotiate with them or fellow autonomous systems to reach their goals.The objective of this fellowship is to develop the scientific and engineering underpinnings for autonomous systems to become part of our every-day's life. There is a clear benefit for society if repetitive or dangerous tasks are performed by machines. Yet, there is a perceived resistance in the media and the public at large to increasingly sophisticated technology assisting key aspects of our lives. These concerns are justified. Most people have first hand experience of software and automatic devices not performing as they should; why should they be willing to delegate to them crucial aspects of their needs?In a recent influential report published by the Royal Academy of Engineering in August 2009 and widely discussed in the media it is argued that there is a real danger that these technologies will not be put into use unless urgent questions about the legal, ethical, social, and regulatory implications are addressed. For instance, the report highlights the issue of liability in case of collisions between autonomous driverless cars. Who should be held responsible? The passenger? The software? The owner? The maker of the vehicle? Quite clearly society and the government need to engage in a maturedebate on several of these issues. However, the report identifies an even more fundamental point:``Who will be responsible for certification of autonomous systems? [Royal Society, Autonomous Systems, August 2009, page 4]While there are complex regulatory aspects to this question, its underlying scientific implication is that we, as computer scientists and engineers, urgently need to offer society techniques to be able to verify and certify that autonomous systems behave as they are intended to. To achieve this, four research objectives are identified:1) The formulation of logic-based languages for the principled specification of AS, including key properties such as fault-tolerance, diagnosability, resilience, etc.2) The development of efficient model checking techniques, including AS-based abstraction, parametric and parallel model checking, for the verification of AS. 3) The construction and open source release of a state-of-the-art model checker for autonomous systems to be used for use-cases certifications.4) The validation of these techniques in three key areas of immediate and mid-term societal importance: autonomous vehicles, services, and e-health.This fellowship intends to pursue novel techniques in computational logic to answer the technical challenges above. A success in these areas will open the way for the verification of AS, thereby opening the way to their certification for mainstream use in society.