• a novel segmentation-based approach to estimate intention of a mobile agent. • an efficient implementation of a new segmentation-based algorithm for continues or realtime intention recognition. • evaluation of the latency, stability, and accuracy of the proposed algorithm compared to other state-of-the-art online intention algorithms. This paper proposes and evaluates an efficient online algorithm for recognizing the movement intentions of mobile agents. As an agent reveals new movements, our algorithm continuously ranks various possible intentions, such as reaching a specific destination or avoiding a particular area, using a novel approach to semantic trajectory segmentation. We empirically validate the performance of our algorithm against state-of-the-art alternatives in the path planning using simulated movement data. The results show that our approach improves reliability and accuracy in identifying true intention in scenarios with an increased number of candidate destinations, or when a mobile agent takes less planned and predictable routes.

Goal recognition (GR) involves inferring an agent's unobserved goal from a sequence of observations. This is a critical problem in AI with diverse applications. Traditionally, GR has been addressed using 'inference to the best explanation' or abduction, where hypotheses about the agent's goals are generated as the most plausible explanations for observed behavior. Alternatively, some approaches enhance interpretability by ensuring that an agent's behavior aligns with an observer's expectations or by making the reasoning behind decisions more transparent. In this work, we tackle a different challenge: explaining the GR process in a way that is comprehensible to humans. We introduce and evaluate an explainable model for goal recognition (GR) agents, grounded in the theoretical framework and cognitive processes underlying human behavior explanation. Drawing on insights from two human-agent studies, we propose a conceptual framework for human-centered explanations of GR. Using this framework, we develop the eXplainable Goal Recognition (XGR) model, which generates explanations for both why and why not questions. We evaluate the model computationally across eight GR benchmarks and through three user studies. The first study assesses the efficiency of generating human-like explanations within the Sokoban game domain, the second examines perceived explainability in the same domain, and the third evaluates the model's effectiveness in aiding decision-making in illegal fishing detection. Results demonstrate that the XGR model significantly enhances user understanding, trust, and decision-making compared to baseline models, underscoring its potential to improve human-agent collaboration.

High-stakes algorithmic decisions should be contestable, yet there is limited guidance on how to design for contestability, resulting in inadequate contestation processes. Using an algorithmic university admissions decision scenario, we investigate what type of review process people prefer when contesting algorithmic decisions. Through a choice-based conjoint experiment, we explore review process preferences, asking participants to choose their preferred review process from a choice of two that differ across five design attributes: who the reviewer is, how independent the review is, the ability to communicate with the reviewer, the style of the review, and how much the review costs. Expanding on existing studies that focus on the perspective of the decision subject, we introduce eight different scenario perspectives to explore the extent to which particular design attributes matter to different stakeholders. People consistently prefer human reviewers who can make fresh decisions and communicate directly, while also prioritising affordable review processes. These findings highlight the importance of human involvement and cost-effectiveness in review processes. While the impact of perspective was relatively small, our qualitative analysis reveals important underlying tensions between efficiency, fairness, and individual needs. These subtle variations underscore the complexity of designing universally acceptable review processes. We propose design considerations that can help decision-makers to design review processes that are tailored to the specific decision-making context.

We consider the effectiveness of multiobjective counterfactual explanations (MOCEs) in helping individuals learntactics, or rules of thumb, to apply when required to select a course of action in a specific context. In this setting, a counterfactual explanation compares one course of action against another. A MOCE presents this comparison by highlighting how the two options differ across a range of objectives or metrics. We conduct a study in which participants are presented with various scenarios alongside courses of action that could be implemented in those scenarios. Counterfactual explanations, including those involving multiple objectives, are used to identify the positive and negative aspects of the provided options. Participants were then required to identify the best course of action in various contexts. Participants trained with MOCE outperformed those given no explanations in seven of eight scenarios and those given single-objective counterfactual explanations (SOCEs) in four. SOCEs gave participants an aggregated outcome (expected rewards) without breaking these into specific objectives. MOCE improved tactic learning, but participants provided with SOCE or no explanation performed better in multitactic scenarios. These findings suggest that MOCE enhances tactical decision-making, but further research is needed for multitactic integration.

In this article, we introduce and evaluate a tool for researchers and practitioners to assess the actionability of information provided to users to support algorithmic recourse. While there are clear benefits of recourse from the user’s perspective, the notion of actionability in explainable AI research remains vague, and claims of ‘actionable’ explainability techniques are based on researchers’ intuitions. Inspired by definitions and instruments for assessing actionability in other domains, we construct a seven-item tool and investigate its effectiveness through two user studies. We show that the tool discriminates actionability across explanation types and that the distinctions align with human judgments. We illustrate the impact of context on actionability assessments, suggesting that domain-specific tool adaptations may foster more human-centred algorithmic systems. This is a valuable step forward for research and practices into actionable explainability and algorithmic recourse, providing the first clear human-centred tool for assessing actionability in explainable AI.

Prior research on AI-assisted human decision-making has explored several different explainable AI (XAI) approaches. A recent paper has proposed a paradigm shift calling for hypothesis-driven XAI through a conceptual framework called evaluative AI that gives people evidence that supports or refutes hypotheses without necessarily giving a decision-aid recommendation. In this paper, we describe and evaluate an approach for hypothesis-driven XAI based on the Weight of Evidence (WoE) framework, which generates both positive and negative evidence for a given hypothesis. Through human behavioural experiments, we show that our hypothesis-driven approach increases decision accuracy and reduces reliance compared to a recommendation-driven approach and an AI-explanation-only baseline, but with a small increase in under-reliance compared to the recommendation-driven approach. Further, we show that participants used our hypothesis-driven approach in a materially different way to the two baselines.

Displaying confidence scores in human-AI interaction has been shown to help build trust between humans and AI systems. However, most existing research uses only the confidence score as a form of communication. As confidence scores are just another model output, users may want to understand why the algorithm is confident to determine whether to accept the confidence score. In this paper, we show that counterfactual explanations of confidence scores help study participants to better understand and better trust a machine learning model's prediction. We present two methods for understanding model confidence using counterfactual explanation: (1) based on counterfactual examples; and (2) based on visualisation of the counterfactual space. Both increase understanding and trust for study participants over a baseline of no explanation, but qualitative results show that they are used quite differently, leading to recommendations of when to use each one and directions of designing better explanations.

Analogical reasoning enables agents to extract relevant information from scenes, and efficiently navigate them in familiar ways. While progressive-matrix problems (PMPs) are becoming popular for the development and evaluation of analogical reasoning in computer vision, we argue that the dominant methodology in this area struggles to expose the lack of meaningful generalisation in solvers, and rein-forces an objectivist stance on perception - that objects can only be seen one way - which we believe to be counter-productive. In this paper, we introduce the Unicode Analogies challenge, consisting of polysemic, character-based PMPs to benchmark fluid conceptualisation ability in vision systems. Writing systems have evolved characters at multiple levels of abstraction, from iconic through to symbolic representations, producing both visually interrelated yet exceptionally diverse images when compared to those exhibited by existing PMP datasets. Our framework has been designed to challenge models by presenting tasks much harder to complete without robust feature extraction, while remaining largely solvable by human participants. We therefore argue that Unicode Analogies elegantly captures and tests for a facet of human visual reasoning that is severely lacking in current-generation AI.

Diverse, top-k, and top-quality planning are concerned with the generation of sets of solutions to sequential decision problems. Previously this area has been the domain of classical planners that require a symbolic model of the problem instance. This paper proposes a novel alternative approach that uses Monte Carlo Tree Search (MCTS), enabling application to problems for which only a black-box simulation model is available. We present a procedure for extracting bounded sets of plans from pre-generated search trees in best-first order, and a metric for evaluating the relative quality of paths through a search tree. We demonstrate this approach on a path-planning problem with hidden information, and suggest adaptations to the MCTS algorithm to increase the diversity of generated plans. Our results show that our method can generate diverse and high-quality plan sets in domains where classical planners are not applicable.

Deep reinforcement learning has shown useful in the field of robotics but the black-box nature of deep neural networks impedes the applicability of deep reinforcement learning agents for real-world tasks. This is addressed in the field of explainable artificial intelligence, by developing explanation methods that aim to explain such agents to humans. Model trees as surrogate models have proven useful for producing explanations for black-box models used in real-world robotic applications, in particular, due to their capability of providing explanations in real time. In this paper, we provide an overview and analysis of available methods for building model trees for explaining deep reinforcement learning agents solving robotics tasks. We find that multiple outputs are important for the model to be able to grasp the dependencies of coupled output features, i.e. actions. Additionally, our results indicate that introducing domain knowledge via a hierarchy among the input features during the building process results in higher accuracies and a faster building process.

In this article, we show that explanations of decisions made by machine learning systems can be improved by not only explaining why a decision was made but also explaining how an individual could obtain their desired outcome. We formally define the concept of directive explanations (those that offer specific actions an individual could take to achieve their desired outcome), introduce two forms of directive explanations (directive-specific and directive-generic), and describe how these can be generated computationally. We investigate people’s preference for and perception toward directive explanations through two online studies, one quantitative and the other qualitative, each covering two domains (the credit scoring domain and the employee satisfaction domain). We find a significant preference for both forms of directive explanations compared to non-directive counterfactual explanations. However, we also find that preferences are affected by many aspects, including individual preferences and social factors. We conclude that deciding what type of explanation to provide requires information about the recipients and other contextual information. This reinforces the need for a human-centered and context-specific approach to explainable AI.

If you were significantly impacted by an algorithmic decision, how would you want the decision to be reviewed? In this study, we explore perceptions of review processes for algorithmic decisions that differ across three dimensions: the reviewer, how the review is conducted, and how long the review takes. Using a choice-based conjoint analysis we find that people prefer review processes that provide for human review, the ability to participate in the review process, and a timely outcome. Using a survey, we find that people also see human review that provides for participation to be the fairest review process. Our qualitative analysis indicates that the fairest review process provides the greatest likelihood of a favourable outcome, an opportunity for the decision subject and their situation to be fully and accurately understood, human involvement, and dignity. These findings have implications for the design of contestation procedures and also the design of algorithmic decision-making processes.

In this paper, we present a novel approach to epistemic planning called planning with perspectives (PWP) that is both more expressive and computationally more efficient than existing state-of-the-art epistemic planning tools. Epistemic planning — planning with knowledge and belief — is essential in many multi-agent and human-agent interaction domains. Most state-of-the-art epistemic planners solve epistemic planning problems by either compiling to propositional classical planning (for example, generating all possible knowledge atoms or compiling epistemic formulae to normal forms); or explicitly encoding Kripke-based semantics. However, these methods become computationally infeasible as problem sizes grow. In this paper, we decompose epistemic planning by delegating reasoning about epistemic formulae to an external solver. We do this by modelling the problem using Functional STRIPS, which is more expressive than standard STRIPS and supports the use of external, black-box functions within action models. Building on recent work that demonstrates the relationship between what an agent ‘sees’ and what it knows, we define the perspective of each agent using an external function, and build a solver for epistemic logic around this. Modellers can customise the perspective function of agents, allowing new epistemic logics to be defined without changing the planner. We ran evaluations on well-known epistemic planning benchmarks to compare an existing state-of-the-art planner, and on new scenarios that demonstrate the expressiveness of the PWP approach. The results show that our PWP planner scales significantly better than the state-of-the-art planner that we compared against, and can express problems more succinctly.

Convolutional neural network (CNN) models for computer vision are powerful but lack explainability in their most basic form. This deficiency remains a key challenge when applying CNNs in important domains. Recent work on explanations through feature importance of approximate linear models has moved from input-level features (pixels or segments) to features from mid-layer feature maps in the form of concept activation vectors (CAVs). CAVs contain concept-level information and could be learned via clustering. In this work, we rethink the ACE algorithm of Ghorbani et~al., proposing an alternative invertible concept-based explanation (ICE) framework to overcome its shortcomings. Based on the requirements of fidelity (approximate models to target models) and interpretability (being meaningful to people), we design measurements and evaluate a range of matrix factorization methods with our framework. We find that non-negative concept activation vectors (NCAVs) from non-negative matrix factorization provide superior performance in interpretability and fidelity based on computational and human subject experiments. Our framework provides both local and global concept-level explanations for pre-trained CNN models.

In most multiagent applications, communication is essential among agents to coordinate their actions and achieve their goals. However, communication often has a related cost that affects overall system performance. In this paper, we draw inspiration from epistemic planning studies to develop a communication model for agents that allows them to cooperate and make communication decisions effectively within a planning task. The proposed model treats a communication process as an action that modifies the epistemic state of the team. We evaluate whether agents can cooperate effectively and achieve higher performance using communication protocol modeled in our epistemic planning framework in two simulated tasks. Based on an empirical study conducted using search and rescue tasks with different scenarios, our results show that the proposed model improved team performance across all scenarios than baseline models.

Eye gaze has the potential to provide insight into the minds of individuals, and this idea has been used in prior research to improve human goal recognition by combining human's actions and gaze. However, most existing research assumes that people are rational and honest. In adversarial scenarios, people may deliberately alter their actions and gaze, which presents a challenge to goal recognition systems. In this paper, we present new models for goal recognition under deception using a combination of gaze behaviour and observed movements of the agent. These models aim to detect when a person is deceiving by analysing their gaze patterns and use this information to adjust the goal recognition. We evaluated our models in two human-subject studies: (1) using data collected from 30 individuals playing a navigation game inspired by an existing deception study and (2) using data collected from 40 individuals playing a competitive game (Ticket To Ride). We found that one of our models (Modulated Deception Gaze+Ontic) offers promising results compared to the previous state-of-the-art model in both studies. Our work complements existing adversarial goal recognition systems by equipping these systems with the ability to tackle ambiguous gaze behaviours.

As the use of algorithmic systems in high-stakes decision-making increases, the ability to contest algorithmic decisions is being recognised as an important safeguard for individuals. Yet, there is little guidance on what `contestability'--the ability to contest decisions--in relation to algorithmic decision-making requires. Recent research presents different conceptualisations of contestability in algorithmic decision-making. We contribute to this growing body of work by describing and analysing the perspectives of people and organisations who made submissions in response to Australia's proposed `AI Ethics Framework', the first framework of its kind to include `contestability' as a core ethical principle. Our findings reveal that while the nature of contestability is disputed, it is seen as a way to protect individuals, and it resembles contestability in relation to human decision-making. We reflect on and discuss the implications of these findings.

Epistemic planning can be used to achieve implicit coordination in cooperative multi-agent settings where knowledge and capabilities are distributed between the agents. In these scenarios, agents plan and act on their own without having to agree on a common plan or protocol beforehand. However, epistemic planning is undecidable in general. In this paper, we show how implicit coordination can be achieved in a simpler, propositional setting by using nondeterminism as a means to allow the agents to take the other agents' perspectives. We identify a decidable fragment of epistemic planning that allows for arbitrary initial state uncertainty and non-determinism, but where actions can never increase the uncertainty of the agents. We show that in this fragment, planning for implicit coordination can be reduced to a version of fully observable nondeterministic (FOND) planning and that it thus has the same computational complexity as FOND planning. We provide a small case study, modeling the problem of multi-agent path finding with destination uncertainty in FOND, to show that our approach can be successfully applied in practice.

Prominent theories in cognitive science propose that humans understand and represent the knowledge of the world through causal relationships. In making sense of the world, we build causal models in our mind to encode cause-effect relations of events and use these to explain why new events happen by referring to counterfactuals — things that did not happen. In this paper, we use causal models to derive causal explanations of the behaviour of model-free reinforcement learning agents. We present an approach that learns a structural causal model during reinforcement learning and encodes causal relationships between variables of interest. This model is then used to generate explanations of behaviour based on counterfactual analysis of the causal model. We computationally evaluate the model in 6 domains and measure performance and task prediction accuracy. We report on a study with 120 participants who observe agents playing a real-time strategy game (Starcraft II) and then receive explanations of the agents' behaviour. We investigate: 1) participants' understanding gained by explanations through task prediction; 2) explanation satisfaction and 3) trust. Our results show that causal model explanations perform better on these measures compared to two other baseline explanation models.

OBJECTIVE: To conduct a systematic scoping review of explainable artificial intelligence (XAI) models that use real-world electronic health record data, categorize these techniques according to different biomedical applications, identify gaps of current studies, and suggest future research directions. MATERIALS AND METHODS: We searched MEDLINE, IEEE Xplore, and the Association for Computing Machinery (ACM) Digital Library to identify relevant papers published between January 1, 2009 and May 1, 2019. We summarized these studies based on the year of publication, prediction tasks, machine learning algorithm, dataset(s) used to build the models, the scope, category, and evaluation of the XAI methods. We further assessed the reproducibility of the studies in terms of the availability of data and code and discussed open issues and challenges. RESULTS: Forty-two articles were included in this review. We reported the research trend and most-studied diseases. We grouped XAI methods into 5 categories: knowledge distillation and rule extraction (N = 13), intrinsically interpretable models (N = 9), data dimensionality reduction (N = 8), attention mechanism (N = 7), and feature interaction and importance (N = 5). DISCUSSION: XAI evaluation is an open issue that requires a deeper focus in the case of medical applications. We also discuss the importance of reproducibility of research work in this field, as well as the challenges and opportunities of XAI from 2 medical professionals' point of view. CONCLUSION: Based on our review, we found that XAI evaluation in medicine has not been adequately and formally practiced. Reproducibility remains a critical concern. Ample opportunities exist to advance XAI research in medicine.

In autonomous multiagent or multirobotic systems, the ability to quickly and accurately respond to threats and uncertainties is important for both mission outcomes and survivability. Such systems are never truly autonomous, often operating as part of a human-agent team. Artificial intelligent agents (IAs) have been proposed as tools to help manage such teams; e.g., proposing potential courses of action to human operators. However, they are often underutilized due to a lack of trust. Designing transparent agents, who can convey at least some information regarding their internal reasoning processes, is considered an effective method of increasing trust. How people interact with such transparency information to gain situation awareness while avoiding information overload is currently an unexplored topic. In this article, we go part way to answering this question, by investigating two forms of transparency: sequential transparency, which requires people to step through the IA's explanation in a fixed order; and demand-driven transparency, which allows people to request information as needed. In an experiment using a multivehicle simulation, our results show that demand-driven interaction improves the operators' trust in the system while maintaining, and at times improving, performance and usability.

Requirements engineering involves the elicitation, representation and communication of diverse stakeholder needs. However, this can be particularly challenging when developing technology embedded within complex social systems. So-called socially-oriented requirements can be abstract, ambiguous and driven by the organisational, cultural and political contexts of the stakeholders involved. Motivational models are one solution which supports project-wide understanding of the key goals of stakeholders. Yet, there is still a lack of understanding about the role they can play in larger industrial projects. We present our use of motivational modelling in an Australia-wide project that develops new technology to assist people who are homeless in accessing service providers. We interviewed 100 stakeholders and utilised motivational models to advocate for the needs of key stakeholder groups. We discuss the benefits, challenges and lessons learned.

The Theory of Mind provides a framework for an agent to predict the actions of adversaries by building an abstract model of their strategies using recursive nested beliefs. In this paper, we extend a recently introduced technique for opponent modeling based on Theory of Mind reasoning. Our extended multi-agent Theory of Mind model explicitly considers multiple opponents simultaneously. We introduce a stereotyping mechanism, which segments the agent population into sub-groups of agents with similar behavior. Here, sub-group profiles guide decision making in place of individual agent profiles. We evaluate our model using a multi-player stochastic game, which presents agents with the challenge of unknown adversaries in a partially-observable environment. Simulation results demonstrate that the model performs well under uncertainty and that stereotyping allows larger groups of agents to be modeled robustly. The findings strengthen results showing that Theory of Mind modeling is useful in many artificial intelligence applications.

The automatic generation of realistic behavior such as tactical intercepts for Unmanned Aerial Vehicles (UAV) in air combat is a challenging problem. State-of-the-art solutions propose hand-crafted algorithms and heuristics whose performance depends heavily on the initial conditions and specific aerodynamic characteristics of the UAVs involved. This demo shows the ability of domain-independent planners, embedded into simulators, to generate on-line, feed-forward, control signals that steer simulated aircraft as best suits the situation.

Dynamic Symbolic Execution (DSE) is a technique to automatically generate test inputs by executing a program with concrete and symbolic values simultaneously. A key challenge in DSE is scalability; executing all feasible program paths is not possible, owing to the potentially exponential or infinite number of paths. Loops are a main source of path explosion, in particular where the number of iterations depends on a program's input. Problems arise because DSE maintains symbolic values that capture only the dependencies on symbolic inputs. This ignores control dependencies, including loop dependencies that depend indirectly on the inputs. We propose a method to increase the coverage achieved by DSE in the presence of input-data dependent loops and loop dependent branches. We combine DSE with abstract interpretation to find indirect control dependencies, including loop and branch indirect dependencies. Preliminary results show that this results in better coverage, within considerably less time compared to standard DSE.

According to Clark's seminal work on common ground and grounding, participants collaborating in a joint activity rely on their shared information, known as common ground, to perform that activity successfully, and continually align and augment this information during their collaboration. Similarly, teams of human and artificial agents require common ground to successfully participate in joint activities. Indeed, without appropriate information being shared, using agent autonomy to reduce the workload on humans may actually increase workload as the humans seek to understand why the agents are behaving as they are. While many researchers have identified the importance of common ground in artificial intelligence, there is no precise definition of common ground on which to build the foundational aspects of multi-agent collaboration. In this paper, building on previously-defined modal logics of belief, we present logic definitions for four different types of common ground. We define modal logics for three existing notions of common ground and introduce a new notion of common ground, called salient common ground. Salient common ground captures the common ground of a group participating in an activity and is based on the common ground that arises from that activity as well as on the common ground they shared prior to the activity. We show that the four definitions share some properties, and our analysis suggests possible refinements of the existing informal and semi-formal definitions.

Proper epistemic knowledge bases (PEKBs) are syntactic knowledge bases that use multi-agent epistemic logic to represent nested multi-agent knowledge and belief. PEKBs have certain syntactic restrictions that lead to desirable computational properties; primarily, a PEKB is a conjunction of modal literals, and therefore contains no disjunction. Sound entailment can be checked in polynomial time, and is complete for a large set of arbitrary formulae in logics Kn and KDn. In this paper, we extend PEKBs to deal with a restricted form of disjunction: 'knowing whether.' An agent i knows whether Q iff agent i knows Q or knows not Q; that is, []Q or []not(Q). In our experience, the ability to represent that an agent knows whether something holds is useful in many multi-agent domains. We represent knowing whether with a modal operator, and present sound polynomial-time entailment algorithms on PEKBs with the knowing whether operator in Kn and KDn, but which are complete for a smaller class of queries than standard PEKBs.

Symbolic execution can automatically explore different execution paths in a system under test and generate tests to precisely cover them. It has two main advantages-being automatic and thorough within a theory-and has many successful applications. The bottleneck of symbolic execution currently is the computation consumption for complex systems. Compositional Symbolic Execution (CSE) introduces a summarisation module to eliminate the redundancy in the exploration of repeatedly encountered code. In our previous work, we generalised the summarisation for any code fragments instead of functions. In this paper, we transplant this idea onto LLVM with many additional features, one of them being the use of incremental solving. We show that the combination of CSE and incremental solving is mutually beneficial. The obvious weakness of CSE is the lack of context during summarisation. We discuss the use of assumption-based features, available in modern constraint solvers, as a way to overcome this problem.

Deriving requirements that satisfy the needs and desires of users is crucial in software engineering. However, to be able to specify these requirements, potential users must be identified and perhaps prioritised first. In organisational and commercial settings, users often have well-defined roles and responsibilities tied to specific work-flows, which are exploited in requirements engineering methodologies. However, in more social settings, such as platforms for enhancing social interaction, there are a range of non-specific users with ill-defined roles. This paper proposes a novel approach to segment potential and target users based on system goals, adopting customer segmentation concepts adopted from the field of marketing. We evaluate the appropriateness of the proposed approach on two different case studies. Results indicate the proposed method is a suitable approach for finding potential and target users and that user segmentation gives system analysts a better insight for requirements elicitation.

Many AI applications involve the interaction of multiple autonomous agents, requiring those agents to reason about their own beliefs, as well as those of other agents. However, planning involving nested beliefs is known to be computationally challenging. In this work, we address the task of synthesizing plans that necessitate reasoning about the beliefs of other agents. We plan from the perspective of a single agent with the potential for goals and actions that involve nested beliefs, non-homogeneous agents, co-present observations, and the ability for one agent to reason as if it were another. We formally characterize our notion of planning with nested belief, and subsequently demonstrate how to automatically convert such problems into problems that appeal to classical planning technology. Our approach represents an important first step towards applying the well-established field of automated planning to the challenging task of planning involving nested beliefs of multiple agents.

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.

Reactive path planning to avoid collisions with moving obstacles enables more robust agent systems. However, many solutions assume that moving objects are passive; that is, they do not consider that the moving objects are themselves re-planning to avoid collisions, and thus may change their trajectory. In this paper we present a model, Anticipatory Stigmergic Collision Avoidance (ASCA) for reciprocal collision avoidance using anticipatory stigmergy. Unlike standard stigmergy, in which agents leave pheromones to indicate a trace of previous actions, anticipatory stigmergy deposits pheromones on intended future paths. By sharing their intended future paths with each other at regular intervals, agents can re-plan to attempt to avoid collisions. We experimentally evaluate ASCA over three scenarios, and compare with a state of art approach, Reciprocal Velocity Obstacles (RVO). Our evaluation showed that ASCA is consistently more robust in noisy environments in which transmitted information can be lost or degraded. Further, using ASCA without noise results in fewer collisions than RVO when agents are in formation, but more collisions when formed randomly.

In this paper, we describe research results arising from a technology transfer exercise on agent-oriented requirements engineering with an industry partner. We introduce two improvements to the state-of-the-art in agent-oriented requirements engineering, designed to mitigate two problems experienced by ourselves and our industry partner: (1) the lack of systematic methods for agent-oriented requirements elicitation and modelling; and (2) the lack of prescribed deliverables in agent-oriented requirements engineering. We discuss the application of our new approach to an aircraft turnaround simulator built in conjunction with our industry partner, and show how agent-oriented models can be derived and used to construct a complete requirements package. We evaluate this by having three independent people design and implement prototypes of the aircraft turnaround simulator, and comparing the three prototypes. Our evaluation indicates that our approach is effective at delivering correct, complete, and consistent requirements that satisfy the stakeholders, and can be used in a repeatable manner to produce designs and implementations. We discuss lessons learnt from applying this approach.

Test case prioritization is the process of ordering the execution of test cases to achieve a certain goal, such as increasing the rate of fault detection. Increasing the rate of fault detection can provide earlier feedback to system developers, improving fault fixing activity and, ultimately, software delivery. Many existing test case prioritization techniques consider that tests can be run in any order. However, due to functional dependencies that may exist between some test cases-that is, one test case must be executed before another-this is often not the case. In this paper, we present a family of test case prioritization techniques that use the dependency information from a test suite to prioritize that test suite. The nature of the techniques preserves the dependencies in the test ordering. The hypothesis of this work is that dependencies between tests are representative of interactions in the system under test, and executing complex interactions earlier is likely to increase the fault detection rate, compared to arbitrary test orderings. Empirical evaluations on six systems built toward industry use demonstrate that these techniques increase the rate of fault detection compared to the rates achieved by the untreated order, random orders, and test suites ordered using existing "coarse-grained” techniques based on function coverage.

Software testing remains the most widely used approach to verification in industry today, consuming between 30-50 percent of the entire development cost. Test input selection for intelligent agents presents a problem due to the very fact that the agents are intended to operate robustly under conditions which developers did not consider and would therefore be unlikely to test. Using methods to automatically generate and execute tests is one way to provide coverage of many conditions without significantly increasing cost. However, one problem using automatic generation and execution of tests is the oracle problem: How can we automatically decide if observed program behavior is correct with respect to its specification? In this paper, we present a model-based oracle generation method for unit testing belief-desire-intention agents. We develop a fault model based on the features of the core units to capture the types of faults that may be encountered and define how to automatically generate a partial, passive oracle from the agent design models. We evaluate both the fault model and the oracle generation by testing 14 agent systems. Over 400 issues were raised, and these were analyzed to ascertain whether they represented genuine faults or were false positives. We found that over 70 percent of issues raised were indicative of problems in either the design or the code. Of the 19 checks performed by our oracle, faults were found by all but 5 of these checks. We also found that 8 out the 11 fault types identified in our fault model exhibited at least one fault. The evaluation indicates that the fault model is a productive conceptualization of the problems to be expected in agent unit testing and that the oracle is able to find a substantial number of such faults with relatively small overhead in terms of false positives.

SUMMARY Despite the existence of a number of animation tools for a variety of languages, methods for employing these tools for specification testing have not been adequately explored. Similarly, despite the close correspondence between specification testing and implementation testing, the two processes are often treated independently, and relatively little investigation has been performed to explore their relationship. This paper presents the results of applying a framework and method for the systematic testing of specifications and their implementations. This framework exploits the close correspondence between specification testing and implementation testing. The framework is evaluated on a sizable case study of the Global System for Mobile Communications 11.11 Standard, which has been developed towards use in a commercial application. The evaluation demonstrates that the framework is of similar cost‐effectiveness to the BZ‐Testing‐Tools framework and more cost‐effective than manual testing. A mutation analysis detected more than 95% of non‐equivalent specification and implementation mutants. Copyright © 2010 John Wiley & Sons, Ltd.

For agents to fulfill their potential of being intelligent and adaptive, it is useful to model their interaction protocols as executable entities that can be referenced, inspected, composed, shared, and invoked between agents, all at runtime. We use the term first‐class protocol to refer to such protocols. Rather than having hard‐coded decision‐making mechanisms for choosing their next move, agents can inspect the protocol specification at runtime to do so, increasing their flexibility. In this article, we show that propositional dynamic logic (PDL) can be used to represent and reason about the outcomes of first‐class protocols. We define a proof system for PDL that permits reasoning about recursively defined protocols. The proof system is divided into two parts: one for reasoning about terminating protocols, and one for reasoning about nonterminating protocols. We prove that proofs about terminating protocols can be automated, while proofs about nonterminating protocols are unable to be automated in some cases. We prove that, for a restricted class of nonterminating protocols, proofs about them can be transformed to proofs about terminating protocols, making them automatable.

Achieving consistency between a specification and its implementation is an important part of software development In previous work, we have presented a method and tool support for testing a formal specification using animation and then verifying an implementation of that specification. The method is based on a testgraph, which provides a partial model of the application under test. The testgraph is used in combination with an animator to generate test sequences for testing the formal specification. The same testgraph is used during testing to execute those same sequences on the implementation and to ensure that the implementation conforms to the specification. So far, the method and its tool support have been applied to software components that can be accessed through an application programmer interface (API). In this paper, we use an industrially-based case study to discuss the problems associated with applying the method to a software system with a graphical user interface (GUI). In particular, the lack of a standardised interface, as well as controllability and observability problems, make it difficult to automate the testing of the implementation. The method can still be applied, but the amount of testing that can be carried on the implementation is limited by the manual effort involved.

Achieving consistency between a specification and its implementation is an important part of software development. In this paper, we present a method for generating passive test oracles that act as self-checking implementations. The implementation is verified using an animation tool to check that the behavior of the implementation matches the behavior of the specification. We discuss how to integrate this method into a framework developed for systematically animating specifications, which means a tester can significantly reduce testing time and effort by reusing work products from the animation. One such work product is a testgraph: a directed graph that partially models the states and transitions of the specification. Testgraphs are used to generate sequences for animation, and during testing, to execute these same sequences on the implementation.

Formal specifications can precisely and unambiguously define the required behavior of a software system or component. However, formal specifications are complex artifacts that need to be verified to ensure that they are consistent, complete, and validated against the requirements. Specification testing or animation tools exist to assist with this by allowing the specifier to interpret or execute the specification. However, currently little is known about how to do this effectively.This article presents a framework and tool support for the systematic testing of formal, model-based specifications. Several important generic properties that should be satisfied by model-based specifications are first identified. Following the idea of mutation analysis, we then use variants or mutants of the specification to check that these properties are satisfied. The framework also allows the specifier to test application-specific properties. All properties are tested for a range of states that are defined by the tester in the form of a testgraph, which is a directed graph that partially models the states and transitions of the specification being tested. Tool support is provided for the generation of the mutants, for automatically traversing the testgraph and executing the test cases, and for reporting any errors. The framework is demonstrated on a small specification and its application to three larger specifications is discussed. Experience indicates that the framework can be used effectively to test small to medium-sized specifications and that it can reveal a significant number of problems in these specifications.