Observable and Attention-Directing BDI Agents for Human-Autonomy Teaming

Blair Archibald Muffy Calder Michele Sevegnani Mengwei Xu School of Computing Science, University of Glasgow, Glasgow, UK {blair.archibald, muffy.calder, michele.sevegnani, mengwei.xu}@glasgow.ac.uk

Abstract

Human-autonomy teaming (HAT) scenarios feature humans and autonomous agents collaborating to meet a shared goal. For effective collaboration, the agents must be transparent and able to share important information about their operation with human teammates. We address the challenge of transparency for Belief-Desire-Intention agents defined in the Conceptual Agent Notation (Can) language. We extend the semantics to model agents that are observable (i.e. the internal state of tasks is available), and attention-directing (i.e. specific states can be flagged to users), and provide an executable semantics via an encoding in Milner’s bigraphs. Using an example of unmanned aerial vehicles, the BigraphER tool, and PRISM, we show and verify how the extensions work in practice.

1 Introduction

Autonomous agents e.g. robots [28] are becoming increasingly. As the autonomy increases, so does the tasks that can be performed [29], and more emphasis is being placed on how agents can form teams, alongside humans, to achieve a common goal, a.k.a. human-autonomy teaming (HAT) [33, 20].

Transparency is especially important in HAT. While there is no single definition [39, 34], we draw on IEEE P7001 standard definition [16] that transparency is measurable, testable, and is “the transfer of information from an autonomous system or its designers to a stakeholder, which is honest, contains information relevant to the causes of some action, decision or behaviour and is presented at a level of abstraction and in a form meaningful to the stakeholder.” Here, we focus on two transparency requirements: observability of internal states and attention-directing of a human teammate.

To illustrate transparency, consider a HAT scenario where a human and an Unmanned Aerial Vehicle (UAV) survey a site together. The UAV performs site surveys through imaging and retrieves objects if needed, while the human assembles and interprets geographically related information (obtained from the UAV). To coordinate an effective exploration, it is essential to have the appropriate transparency into what tasks either is performing and the progress of the relevant tasks. For example, the human needs to know if the UAV has finished surveying an area, or how much is left, before assembling analysis for the same area. Transparency must also be supported to allow attention-direction during autonomy failure (e.g. the engine is malfunctioning) and to highlight changes in the environment, e.g. when a specific land condition is detected by the UAV the human should be notified immediately for inspection.

We tackle the challenge of transparency by modelling and verifying agents that are observable [6], i.e. the status of tasks is known, and attention-directing, i.e. specific states can be flagged to users. Both observability and attention-directing are recommended features in a practical HAT system engineering guide [18], though strictly this guide refers to the former as transparency and the latter as augmenting cognition, which we consider part of transparency.

To demonstrate these features, we extend a model of Belief-Desire-Intention (BDI) agents proposed in [3] that presents an executable semantics of the Can agent language [41] based on Milner’s Bigraphs [19]. BDI agents [7, 23] consist of, (B)eliefs: what the agent knows; (D)esires: what the agent wants to bring about; and (I)ntentions: the desires the agent is currently acting upon. BDI agents are chosen as they are represented in a declarative fashion (easy to log) with some self-explanatory concepts e.g. the beliefs of the agent. Can is chosen as it features a high-level agent programming language that captures the essence of BDI concepts without describing implementation details such as data structures. As a superset of AgentSpeak [22], Can includes advanced BDI agent behaviours such as reasoning with declarative goals, concurrency, and failure recovery, which are necessary for our UAV example modelled in Section 3. Importantly, although we focus on the Can, the language features are similar to those of other mainstream BDI languages and the same modelling techniques would apply to other BDI programming languages. Besides the work of [8] that focuses on transparent ethical reasoning (i.e. why a decision has been made by an agent), we believe this is the first formal analysis of transparency applied to mainstream BDI agents.

We make the following research contributions: (1) an extension of Can language semantics to support transparency, (2) an extension of the bigraph based executable semantics framework, (3) an evaluation based on Unmanned Aerial Vehicles (UAVs) to illustrate the framework.

2 Framework

In this section, we provide transparency mechanisms for observability, i.e. documenting the status of tasks and their progress toward completion, and attention-directing, i.e. flagging information about specific states—of the situation or agent itself—to a user. We start with some Can language background.

2.1 Can Background

The Can language formalises a classical BDI agent consisting of a belief base $\mathcal{B}$ and a plan library $\Pi$ . The belief base $\mathcal{B}$ is a set of formulas encoding the current beliefs and has belief operators for entailment (i.e. $\mathcal{B}\models\varphi)$ , and belief atom addition (resp. deletion) $\mathcal{B}\cup\{b\}$ (resp. $\mathcal{B}\setminus\{b\}$ ) and any logic over the belief base $\mathcal{B}$ is allowed providing entailment is supported. A plan library $\Pi$ is a collection of plans of the form $e:\varphi\leftarrow\mathit{P}$ with $e$ the triggering event, $\varphi$ the context condition, and $\mathit{P}$ the plan-body. Events can be either be external (i.e. from the environment in which the agent is operating) or internal (i.e. sub-events that the agent itself tries to accomplish). In the plan-body, we use $\mathit{P}_{\_}{1};\mathit{P}_{\_}{2}$ for sequence and $\mathit{goal}(\varphi_{\_}{s},\mathit{P},\varphi_{\_}{f})$ for the declarative goal failing if $\varphi_{\_}{f}$ holds and exiting successfully if $\varphi_{\_}{s}$ holds (see [26]).

A basic configuration $\langle\mathcal{B},P\rangle$ , where $P$ is the plan-body being executed (i.e. the current intention), is used in rules that define the execution of a single intention. The agent configuration is defined as $\langle E^{e},\mathcal{B},\Gamma\rangle$ where $E^{e}$ denotes the a set of pending external events and $\Gamma$ the current set of intentions (i.e. partially executed plan-body programs). The agent-level evolution is specified by the transitions over the agent configuration. For example, the agent-level transition to progressing intention which is progessable ( $\langle\mathcal{B},P\rangle\rightarrow\langle\mathcal{B}^{\prime},P^{\prime}\rangle$ ) or dropping any unprogressable intention ( $\langle\mathcal{B},P\rangle\nrightarrow$ ) can be given as follows:

$\dfrac{P\in\Gamma\ \ \ \langle\mathcal{B},P\rangle\rightarrow\langle\mathcal{B}^{\prime},P^{\prime}\rangle}{\langle E^{e},\mathcal{B},\Gamma\rangle\Rightarrow\langle E^{e},\mathcal{B}^{\prime},(\Gamma\setminus\{P\})\cup\{P^{\prime}\}\rangle}\ A_{\_}{step}$ $\dfrac{P\in\Gamma\ \ \ \langle\mathcal{B},P\rangle\nrightarrow}{\langle E^{e},\mathcal{B},\Gamma\rangle\Rightarrow\langle E^{e},\mathcal{B},\Gamma\setminus\{P\}\rangle}A_{\_}{update}$

We refer the reader to [41, 26] for a full overview of the semantics of Can.

2.2 Observability

Observability captures what an agent is doing so that human teammates can coordinate their tasks for effective collaboration. As intention represents tasks, we focus on the status and progress of intentions.

2.2.1 Intention Status

$\dfrac{e\in E^{e}}{\langle E^{e},\mathcal{B},\Gamma\rangle\Rightarrow\langle E^{e}\setminus\{e\},\mathcal{B},\Gamma\cup\{e\}\rangle}A_{\_}{event}$

$\dfrac{\langle e,I,\texttt{pending}\rangle\in E^{e}}{\langle E^{e},\mathcal{B},\Gamma\rangle\Rightarrow\langle E^{e}\setminus\{\langle e,I,\texttt{pending}\rangle\}\cup\{\langle e,I,\texttt{active}\rangle\},\mathcal{B},\Gamma\cup\{\langle e,I\rangle\}\rangle}A^{new}_{\_}{event}$

$\dfrac{\langle P,I\rangle\in\Gamma\ \ \ \langle\mathcal{B},\langle P,I\rangle\rangle\rightarrow\langle\mathcal{B}^{\prime},\langle P^{\prime},I\rangle\rangle}{\langle E^{e},\mathcal{B},\Gamma\rangle\Rightarrow\langle E^{e},\mathcal{B}^{\prime},(\Gamma\setminus\{\langle P,I\rangle\})\cup\{\langle P^{\prime},I\rangle\}\rangle}A^{new}_{\_}{step}$

$\dfrac{P\in\Gamma\ \ \ \langle\mathcal{B},P\rangle\nrightarrow}{\langle E^{e},\mathcal{B},\Gamma\rangle\Rightarrow\langle E^{e},\mathcal{B},\Gamma\setminus\{P\}\rangle}A_{\_}{update}$

$\dfrac{\langle P,I\rangle\in\Gamma\ \ \ \langle e,I,\texttt{active}\rangle\in E^{e}\ \ \ \langle\mathcal{B},\langle P,I\rangle\rangle\nrightarrow\ \ \ P=nil}{\langle E^{e},\mathcal{B},\Gamma\rangle\Rightarrow\langle E^{e}\setminus\{\langle e,I,\texttt{active}\rangle\}\cup\{\langle e,I,\texttt{success}\rangle\},\mathcal{B},\Gamma\setminus\{\langle P,I\rangle\}\rangle}A^{new}_{\_}{update\_suc}$

$\dfrac{\langle P,I\rangle\in\Gamma\ \ \ \langle e,I,\texttt{active}\rangle\in E^{e}\ \ \ \langle\mathcal{B},\langle P,I\rangle\rangle\nrightarrow\ \ \ P\neq nil}{\langle E^{e},\mathcal{B},\Gamma\rangle\Rightarrow\langle E^{e}\setminus\{\langle e,I,\texttt{active}\rangle\}\cup\{\langle e,I,\texttt{failure}\rangle\},\mathcal{B},\Gamma\setminus\{\langle P,I\rangle\}\rangle}A^{new}_{\_}{update\_fail}$

Figure 1: Derivation rules for agent configuration.

As a high-level planning language, Can is agnostic to many practical issues – including transparency. One issue of Can is the inability to tell the status of an intention. For example, the rule $A_{\_}{update}$ in Fig. 1 discards an intention that cannot do any more intention-level transitions: both if it has already succeeded, or if it failed, and there is no way to determine which was the case. In practice, we may find it helpful, particularly in HAT, to have precise knowledge on the success or failure status of an intention.

We extend Can semantics to allow intention status. Following work [14], we introduce four status values for an external event (that ultimately gives rise to an intention): pending, active, success, and failure along with an unique identifier $I$ . These values indicate when an event is not addressed yet (pending), currently being addressed (active), successfully addressed (success), and addressed with a failure (failure). Unique identifiers enable the agent to track the means-end relations between the events and the related intentions, and differentiate intentions from others.

Figure 1 presents the original rules and our status-enabled rules where $\langle E^{e},\mathcal{B},\Gamma\rangle$ consists of a set of external events $E^{e}$ that the agent is required to respond, a belief set $\mathcal{B}$ , and intention base $\Gamma$ is a set of partially executed plan-bodies $P$ that the agent has committed to. While the original rule $A_{\_}{event}$ deletes events once they have turned into intentions, the new rule $A^{new}_{\_}{event}$ instead switches the status of the event to active. When intentions progress, the status of related external events remains active, until the intention is removed either with sucess (if we reached a $nil$ ) via $A^{new}_{\_}{update\_suc}$ or failure via $A^{new}_{\_}{update\_fail}$ .

2.2.2 Intention Progress

Besides the intention status, it is also useful to estimate the progress of intentions. For example, the human teammate may want to know how long the UAV needs to finish surveying to plan their next tasks.

In BDI agents, goal-plan trees (shown in Fig. 2) are a canonical representation of intentions [35]. The root of the tree is an external event, and its children are plans that can handle this event. Plans may contain sub-events, giving rise to a tree structure that represents all possible ways of achieving a task. Traditionally, for simplicity, goal-plan trees often do not represent actions and contain only goals/subgoals and plans e.g. in [35]. However, we need to include the actions—a crucial part in agent execution—to perform faithful intention progress estimation. Finally, executing a BDI program gives one execution trace¹¹1For practicality, we do not allow recursive plans as this can lead to infinite traces. [42], i.e. a path through the tree.

To illustrate goal-plan trees and execution traces, consider the following two plans as follows:

$P_{\_}{1}=e_{\_}{1}:\varphi_{\_}{1}\leftarrow a_{\_}{1};a_{\_}{2};$ $P_{\_}{2}=e_{\_}{1}:\varphi_{\_}{2}\leftarrow a_{\_}{3};a_{\_}{4};a_{\_}{5}.$

These two plans are visualised as the goal-plan tree $T$ given in Fig. 2. The goal-plan tree $T$ expresses that, given an event $e_{\_}1$ , it has two plan choices, namely plan $P_{\_}1$ and $P_{\_}2$ , where the edges between the event $e_{\_}1$ and plan $P_{\_}1$ and $P_{\_}2$ are labelled with the relevant context condition $\varphi_{\_}{1}$ and $\varphi_{\_}{2}$ . If plan $P_{\_}1$ is selected (given $\varphi_{\_}{1}$ holds), it has two sequenced actions $a_{\_}1$ and $a_{\_}2$ to execute where the edge between the plan to its plan-body is labelled with the position number. As such, we can obtain one execution trace $e_{\_}{1};P_{\_}{1};a_{\_}{1};a_{\_}{2}$ and the other one (due to the selection of plan $P_{\_}2$ ) $e_{\_}{1};P_{\_}{2};a_{\_}{3};a_{\_}{4};a_{\_}{5}$ .

Figure 2: A goal-plan tree.

For intention progress estimation, we use a compile-time process to obtain all possible execution traces. For each trace, we record the maximum length of the execution trace. During execution, the agent tracks its current execution trace so that after an agent-step we can determine the maximum length of the full trace this current trace belongs to²²2To ensure each trace is uniquely identifiable, the same action occurring in a different plan is treated as a different action.. The progress of an intention is then estimated as the ratio of the position of the last element in the current trace and the length of the full trace this current trace belongs to. For example, given a trace $e_{\_}{1};P_{\_}{1};a_{\_}{1};a_{\_}{2}$ , its maximum length is 4 and the position for each element in this trace is 1 for $e_{\_}1$ , 2 for $P_{\_}{1}$ , 3 for $a_{\_}{1}$ , and 4 for $a_{\_}{2}$ . If the current execution trace is $e_{\_}{1};P_{\_}{1};a_{\_}{1}$ then the progress estimation is $3/4=75\%$ (as $a_{\_}1$ is the last element). In the case of failure recovery, for example, if action $a_{\_}{1}$ failed, the agent backtracked to event $e_{\_}1$ and subsequently selected the plan $P_{\_}2$ . Then the current trace becomes $e_{\_}{1};P_{\_}{2}$ (against the full trace $e_{\_}{1};P_{\_}{2};a_{\_}{3};a_{\_}{4};a_{\_}{5}$ ) with the progress estimation $2/5=40\%$ . The execution trace is maintained separately for each intention.

2.3 Directing Attention

Agents should be able to direct the attention of teammates when particular states become relevant, e.g. when adversarial situations are encountered. In BDI programming languages such as AgentSpeak, a change in the belief base generates an event, which subsequently requires an agent to select a plan. For example, if a belief atom $b$ is true, an event in the form of $+b$ is added to the desires. While useful, this one-to-one mapping between belief and event is also limiting, especially in the context of directing attention e.g. it prohibits the generation of multiple events. Further, multiple events generated by a single belief change may require adjustment throughout the operational life of the agent.

We take an approach to directing attention that employs the motivation library of [27]. This allows new (and multiple) intentions (e.g. to communicate with a human) to be created dynamically when a particular state is recognised (i.e. the correct beliefs hold). To be precise, a motivation library (specified by the agent designers) $\mathcal{M}$ is a set of rules of the form: $\psi\rightsquigarrow\langle e,I\rangle$ where $\psi$ is a world state, $e$ an event, and $I$ an identifier. The semantics of motivation execution is specified as follows:

$\dfrac{\psi\rightsquigarrow\langle e,I\rangle\in\mathcal{M}\ \ \mathcal{B}\models\psi\ \ \langle e,I\rangle\notin\Gamma\ \ }{\langle E^{e},\mathcal{B},\Gamma\rangle\rightarrow\langle E^{e}\cup\langle e,I,\texttt{active}\rangle,\mathcal{B},\Gamma\cup\{\langle e,I\rangle\}\rangle}$ $A_{\_}{motive}$

Informally, if the agent believes $\psi$ , it should adopt the event $\langle e,I\rangle$ (if it has not adopted it before). As such, the programmers can specify (and revise) multiple rules $\psi\rightsquigarrow\langle e_{\_}1,I_{\_}1\rangle$ , $\ldots$ , $\psi\rightsquigarrow\langle e_{\_}n,I_{\_}n\rangle$ to ensure a correct set of events to be generated at any time when $\psi$ holds. From our experience, this approach also benefits from the modularity principle by separating the dynamics of desires and design of plan library.

3 UAV Example

	1 // Initial beliefs
	2 $\neg$ sensor_malfunc, $\neg$ engine_malfunc
	3 // External events
	4 $\langle$ e_retrv, identifier1 $\rangle$
	5 // Motivation library events
	6 parked <- $\langle$ e_parked, identifier2 $\rangle$
	7 // Plan library
	8 e_retrv : $\varphi$ <- take_off; goal(at_destination, e_path1, fc); retrieve
	9 e_retrv : $\varphi$ <- take_off; goal(at_destination, e_path2, fc); retrieve
	10 e_retrv : $\varphi$ <- take_off; goal(at_destination, e_path3, fc); retrieve
	11 e_retrv : sensor_malfunc <- return_base
	12 e_retrv : engine_malfunc <- activate_parking
	13 e_path1 : true <- navigate_path_1
	14 e_path2 : true <- navigate_path_2
	15 e_path3 : true <- navigate_path_3
	16 e_parked : true <- send_GPS
	$\displaystyle\text{where}\ \varphi=\neg\texttt{sensor\_malfunc}\wedge\neg\texttt{engine\_malfunc},$
	$\displaystyle\texttt{fc}=\texttt{sensor\_malfunc}\vee\texttt{engine\_malfunc}$

Figure 3: UAV BDI agent design.

To demonstrate our new transparency mechanisms, we give a simple Unmanned Aerial Vehicles (UAVs) example, where UAVs are used for object retrieval tasks, e.g. package delivery, and might be subject to engine or sensor malfunction. The agent design is in Fig. 3 where we heavily rely on declarative goal and failure recovery features in Can. There is one main retrieve task, initiated by external event e_retrv (line 4), which can be handled by five relevant plans (lines 8–12). The first 3 plans provide different flight paths after take-off in which they all have a declarative goal. For example, the declarative goal goal(at_destination, e_path1, fc) says that it is achieved if it believes at_destination holds and failed if fc holds. When fc holds, the other two plans (lines 11 and 12) perform safe recovery in the event of engine or sensor malfunction. In the case of engine malfunction, instead of returning to base (when sensor is faulty), the plan in line 12 instructs the UAV to land and park itself. Once the UAV is landed and parked, the human teammate should be notified of the situation and respond accordingly. Therefore, for directing attention, the motivation library is given in line 6, so that if the belief that the UAV parked itself (i.e. parked) holds after the action activateparking, the agent should adopt the event e_parked to send GPS coordinates (line 16) to a human teammate to retrieve the UAV. For succinct presentation, we do not show the encoding of actions such as take_off and retrieve (which can found in the online model³³3https://bitbucket.org/uog-bigraph/observableattention-directingbdimodel/src/master/).

3.1 Analysis

We encoded the Can semantics in bigraphs [19, 3], which has been used previously to encode the semantics of process calculi [9, 31]. Our bigraph encoding permits execution and symbolic analysis and we employ BigraphER [30]—an open-source language and toolkit for bigraphs—to generate (and export) a transition system for analysis with model checking tools e.g. PRISM [17]. The example above is available in BigraphER format in the online model. For reasoning, states are labelled with bigraph patterns [5], predicates that indicate if there is match of a bigraph in that state. Temporal properties are expressed using linear or branching time temporal logics e.g. Computation Tree logic (CTL) [11].

For observability, we want to check 1) if an intention is being progressed, its status should never be pending, 2) if an intention becomes a completed empty program, its related event will eventually succeed, and 3) if an intention becomes blocked, but is not an empty program, its related original event will eventually fail. For progress, we label each step in the execution trace with its true progress estimation and check that there always exists a path where these match. For attention-directing, we check that if the belief atom parked is believed, then eventually the event e_parked will be added to the agent desires.

As an example, consider observability and properties 2) and 3) for the event, namely $\langle$ e_retrv, identifier1 $\rangle$ given in Fig. 3, which we can express in CTL as follows:

$\mathbf{A}[\varphi_{\_}{1}\implies\mathbf{F}(\varphi_{\_}{2}\wedge\neg\varphi_{\_}{4})]\qquad\qquad$ for property 2)

$\mathbf{A}[\varphi_{\_}{3}\implies\mathbf{F}(\varphi_{\_}{4}\wedge\neg\varphi_{\_}{2})]\qquad\qquad$ for property 3)

The specification for property 2) checks that along all paths, if an intention is completed (i.e. $\varphi_{\_}{1}$ holds), this implies that eventually the original event will succeed (and not fail), i.e. $\mathbf{F}(\varphi_{\_}{2}\wedge\neg\varphi_{\_}{4})$ . Similar logic applies when an intention is blocked for property 3). We do not give full details, but for the interested reader, the state formulae can be represented by the following bigraph patterns:

$\varphi_{\_}{1}\stackrel{{\scriptstyle\text{def}}}{{=}}\mathsf{Intent_{\_}{e}.(Identifier.Identifier1\mid Nil\mid id)}$

$\varphi_{\_}{2}\stackrel{{\scriptstyle\text{def}}}{{=}}\mathsf{Event_{\_}{e}.(Identifier.Identifier1\mid Success\mid id)}$ ,

$\varphi_{\_}{3}\stackrel{{\scriptstyle\text{def}}}{{=}}\mathsf{Intent_{\_}{e}.(Identifier.Identifier1\mid ReduceF\mid id)}$

$\varphi_{\_}{4}\stackrel{{\scriptstyle\text{def}}}{{=}}\mathsf{Event_{\_}{e}.(Identifier.Identifier1\mid Failure\mid id)}$ ,

where $\mathsf{Identifier1}$ is the identifier of the event $\langle$ e_retrv, identifier1 $\rangle$ , the symbol $\mathsf{id}$ (called a site in bigraphs) stands for the part of model that is abstracted away such as the execution trace, and the subscript $\mathsf{e}$ (called a link) maintains the mean-end relation between an original event and the related intention. The transition system for the agent in Fig. 3 has 44 states and 44 transitions⁴⁴4There are numerous internal states, that do not appear in the final transition system, but add to build time. and all the above mentioned properties are shown to hold.

4 Related Work

We are not the first to label intention status [14, 15] (as pending/active), however like the original Can semantics, these approaches do not make intention success/failure explicit. We believe having this information is much more important to human users than simply knowing an intention is dropped. Intention estimation has also been explored [36, 37], but in the context of scheduling where they wish to choose the most-completed intention first. The approach is based on completeness measures that use the resource consumption and effects of achieving intentions as an estimate, however this requires domain knowledge on the pre-conditions/post-effects of events that can be hard to obtain. For the attention directing feature, we adopted the motivation library approach from [27]. There are similar approaches such as conditional goals in [24, 25] and automatic events [40] (adopting a goal or an event that is conditionalised by beliefs).

Verifying BDI agents through model checking has been well explored, e.g. [13] verifies the decision making part (modelled in BDI agents) of a hybrid autonomous system, and [12] uses model checking to reason about agent programs written in Agent Programming Languages. Bremner et al.verify that BDI-based decision making (e.g. plan selection) in robotic systems adhere to ethical rules (e.g. save human) [8]. For transparency, they propose a recorder that produces human readable logs consisting of information such as belief base and the plans executed. Though we agree on the use of logging as a means of transparency, their aim is to provide logs for future forensic analysis whereas ours is to provide run-time logs for effective HAT.

5 Conclusion and Future Work

We presented an executable framework for verifiable BDI agents supporting observability (showing task status) and attention-directing (flagging relevant information), to facilitate effective human-autonomy teaming (HAT). Observability allows comprehending what an agent is doing and how much progress has been made, while attention directing ensures communication of critical information to human teammates.

Observability is implemented by enabling the agent to show the status of intentions (e.g. pending or active), and to provide a quantitative estimation of progress at each step. Attention-directing is achieved through a motivation library that allows agents to adopt multiple new events when a particular world state is believed to hold. Using a UAV example, we have demonstrated these features in practice.

Full scale observability and attention directing is beyond this initial framework. Future work includes an in-depth survey to determine what are the most important aspects to be made observable (to humans). This might require domain-dependent observability, for example, sometimes why an agent decides to do something is more important than progress estimation. Our current intention progress is a metric that measures the distance to the end of (a possible) execution trace. However, in practice actions do not take the same length of time and further domain knowledge annotation for agent programs may be required for more realistic progress estimation. Transparency encompasses more than observability and attention directing and determining: what to log, how to log, and how to use these logs, e.g. future forensic analysis or run-time decision making, will be crucial to tackle emerging HAT scenarios. Finally, a long-term goal is analysis of the accuracy of the intention progression predictions in different scenarios.

Acknowledgements

This work is supported by the Engineering and Physical Sciences Research Council, under PETRAS SRF grant MAGIC (EP/S035362/1) and S4: Science of Sensor Systems Software (EP/N007565/1).

References

[1]
[2] Victoria Alonso & Paloma de la Puente (2018): System transparency in shared autonomy: A mini review. Frontiers in neurorobotics 12, p. 83, 10.3389/fnbot.2018.00083.
[3] Blair Archibald et al. (2021): Modelling and verifying BDI agents with bigraphs. arXiv preprint arXiv:2105.02578.
[4] Blair Archibald et al. (2021): Probablistic bigraphs. arXiv preprint arXiv:2105.02559.
[5] Steve Benford et al. (2016): On lions, impala, and bigraphs: Modelling interactions in physical/virtual spaces. ACM Transactions on Computer-Human Interaction (TOCHI) 23(2), pp. 1–56, 10.1145/2882784.
[6] Adella Bhaskara et al. (2020): Agent transparency: A review of current theory and evidence. IEEE Transactions on Human-Machine Systems 50(3), pp. 215–224, 10.1109/THMS.2020.2965529.
[7] Michael Bratman (1987): Intention, plans, and practical reason. Harvard University Press, 10.2307/2185304.
[8] Paul Bremner et al. (2019): On proactive, transparent, and verifiable ethical reasoning for robots. Proceedings of the IEEE 107(3), pp. 541–561, 10.1109/JPROC.2019.2898267.
[9] Mikkel Bundgaard & Vladimiro Sassone (2006): Typed polyadic pi-calculus in bigraphs. In: Proceedings of ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 1–12, 10.1145/1140335.1140336.
[10] Filippo Cantucci & Rino Falcone (2020): Towards trustworthiness and transparency in social human-robot interaction. In: Proceedings of 2020 IEEE International Conference on Human-Machine Systems (ICHMS), IEEE, pp. 1–6, 10.1109/ICHMS49158.2020.9209397.
[11] Edmund M Clarke & E Allen Emerson (1981): Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings of Workshop on Logic of Programs, pp. 52–71, 10.1007/BFb0025774.
[12] Louise A Dennis et al. (2012): Model checking agent programming languages. Automated software engineering 19(1), pp. 5–63, 10.1007/s10515-011-0088-x.
[13] Louise A Dennis et al. (2016): Practical verification of decision-making in agent-based autonomous systems. Automated Software Engineering 23(3), pp. 305–359, 10.1007/s10515-014-0168-9.
[14] James Harland et al. (2014): An operational semantics for the goal life-cycle in BDI agents. Autonomous agents and multi-agent systems 28(4), pp. 682–719, 10.1007/s10458-013-9238-9.
[15] James Harland et al. (2017): Aborting, suspending, and resuming goals and plans in BDI agents. Autonomous Agents and Multi-Agent Systems 31(2), pp. 288–331, 10.1007/s10458-015-9322-4.
[16] IEEE (2020): IEEE Draft Standard for Transparency of Autonomous Systems. In: IEEE P7001/D1, Piscataway NJ: IEEE, pp. 1–76.
[17] Marta Kwiatkowska et al. (2011): PRISM 4.0: Verification of Probabilistic Real-time Systems. In: Proceedings of Conference on Computer Aided Verification, pp. 585–591, 10.1007/978-3-642-22110-147.
[18] Patricia McDermott et al. (2018): Human-machine teaming systems engineering guide. Technical Report, MITRE CORP.
[19] Robin Milner (2009): The space and motion of communicating agents. Cambridge University Press, 10.1017/CBO9780511626661.
[20] Thomas O’Neill et al. (2020): Human–autonomy teaming: A review and analysis of the empirical literature. Human Factors, 10.1177/0018720820960865.
[21] Raja Parasuraman & Victor Riley (1997): Humans and automation: Use, misuse, disuse, abuse. Human factors 39(2), pp. 230–253, 10.1518/001872097778543886.
[22] Anand S Rao (1996): AgentSpeak (L): BDI agents speak out in a logical computable language. In: European workshop on modelling autonomous agents in a multi-agent world, Springer, pp. 42–55, 10.1007/BFb0031845.
[23] Anand S Rao et al. (1995): BDI agents: From theory to practice. In: Proceedings of the First International Conference on Multiagent Systems, pp. 312–319.
[24] M. Birna van Riemsdijk et al. (2004): Dynamics of declarative goals in agent programming. In: Proceedings of International Workshop on Declarative Agent Languages and Technologies, Springer, pp. 1–18, 10.1007/114934021.
[25] M. Birna van Riemsdijk et al. (2005): Semantics of declarative goals in agent programming. In: Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, pp. 133–140, 10.1145/1082473.1082494.
[26] Sebastian Sardina & Lin Padgham (2007): Goals in the context of BDI plan failure and planning. In: the 6th International Joint Conference on Autonomous Agents and Multiagent Systems, pp. 16–23, 10.1145/1329125.1329134.
[27] Sebastian Sardina & Lin Padgham (2011): A BDI agent programming language with failure handling, declarative goals, and planning. Autonomous Agents and Multi-Agent Systems 23(1), pp. 18–70, 10.1007/s10458-010-9130-9.
[28] Allison Sauppé & Bilge Mutlu (2015): The social impact of a robot co-worker in industrial settings. In: Proceedings of the 33rd annual ACM conference on human factors in computing systems, pp. 3613–3622, 10.1145/2702123.2702181.
[29] Isabella Seeber et al. (2020): Machines as teammates: A research agenda on AI in team collaboration. Information & management, 10.1016/j.im.2019.103174.
[30] Michele Sevegnani & Muffy Calder (2016): BigraphER: Rewriting and Analysis Engine for Bigraphs. In: 28th International Conference on Computer Aided Verification, pp. 494–501, 10.1007/978-3-319-41540-6_27.
[31] Michele Sevegnani & Eloi Pereira (2014): Towards a bigraphical encoding of actors. In: International Workshop on Meta Models for Process Languages, 10.13140/RG.2.1.3681.9046.
[32] Michele Sevegnani et al. (2018): Modelling and Verification of Large-Scale Sensor Network Infrastructures. In: 23rd International Conference on Engineering of Complex Computer Systems, ICECCS, pp. 71–81, 10.1109/ICECCS2018.2018.00016.
[33] R Jay Shively et al. (2017): Why human-autonomy teaming? In: International conference on applied human factors and ergonomics, Springer, pp. 3–11, 10.1007/978-3-319-60642-21.
[34] Anna Spagnolli et al. (2017): Transparency as an ethical safeguard. In: International Workshop on Symbiotic Interaction, Springer, pp. 1–6, 10.1007/978-3-319-91593-71.
[35] J. Thangarajah & L. Padgham (2011): Computationally effective reasoning about goal interactions. Journal of Automated Reasoning 47(1), pp. 17–56, 10.1007/s10817-010-9175-0.
[36] John Thangarajah et al. (2014): Quantifying the completeness of goals in BDI agent systems. In: ECAI 2014, IOS Press, pp. 879–884, 10.3233/978-1-61499-419-0-879.
[37] John Thangarajah et al. (2015): Estimating the Progress of Maintenance Goals. In: AAMAS, pp. 1645–1646.
[38] Christos Tsigkanos et al. (2020): Scalable Multiple-View Analysis of Reactive Systems via Bidirectional Model Transformations. In: 35th IEEE/ACM International Conference on Automated Software Engineering, pp. 993–1003, 10.1145/3324884.3416579.
[39] Alan FT Winfield et al. (2021): IEEE P7001: A Proposed Standard on Transparency. Frontiers in Robotics and AI, p. 225, 10.3389/frobt.2021.665729.
[40] Michael Winikoff (2005): JACK intelligent agents: an industrial strength platform. In: Multi-Agent Programming, Springer, pp. 175–193, 10.1007/0-387-26350-07.
[41] Michael Winikoff et al. (2002): Declarative and procedural goals in intelligent agent systems. In: 8th International Conference on Principles of Knowledge Representation and Reasoning, pp. 470–481.
[42] Mengwei Xu et al. (2019): Intention interleaving via classical replanning. In: 31st International Conference on Tools with Artificial Intelligence, IEEE, pp. 85–92, 10.1109/ICTAI.2019.00021.