Belief-Desire-Intention (BDI) agents feature uncertain beliefs (e.g. sensor noise), probabilistic action outcomes (e.g. attempting and action and failing), and non-deterministic choices (e.g. what plan to execute next). To be safely applied in real-world scenarios we need reason about such agents, for example, we need probabilities of mission success and the strategies used to maximise this. Most agents do not currently consider uncertain beliefs, instead a belief either holds or does not. We show how to use epistemic states to model uncertain beliefs, and define a Markov Decision Process for the semantics of the Conceptual Agent Notation (Can) agent language allowing support for uncertain beliefs, non-deterministic event, plan, and intention selection, and probabilistic action outcomes. The model is executable using an automated tool—CAN-verify—that supports error checking, agent simulation, and exhaustive exploration via an encoding to Bigraphs that produces transition systems for probabilistic model checkers such as PRISM. These model checkers allow reasoning over quantitative properties and strategy synthesis. Using the example of an autonomous submarine and drone surveillance together with scalability experiments, we demonstrate our approach supports uncertain belief modelling, quantitative model checking, and strategy synthesis in practice.

We present CAN-Verify , an automated tool for analysing BDI agents written in the Conceptual Agent Notation ( Can ) language. CAN-Verify includes support for syntactic error detection before agent execution, agent program interpretation (running agents), and model-checking of agent programs (analysing agents). The model checking supports verifying the correctness of agents against both generic agent requirements, such as if a task is accomplished, and user-defined requirements, such as certain beliefs eventually holding. The latter can be expressed in structured natural language, allowing the tool to be used by agent programmers without formal training in the underlying verification techniques.

Implementations of the Belief-Desire-Intention (BDI) architecture have a long tradition in the development of autonomous agent systems. However, most practical implementations of the BDI framework rely on a pre-defined plan library for decision-making, which places a significant burden on programmers, and still yields systems that may be brittle, struggling to achieve their goals in dynamic environments. This paper overcomes this limitation by introducing an operational semantics for BDI systems that rely on Classical Planning at run time to both cope with failures that were unforeseeable and synthesise new plans that were unspecified at design time. This semantics places particular emphasis on the interaction of the reasoning cycle and an underlying planning algorithm. We empirically demonstrate the practical feasibility and generality of such an approach in an implementation of this semantics within two popular BDI platforms together with in-depth computational evaluation.

Abstract Belief–desire–intention (BDI) agents are a popular agent architecture. We extend conceptual agent notation (Can)—a BDI programming language with advanced features such as failure recovery and declarative goals—to include probabilistic action outcomes, e.g. to reflect failed actuators, and probabilistic policies, e.g. for probabilistic plan and intention selection. The extension is encoded in Milner’s bigraphs. Through application of our BigraphER tool and the PRISM model checker, theprobabilityof success (intention completion) under different probabilistic outcomes and plan/event/intention selection strategies can be investigated and compared. We present a smart manufacturing use case. A significant result is that plan selection has limited effect compared with intention selection. We also see that the impact of action failures can be marginal—even when failure probabilities are large—due to the agent making smarter choices.

Robot swarms, through redundancy, offer fault-tolerant distributed sensing and actuation, but can lack complex mission-level decision making. Pairing a human operator with the swarm can improve decision making but only if the operator maintains situational awareness—knowledge of the current state of the swarm—as well as being able to anticipate future states. We show how formal methods, in the form of probabilistic models, executed and verified at runtime alongside the system can aid situational awareness by providing valuable insight into both current and future situations. Two models, for determining task and mission success probabilities, are given, and we show that statistical model checking allows timely approximate predictions that take no more than 1s while staying within 2% of the exact solution. We highlight and implement approaches to display this information to an operator, and show how models can be used to try what-if scenarios before decisions are made.

The Belief-Desire-Intention (BDI) architecture is a popular framework for rational agents, yet most verification approaches are limited to analysing the behaviours of an agent in a subset of all possible environments.However, in practice, BDI agents operate in dynamic environments where the exact occurrence of external changes is difficult to predict.For safety/security we need to assess whether the agent behaves as required in all circumstances.To address this, we define environments, accounting for both sensor information about physical changes and new tasks to be completed, as a non-deterministic finitestate automata.We give an environment-enabled extension to the Conceptual Agent Notation (CAN) language including an executable semantics via an encoding to Milner's bigraphs and the BigraphER tool.We illustrate the framework through a simple Unmanned Aerial Vehicle (UAV) example that is verified using mainstream tools including PRISM model checker.Results show our approach can automatically identify agent design flaws to aid agent programmers in design, debugging, and analysis.

The BDI architecture, where agents are modelled based on their belief, desires, and intentions, provides a practical approach to developing intelligent agents. One of the key features of BDI agents is that they are able to pursue multiple intentions in parallel, i.e. in an interleaved manner. Most of the previous works have enabled BDI agents to avoid negative interactions between intentions to ensure the correct execution. However, to avoid execution inefficiencies, BDI agents should also capitalise on positive interactions between intentions. In this paper, we provide a theoretical framework where first-principles planning (FPP) is employed to manage the intention interleaving in an automated fashion. Our FPP approach not only guarantees the achievability of intentions, but also discovers and exploits potential common sub-intentions to reduce the overall cost of intention execution. Our results show that our approach is both theoretically sound and practically feasible. The effectiveness evaluation in a manufacturing scenario shows that our approach can significantly reduce the total number of actions by merging common sub-intentions, while still accomplishing all intentions.

The Belief-Desire-Intention (BDI) paradigm is a flexible framework for representing intelligent agents. Practical BDI agent systems rely on a static plan library to reduce the planning problem to the simpler problem of plan selection. However, fixed pre-defined plan libraries are unable to adapt to fast-changing environments pervaded by uncertainty. In this paper, we advance the state-of-the-art in BDI agent systems by proposing a plan library evolution architecture with mechanisms to incorporate new plans (plan expansion) and drop old/unsuitable plans (plan contraction) to adapt to changes in a realistic environment. The proposal follows a principled approach to define plan library expansion and contraction operators, motivated by postulates that clearly highlight the underlying assumptions, and quantified by decision-support measures of temporal information. In particular, we demonstrate the feasibility of the proposed contraction operator by presenting a multi-criteria argumentation based decision making to remove plans exemplified in a planetary vehicle scenario.