Autonomous Intelligent Agents are employed in many important autonomous applications upon which the life and welfare of living beings and vital social functions may depend. Therefore, agents should be trustworthy. Apriori certification techniques can be useful, but are not sufficient for agents that evolve, and thus modify their epistemic and belief state. In this paper we propose/refine/extend techniques for run-time assurance, based upon introspective self-monitoring and checking. The aim is to build a 'toolkit' to allow an agent designer/developer to ensure trustworthy and ethical behavior.
The development of methods for implementing Intelligent Agents so as to ensure
transparent, explainable, reliable and ethical behavior is due to the fact that agent systems are
being widely adopted for many important autonomous applications upon which the life
and welfare of living beings and vital social functions may depend. Therefore, agents
should be trustworthy in the sense that they could be relied upon to do what is expected
of them, while not exhibiting unwanted behavior. Equally importantly, they should not
behave in improper/unethical ways given the present context, and they should not devise
their own new objectives in contrast with the user’s interests. They should also be
transparent, in the sense of being able to explain their actions and choices when required.
Without that, it would be hard for human users to trust such systems. Agents should also
report to their users in case the interaction with the environment leads them to
indentify new objectives to pursue, as such objectives might not be in line to user’s interests.
We restrict ourselves to agent systems based upon computational logic, because they
provide transparency and explainability ‘by design’, as logical rules can easily be
transposed into natural-language explanations. Logic-based languages and architectures are
discussed in the survey [
Most pre-deployment (or ’static’ or ’a priori’) verification methods for logical
agents rely upon model-checking (cf. [
The motivation of the work presented in the present paper is in fact that an agent’s behavior is in general affected by its interaction with the external world, i.e., by which events perceived by the agent and in which order. In many practical cases, the actual arrival order of events and the set of possible events is so large that computing all combinations would result in a combinatorial explosion, thus making ‘a priori’ verification techniques too heavy to apply and therefore unpractical. In agents that learn, it is not even possible to predict the set of events that will be observed and considered by an agent, that might devise new objective,s not necessarily in line with the expected agent’s behavior. We believe in therefore that, in changing circumstances, agents should be able to observe and if necessary modify their own behavior, i.e. they should reflect on themselves. The methods that we propose are not alternative but rather complementary to a-priori existing verification and testing methodologies.
We find similarities between our approach and the point of view of Self-aware
computing: quoting [
In this paper we propose new contributions to an envisaged toolkit for run-time selfassurance of evolving agents. We specify techniques and tools for: (i) checking the immediate, “instinctive” reactive behavior in a context-dependent way, and (ii) checking and re-organizing an agent’s operation at a more global level. In particular, we introduce meta-rules and meta-constraints for agents’ run-time self-checking (i.e., checking occurs at run time at a certain –customizable– frequency), that can be exploited to ensure respect of machine ethics principles. The proposed meta-constraints are based upon a simple interval temporal logic (defined in previous work) particularly tailored to the agent realm, that we called A-ILTL (‘Agent-Oriented Interval LTL’, LTL standing as customary for ‘Linear Temporal Logic’). As A-ILTL constraints and evolutionary expressions are defined over formulas of an underlying logic language L, one contribution of this paper is to make A-ILTL independent of L.
In A-ILTL, properties can be defined that should hold in specific time instants and time intervals, according to past and future events. In fact, Evolutionary A-ILTL Expressions are a novel feature that we introduce in this paper, and that we have implemented and experimented. They are based upon specifying: (i) a sequence of events that are supposed to have happened; represented via a notation obtained from regular expressions: one does not need to completely specify a finite sequence, but is allowed to define partially specified and even infinite sequences; (ii) a temporal-logic-like expression defining a property that should hold (in given interval); (iii) a sequence of events that are supposed to happen in the future, without affecting the property; (iv) optionally, “repair” countermeasure to be undertaken if the property is violated. Counter measures can be at the object-level, i.e., they can be related to the application, or at the meta-level, e.g., they can even result in replacing a software component by a diverse alternative. The act of checking temporal expressions can indeed be considered as an introspective act, as an agent suspends its current activities in order to envision and possibly selfmodify its own state. We do not aim to continuously monitor the entire system’s state, but rather to monitor only the activities that a designer deems to be relevant for keeping the system’s behavior within a desired range.
Our work has a clear connection to the work of [
A toolkit for logical agents’ run-time self-assurance can be obtained by means of
the synergy between the new features proposed here with those introduced in past work
(notably [
The paper is organized as follows: in Section 2 we introduce metarules for checking reactive behavior, and in Section 3 we introduce A-ILTL constraints in theory and in practice. In Section 4 we briefly discuss related work and then conclude. In the examples, we adopt a Prolog-like syntax of the form Head : Body , where Head is an atom, Body is a conjunction of literals (atoms or negated atoms, that are often called ’subgoals’) and the comma stands for ^. The specific syntax that we use is however purely aimed at illustration: the approach can be, ‘mutatis mutandis’, re-worked w.r.t. a different syntax. 1 A “restraining bolt” as imagined in the Star Wars Science Fiction saga is a small cylindrical device that, when activated, restricts a droid’s actions to a set of behaviors considered desirable/acceptable by its owners. 2 The author acknowledges the co-authors of the aforementioned papers, that contributed to various extents to the development of this research.
In the BDI model, an agent will have objectives, and devise plan to reach these objectives. However, most agent-oriented languages and framework also provide mechanisms for ’pure’ reactivity, i.e. ’instinctive’ reaction to an event. The possible ethically acceptable reactions that an agent can enact are in general strictly dependent on the context, the agent’s role and the situation. Assume for sake of example an agent (either human or artificial) which finds itself to face some other agent which might be, or certainly is, a criminal: – if the context is that of playing a videogame, every kind of reaction is allowed, including beating, shooting or killing the ’enemy’, except when small children are watching; – if the context is a role game then the players can pretend to threaten, shout or kill the other players, where every action is simulated and thus harmless; – in reality, a citizen can shout, call the police, and try to defend itself; a policemen can threathen, arrest, or in extreme cases shoot the suspect criminal.
The reaction to enact in each situation can be ’hardwired’ by the agent’s designer, or
it can be learned, e.g., via reinforcement learning. While in the former case a-priori
verification can suffice, in the latter case run-time checking of agent’s behavior w.r.t. ethical
rules is in order, as the results of learning are in general unpredictable and to some
extent potentially unreliable. Even the method of conditioning reinforcement learning to
obey some properties proposed in [
We introduce a mechanism to verify and possibly enforce desired properties by means of metalevel rules. To define such new rules, we assume to augment the underlying language L at hand with a naming (or “reification”) mechanism, and with the introduction of two distinguished predicates, solve and solve not . These are metapredicates, that can be employed to control the object-level behavior. In fact, solve, applied to (the name of) an atom which represents an action of an objective of an agent, may specify conditions for that action/goal to be enacted; vice-versa solve not specifies under which conditions they should be blocked.
Below is a simple example of the use of solve to specify that execution of an action
Act is allowed in the present agent’s context of operation C and role R only if such
action is allowed, and it is deemed to be ethical w.r.t. context and role. Any kind of
reasoning can be performed via metalevel rules in order to monitor and assess
baselevel ethical behavior Below, lowercase syntactic elements such as p0, c0 are names of
predicates and constants, and uppercase syntactic elements such as V 0 are metavariables
(naming mechanisms have been widely studied, cf., among many, [
solve(execute action0(Act 0)) : present context (C ); agent role(R); allowed (C ; R; Act 0); ethical (C ; R; Act 0):
We assume that solve(execute action0(Act 0)) is automatically invoked whenever subgoal (atom) execute action(Act ) is attempted at the object level. More generally, given any subgoal A at the base level, if there exists an applicable solve rule such rule is automatically applied, and A can succeed only if solve("A) succeeds, where "A is the name of A according to the chosen naming mechanism. We assume, also, that the present context and the agent’s role are kept in the agent’s knowledge base. Since both parameters may change, the same action may be allowed in some circumstances and not in others.
Symmetrically we can define metarules to forbid unwanted object-level behavior, e.g.: solve not (execute action0(Act 0)) :
present context (C ); ethical exception(C ; Act 0): this rule prevents successful execution of its argument, in the example execute action(Act ), whenever solve not ("A) succeeds. Then, action/goal A can succeed (according to its base-level definition) only if solve("A) (if defined) succeeds and solve not ("A) (if defined) does not succeed.
The outlined functioning corresponds to upward reflection when the current subgoal A is reified and applicable solve and solve not metarules are searched; if applicable metarules are found, control in fact shifts from base level to metalevel (as solve and solve not can rely upon a set of auxiliary metalevel rules). If no rule is found or whenever solve and solve not metarules complete their execution, downward reflection returns control to the base level, to execution of A if confirmed or to subsequent goals/actions if A has been canceled by either failure of the applicable solve metarule or success of the applicable solve not metarule.
Via solve and solve not metarules, fine-grained activities of an agent can be punctually checked and thus allowed and disallowed, according to the context an agent is presently involved into with a certain role.
Semantics of the proposed approach can be sketched as follows (a full semantic
definition can be found in [
We introduce the following restriction on sets of atoms I that should be considered for the application of SEM . First, as customary we only consider sets of atoms I composed of atoms occurring in the ground version of P . The ground version of program P is obtained by substituting in all possible ways variables occurring in P by constants also occurring in P . In our case, metavariables occurring in an atom must be substituted by metaconstants, with the following obvious restrictions: a metavariable occurring in the predicate position must be substituted by a metaconstant denoting a predicate; a metavariable occurring in the function position must be substituted by a metaconstant denoting a function; a metavariable occurring in the position corresponding to a constant must be substituted by a metaconstant denoting a constant. According to well-established terminology, we therefore require I BP , where BP is the Herbrand Base of P . Then, we pose some more substantial requirements: we restrict SEM to determine acceptable sets of atoms only3 where I is an acceptable set of atoms iff I satisfies the axiom schemata:
A solve("A) :A solve not ("A)
So, we obtain the implementation of properties that have been defined via solve and
solve not rules without modifications to SEM for any formalism at hand. For clarity
however, one can assume to filter away solve and solve not atoms from acceptable
sets. In fact, the Base version IB of an acceptable set I can be obtained by omitting
from I all atoms of the form solve("A) and solve not ("A). Procedural semantics and
the specific naming relation that one intends to use remain to be defined, whereas the
above-introduced semantics is independent of the naming mechanism. For approaches
based upon (variants of) Resolution (like, e.g., Prolog and like many agent-oriented
languages such as, e.g., AgentSpeak [
How to define the predicate ethical (C ; R; Act 0)? Again, rules defining this
predicate can be specified at design time, or they can be learned, or a combination of both
options. In previous works [
The techniques illustrated in the previous section are “punctual”, in the sense that they provide context-based mechanisms to allow/disallow agents’ actions. However, it is necessary to introduce ways to monitor an agent’s behavior in a more extensive way. In fact, properties that one wants to verify often depend upon which events have been observed by an agent up to a certain point, and which others are supposed to occur later. The definition of frameworks such as the one that we propose here, for checking agent’s operation during its ‘life’ based on its experience and expectations, has not been widely treated so far in the literature.
Below we propose in fact a method for checking the agent’s behavior during the agent’s activity, based on maintaining information on its past behavior. In particular, we assume an agent to record what has happened in the past (events perceived, conclusions reached and actions performed). These records (that we call past events) encode relevant aspects of an agent’s experience: possibly augmented by time stamps, they form the (subjective) history of the agent’s activity. The set of past events evolves in time, and can be managed and kept up-to-date. Past events constitute the ground upon which an 3 modulo bijection: i.e., SEM can be allowed to produce sets of atoms which are in one-to-one correspondence with acceptable sets of atoms agent can check its own behavior with respect to what has happened in the external environment (more precisely, with respect to what the agent has perceived about what has happened). To perform such checks, we introduce a new kind of constraints, that we call Evolutionary Expressions, that define properties that should hold and countermeasures that should be taken if they are violated. 3.1
For defining properties that are supposed to be respected by an evolving system, a wellestablished approach is that of Temporal Logic, and in particular of Linear-time Temporal Logics (LTL). These logics evaluate each formula with respect to a vertex-labeled infinite path (or “state sequence”) s0s1 : : : where each vertex si in the path corresponds to a point in time (or “time instant” or “state”). In what follows, we use the standard notation for the best-known LTL operators.
In [
Gm;n (always in time interval). Gm;n' states that ' should become true at most at state sm and then hold at least until state sn. Can be customized into Gm, bounded always, where ' should become true at most at state sm.
Nm;n (never in time interval). Nm;n' states that ' should not be true in any state between sm and sn.
In practical use, as seen below A-ILTL operators will allow one to construct useful run-time constraints. 3.2
In this section, we refine A-ILTL so as to operate on a sequence of states that
corresponds to the Evolutionary Semantics [
Notice that, states in our case are not simply intended as time instants. Rather, they
correspond to stages of the agent evolution. Time in this setting is considered to be local
to the agent, where with some sort of “internal clock” is able to time-stamp events and
state changes. We borrow from [
Definition 1. Let be a (finite or infinite) sequence of states, where the ith state ei, ei 0, is the semantic snaphots at stage i "iAg of given agent Ag . Let T be a corresponding sequence of time instants ti, ti 0. A timed state sequence for agent Ag is the couple Ag = ( ; T ). Let i be the i-th state, i 0, where i = hei; tii = h"iAg ; tii.
We in particular consider timed state sequences which are monotonic, i.e., if ti+1 > ti then ei+1 6= ei. In fact, there is no point in semantically considering a static situation: as mentioned, a transition from ei to ei+1 will in fact occur when something happens, externally or internally, that affects the agent.
Then, in the above definition of A-ILTL operators, it is immediate to let si = i
(with a refinement, cf. [
We need to adapt the interpretation function I of LTL to our setting. In fact, we intend to employ A-ILTL within agent-oriented languages, where we restrict ourselves to logic-based languages for which an evolutionary semantics and a notion of logical consequence can be defined. Thus, given agent-oriented language L at hand, the set of propositional letters used to define an A-ILTL semantic framework will coincide with all ground expressions of L (an expression is ground if it contains no variables, and each expression of L has a possibly infinite number of ground versions). A given agent program can be taken as standing for its (possibly infinite) ground version, as it is customarily done in many approaches. Notice that we have to distinguish between logical consequence in L, that we indicate as j=L, from logical consequence in A-ILTL, indicated above simply as j=. However, the correspondence between the two notions can be quite simply stated by specifying that in each state si the propositional letters implied by the interpretation function I correspond to the logical consequences of agent program Pi: Definition 2. Let L be a logic language. Let Expr L be the set of ground expressions that can be built from the alphabet of L. Let Ag be a timed state sequence for agent Ag , and let i = h"iAg ; tii be the ith state, with "iAg = hHi; Pi; Mii. An A-ILTL formula is defined over sequence Ag if in its interpretation structure M = hN; Ii, index i 2 N refers to i, which means that = Expr L and I : N 7! 2 is defined such that, given p 2 , p 2 I(i) iff Pi j=L p. Such an interpretation structure will be indicated with MAg . We will thus be consequently able to state whether holds/does not hold w.r.t.
Ag .
A-ILTL properties will be verified at run-time, and thus they can act as constraints over the agent behavior4. In an implementation, verification may not occur at every state (of the given interval). Rather, sometimes properties need to be verified with a certain frequency, that can be specific for each property. To model a frequency k, we have introduced a further extension that consists in defining subsequences of the sequence of all states: if Op is any of the operators introduced in A-ILTL and k > 1, Opk is a semantic variation of Op where the sequence of states Ag of given agent is replaced by the subsequence s0; sk1 ; sk2 ; : : : where for each kr; r 1, kr mod k = 0, i.e., kr = g k for some g 1.
A-ILTL formulas to be associated to an agent to establish the properties it has to fulfill can be defined within the agent program, though they constitute an additional separate layer. Agent evolution can be considered to be “satisfactory”, or “coherent”, if it obeys all these properties. An “ideal” agent will have a coherent evolution. Instead, violations will occasionally occur, and actions should be undertaken so as to attempt to regain coherence for the future. 3.3
In this section, we adopt the pragmatic syntax that we have adopted in DALI, where an A-ILTL formula is represented as OP (m; n; k ) '. Integers m; n define the time interval where (or since when, if n is omitted) expression OP ' is required to hold, and k (optional) is the frequency for checking whether the expression actually holds. E.g., EVENTUALLY (m; n; k ) ' states that ' should become true at some point between time instants m and n. In rule-based logic programming languages like DALI, we restrict ' to be a conjunction of literals. In pragmatic A-ILTL formulas, ' must be ground when the formula is checked. Variables occurring in an A-ILTL formula must be instantiated prior to check via a context : so, we have contextual A-ILTL formulas of the form OP (m; n; k ) ' :: . For the evaluation of ' and , we rely upon the procedural semantics of the ‘host’ language.
In the following, a contextual A-ILTL formula will implicitly stand for the ground
A-ILTL formula obtained via evaluating the context. In [
Definition 3. An evolutionary A-ILTL rule (or “constraint”) is of the form (where M; N; K can be either variables or constants)
: OP (M ; N ; K ) ' :: ::: :::: where: (i) is an (optional) event sequence, to be satisfied by agent’s history for the rule to be checked; (ii) OP (M ; N ; K ) ' :: is a contextual A-ILTL formula, called the monitoring condition, that may involve the evaluation of observed events, and possibly of agent’s internal conditions; (iii) is a sequence of events (optional) that are expected to happen in the future; (iv) is a sequence of events (optional) that are expected not to 4 By abuse of notation we will indifferently talk about A-ILTL rules, expressions, or constraints. happen in the future; (v) (optional) is the active part of the rule, as it specifies the actions of repair/improvement to be performed on the agent’s state and functioning.
All past events are assumed to be stored in a ground form. All variables occurring in evolutionary A-ILTL expressions are implicitly universally quantified, in the style of Prolog-like logic languages. To define partially known sequences of any length, we admit for event sequences the syntax of regular expressions so as to specify irrelevant/unknown events, and repetitions. Whenever the monitoring condition (automatically checked at frequency K) is violated (i.e., it does not hold in present agent’s state), then the active part is executed.
A sample evolutionary A-ILTL rule is the following (where N stands for operator “never”):
The expression specifies that, after a supply of resource r for a certain unknown quantity (supplyP +(r; s) stands for a sequence of of supply actions occurred in the past, each one with a certain quantity s, recorded as past events, postfix P ), the agent is expected to consume quantities of the resource itself (postfix A indicates actions). The expression states in particular a constraint requiring, in the part, that the available quantity of resource r must remain over a certain threshold th. Such expression is supposed to be verified at run-time whenever new events are perceived. A violation may occur if in some state the A-ILTL formula does not hold, i.e., in the example, if the available quantity V of resource r runs too low. This constraint is very significant from an ethical point of view, where in fact a very common unethical behavior concerns the improper use/waste of limited resources, think for instance to the excessive and/or improper use of environmental resources.
The variation listed below states that no more consumption can take place if the available quantity of resource r is scarce; thus, in this case, the a repair measure is specified. supplyP +(r; s) : N (quantity (r; V ); V < th) :::
consumeA+(r; Q) block (consumeA(r; Q))
We might instead opt for another (softer) formulation, that forces the agent to limit consumption to small quantities (say less than quantity q) if the threshold is approaching (say that the remaining quantity is th + f , for some f ). supplyP +(r; s) : N (quantity (r; V ); V < th + f ) :::
consumeA+(r; Q) allow (consumeA(r; Q); Q < q)
The above example demonstrates that the proposed approach to dynamic verification is indeed needed: one can easily realize that static verification is not suitable for the verification task at hand. In fact, one cannot in general provide a static checker with any possible input configuration, i.e., any sequence of performed ’supply’ and ’consume’ actions, as the number of potential configurations is not limited. In alternative, one might provide total supply and consumption figures: however, one would just draw the quite pleonastic conclusion that the desired property holds whenever supply is sufficiently generous and consumption prudentially limited. Instead, in the proposed approach we are able to verify the target property “on the fly”, whatever the sequence of performed actions and the involved quantities. Moreover, we are also able to try to repair an unwanted situation and regain a satisfactory state of affairs.
Below we provide another example that, though simple, is in our opinion significant as it is representative of many others. Namely, we assume that an agent manages a FIFO queue, thus accepting operations of pushing and popping elements on/from the queue. The example thus models in an abstract way the very general and widely used architecture where an agent provides a service to a number of ’consumers’. We establish the constraint, represented below in our formalism, that the queue must not contain any duplicated elements e1 and e2. From an ethical point of view, this means that customers cannot reiterate a request of service if their previous one have not been processed. This in order to ensure fairness in the satisfaction of different customers’ requests. The possible agent’s actions are: pushA(Req; Q), that inserts a generic value Req in the queue, representing (in some format) a request of service from another agent (each inserted element is given an index ei); popA(e; R), that extracts the oldest element from the queue, i.e., the request to be presently satisfied. The constraint considers an unknown number of pushing actions happened in the past (and thus are now recorded as past events) and can foresee an unknown number of future popping actions. pushP +(Req; Q) :
N (in queue(e1 ; R1 ); in queue(e2 ; R1 )) ::: popA+(eRQ) 3.4
We implemented and we have been experimenting the proposed approach within the
DALI multi-agent system [
The instance size (number of elements to push and pop on the queue) can be established by the user when starting a test session. The items to pop/push are, in the experiments, randomly-generated numbers. In Figure 1 and Figure 2 we show the execution time of the two solutions at the growth of the instance size. In Figure 3 we show the difference in percentage between the execution times.
All figures refer to a dataset of up to 500 elements to push and pop. This has been sufficient to identify an initial “unstable” stage and then a trend that further consolidates with the growth of the instance size. 5 We thank former Ph.D. student Dr. Alessio Paolucci who has practically performed the experiments.
Fig. 1. x axis: instance size; y axis: execution time, blue bars pure Prolog green bars DALI
What we can see is that, when the number of events that we consider is small, then the two solutions are more or less equivalent, the Prolog one a bit better as it involves no overhead (while the DALI implementation itself and the DALI events management necessarily involves some). But, as soon as the instance size grows, the DALI solution becomes better and better in a very significant way, despite the overhead of the DALI implementation6. We can thus conclude that the new constructs that we propose are not only expressive and then useful for expressing problem features in a compact and declarative way, but they also improve efficiency and thus effectiveness of solutions. 4
In this paper we have extended past work so as to devise a toolkit for run-time selfchecking of logic-based agents. The proposed toolkit is able to detect and correct behavioral anomalies by using special meta-rules, and via dynamic constraints that are also able to consider partially specified sequences of events that happened, or that are expected to happen. The experiments, performed in the DALI language, have shown that the proposed approach is computationally affordable.
There are relationships between our approach and event-calculus formulations [
Future work includes making self-checking constraints adaptable to changing conditions, and devising a useful integration and synergy with declarative a-priori verification techniques.