Michael Winikoff

Michael Winikoff, John Thangarajah, Sebastian Rodriguez

Explainability is important for the transparency of autonomous and intelligent systems and for helping to support the development of appropriate levels of trust. There has been considerable work on developing approaches for explaining systems and there are standards that specify requirements for transparency. However, there is a gap: the standards are too high-level and do not adequately specify requirements for explainability. This paper develops a scoresheet that can be used to specify explainability requirements or to assess the explainability aspects provided for particular applications. The scoresheet is developed by considering the requirements of a range of stakeholders and is applicable to Multiagent Systems as well as other AI technologies. We also provide guidance for how to use the scoresheet and illustrate its generality and usefulness by applying it to a range of applications.

Michael Fisher, Viviana Mascardi, Kristin Yvonne Rozier et al.

A computational system is called autonomous if it is able to make its own decisions, or take its own actions, without human supervision or control. The capability and spread of such systems have reached the point where they are beginning to touch much of everyday life. However, regulators grapple with how to deal with autonomous systems, for example how could we certify an Unmanned Aerial System for autonomous use in civilian airspace? We here analyse what is needed in order to provide verified reliable behaviour of an autonomous system, analyse what can be done as the state-of-the-art in automated verification, and propose a roadmap towards developing regulatory guidelines, including articulating challenges to researchers, to engineers, and to regulators. Case studies in seven distinct domains illustrate the article.

Michael Winikoff

Formal software verification uses mathematical techniques to establish that software has certain properties. For example, that the behaviour of a software system satisfies certain logically-specified properties. Formal methods have a long history, but a recurring assumption is that the properties to be verified are known, or provided as part of the requirements elicitation process. This working note considers the question: where do the verification properties come from? It proposes a process for systematically identifying verification properties.

Michael Winikoff

In this talk I review where we stand regarding the engineering of multi-agent systems. There is both good news and bad news. The good news is that over the past decade we've made considerable progress on techniques for engineering multi-agent systems: we have good, usable methodologies, and mature tools. Furthermore, we've seen a wide range of demonstrated applications, and have even begun to quantify the advantages of agent technology. However, industry involvement in AAMAS appears to be declining (as measured by industry sponsorship of the conference), and industry affiliated attendants at AAMAS 2012 were few (1-2%). Furthermore, looking at the applications of agents being reported at recent AAMAS, usage of Agent Oriented Software Engineering (AOSE) and of Agent Oriented Programming Languages (AOPLs) is quite limited. This observation is corroborated by the results of a 2008 survey by Frank and Virginia Dignum. Based on these observations, I make five recommendations: (1) Re-engage with industry; (2) Stop designing AOPLs and AOSE methodologies ... and instead ... (3) Move to the "macro" level: develop techniques for designing and implementing interaction, integrate micro (single cognitive agent) and macro (MAS) design and implementation; (4) Develop techniques for the Assurance of MAS; and (5) Re-engage with the US.