An important issue in deploying an autonomous system is how to enable human users and stakeholders to develop an appropriate level of trust in the system. It has been argued that a crucial mechanism to enable appropriate trust is the ability of a system to explain its behaviour. Obviously, such explanations need to be comprehensible to humans. Due to the perceived similarity in functioning between humans and autonomous systems, we argue that it makes sense to build on the results of extensive research in social sciences that explores how humans explain their behaviour. Using similar concepts for explanation is argued to help with comprehensibility, since the concepts are familiar. Following work in the social sciences, we propose the use of a folk-psychological model that utilises beliefs, desires, and ``valuings''. We propose a formal framework for constructing explanations of the behaviour of an autonomous system, present an (implemented) algorithm for giving explanations, and present evaluation results.

Abstract 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.

Autonomous agents are increasingly required to be able to make moral decisions. In these situations, the agent should be able to reason about the ethical bases of the decision and explain its decision in terms of the moral values involved. This is of special importance when the agent is interacting with a user and should understand the value priorities of the user in order to provide adequate support. This paper presents a model of agent behavior that takes into account user preferences and moral values.

Agent systems are used for a wide range of applications, and techniques to detect and avoid defects in such systems are valuable. In particular, it is desirable to detect issues as early as possible in the software development lifecycle. We describe a technique for checking the plan structures of a BDI agent design against the requirements models, specified in terms of scenarios and goals. This approach is applicable at design time, not requiring source code. A lightweight evaluation demonstrates that a range of defects can be found using this technique.

Before deploying a software system we need to assure ourselves (and stakeholders) that the system will behave correctly. This assurance is usually done by testing the system. However, it is intuitively obvious that adaptive systems, including agent-based systems, can exhibit complex behaviour, and are thus harder to test. In this paper we examine this "obvious intuition" in the case of Belief-Desire-Intention (BDI) agents. We analyse the size of the behaviour space of BDI agents and show that although the intuition is correct, the factors that influence the size are not what we expected them to be. Specifically, we found that the introduction of failure handling had a much larger effect on the size of the behaviour space than we expected. We also discuss the implications of these findings on the testability of BDI agents.

One approach to moderating the expected behaviour of agents in open societies is the use of explicit languages for defining norms, conditional commitments and/or social expectations, together with infrastructure supporting conformance checking. This article presents a logical account of the fulfilment and violation of social expectations modelled as conditional rules over a hybrid linear propositional temporal logic. Our semantics captures the intuition that the fulfilment or violation of an expectation must be determined without recourse to information from later states.We define a means of updating expectations from one state to the next based on formula progression, and show how conformance checking was implemented by combining the MCFULLmodel checking algorithm of Franceschet and de Rijke and the semantics for LTL over truncated paths proposed by Eisner et al. We present algorithms for both traditional offline model checking, where the complete model is available at once, and online model checking, where states are added to the model sequentially at runtime.

Goals are central to the design and implementation of intelligent software agents. Much of the literature on goals and reasoning about goals only deals with a limited set of goal types, typically achievement goals, and sometimes maintenance goals; and much of the work on interactions between goals only deals with achievement goals. We aim at extending a previously proposed unifying framework for goals with additional richer goal types, including a combined “achieve and maintain” goal type. We propose to provide an operationalization of these new goal types, proving that the operationalization meets desired properties.

A critical issue in software maintenance and evolution is change propagation: given a primary change that is made in order to meet a new or changed requirement, what additional, secondary, changes are needed? We have previously developed techniques for effectively supporting change propagation within design models of intelligent agent systems. In this paper, we propose how this approach is applied to support change propagation within UML design models. Our approach offers a number of advantages in terms of saving substantial time writing hard-coded rules, ensuring soundness and completeness, and at the same time capturing the cascading nature of change propagation. We will also present and discuss the results of an evaluation performed to assess the scalability of our approach.

Service discovery approaches, which mainly use keyword matching of service descriptions, have a low matching precision. This paper proposes an approach to increasing the matching precision by using services' functional contexts during the matching process. To enable a precise functional context matching, both the services' goals and the domain semantics are considered. For that purpose, we introduce the concept of functional substitutability and the proposed context matching technique uses this concept to match the underlying constraints of the functional contexts. Compared to the keyword-based context matching approach, simulation experiments showed that the (context retrieval) precision using the devised matching approach is much better and more stable against query semantic mutations.

Achieving confidence in the correctness, completeness and consistency of requirements specifications can be problematic and the consequences of incorrect requirements can be costly. In this paper we argue that specification and animation can provide reasonably high levels of assurance in the requirements without the overheads of using general purpose theorem proving tools. We propose a framework based on mode analysis and the operational semantics of logic programs for animating specifications. The framework allows us to combine prototyping and limited forms of automated deduction to increase our levels of confidence in specifications. Finally, we show how such a framework can be used to increase the level of confidence in the correctness of a simple dependency management system specification written in Z.

In this paper we demonstrate how light weight tools can be used to increase the level of confidence in Z specifications. In particular we outline the Pipedream approach to exploring Z specifications through animation, and illustrate the range of analyses that can be performed. We argue that, while a light weight approach does not give the same levels of assurance that an automated reasoning system would, it does give levels of assurance which are adequate for most projects and with significantly less overhead. We illustrate how animation can be used to perform verification using the example of a simple dependency management system.