This paper deals with run-time detection and possible correction of erroneous and/or anomalous behavior in agents defined in datalog- or prologbased logic languages. In particular, we augment our previous approaches by allowing an agent to explicitly observe and record its past behavior so as to be able to decide its best actions, detect anomalous behavior and try to dynamically correct detected problems.
Agents, in their interaction with the environment, are subject to modify themselves and evolve according to both external and internal stimuli, the latter due to the proactive and deliberative capabilities of the agent themselves.
In previous work, we defined semantic frameworks for datalog-based and
prologbased logical agents that account for: (i) the kind of evolution of reactive and proactive
agents due to directly dealing with stimuli, that are to be coped with, recorded and
possibly removed [
As agent systems are more widely used in real-world applications, the issue of
verification is becoming increasingly important (see [
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. We believe that static verification should be integrated with dynamic self-checking aimed at detecting properties violation and trying to restore an acceptable or desired state of affairs.
The definition of frameworks such as the one that we propose here, for checking
agent behavior during its life based on its experience, has not been widely treated up to
now. In the quest quest for agent platforms whose component entities would be capable
of exhibiting a correct and rigorous behavior with respect to expectations, developers
have frequently applied model-checking techniques (cf. [
In this paper, we propose a method for checking the agent behavior correctness during the agent activity, based on maintaining information on its past “experiences” and behavior. If augmented by time stamps, these records (that we call past events) constitute in a way the history of the agent activity. The set of past events evolves in time, and past events constitute the ground upon which the 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 LTL Expressions, that according to what has happened and to what is supposed to happen in the future define properties that should hold and what should be done if they are violated. Evolutionary LTL Expressions are based upon specifying: (i) a sequence of events that are supposed to have happened; by using a notation obtained from regular expressions, one does not need to completely specify a finite sequence, but is allowed to define partially specified sequences of unlimited length; (ii) a temporal-logic-like expression defining a property that should hold; (iii) a sequence of events that are supposed to happen in the future, without affecting the property; (iv) a sequence of events that are supposed to happen in the future; (v) optionally, “repair” actions to be undertaken if the property is violated. The interval temporal logic adopted for defining properties has been introduced in previous work. Evolutionary LTL Expressions are a novel feature that we introduce in this paper, and that we have (prototypically) implemented and experimented.
Our approach can be adopted in any logic agent-oriented framework, and we
believe that, more generally, evolutionary LTL expressions can be adopted as a
programming construct in event-based extensions to datalog and prolog. In particular, one such
language is DALI [
The paper is structured as follows. In Section 2 we provide the reader with some background, concerning our declarative semantics of evolving agents, and temporal logic (extended to interval temporal logic). In Section 3 we introduce Evolutionary LTL Expressions, that define properties that are supposed to hold, given events that are supposed to have occurred in the past, and events that are supposed to occur or not to occur in the future. These expressions are actually constraints to be verified at run-time. We compare the proposed approach with other approaches to verification in Section 4. We introduce and discuss the problem of the experimental evaluation of the approach in Section 5. Finally, in Section 6 we conclude.
In this paper we will refer to the declarative semantics introduced in [
As a typical situation, perception of an external event will have an effect on the program which represents the agent: for instance, the event will be stored as a new fact. This transforms the program into a new program, that will procedurally behave differently than before, e.g., by possibly reacting to the event. Or, the internal event corresponding to the decision of the agent to undertake an activity triggers a more complex program transformation, resulting in a version of the program where the corresponding intention is “loaded” so as to become executable.
We abstractly formalize an agent as the tuple Ag = < PAg; E; I; A > where Ag is the agent name and PAg (that we call “agent program”) describes the agent behavioral rules. E is the set of the external events, i.e, events that the agent is capable to perceive and recognize: let E = fE1; : : : ; Eng for some n. I is the internal events set (distinguished internal conclusions): let I = fI1; : : : ; Img for some m. A is the set of actions that the agent can possibly perform: let A = fA1; : : : ; Akg for some k. Let Y = (E [ I [ A).
According to this semantic account, one will have an initial program P0 = PAg
which, according to events that happen and actions which are performed, passes through
corresponding program-transformation steps (each one transforming Pi into Pi+1, cf.
[
The different languages and different formalisms in which an agent can possibly be expressed will influence the following key points: (i) when a transition from Pi to Pi+1 takes place, i.e., which are the external and internal factors that determine a change in the agent; (ii) which kind of transformations are performed; (iii) which semantic approach is adopted, i.e., how Mi is obtained from Pi.
We also believe it useful to perform an Initialization step, where the program PAg written by the programmer is transformed into a corresponding program P0 by means of some sort of knowledge compilation. This initialization step can be understood as a rewriting of the program in an intermediate language and/or as the loading of a “virtual machine” that supports language features. This stage can on one extreme do nothing, on the other extreme it can perform complex transformations by producing “code” that implements language features in the underlying logical formalism. P0 can be simply a program (logical theory) or can have additional information associated to it.
Let H be the history of an agent, that is, a set of events that happened and actions
performed by the agent, each one time-stamped so as to indicate when they occurred. In
particular, we introduce a set P of current “valid” past events that describe the state of
the world as perceived by the agent1, and a set PNV where we store all previous ones.
Thus, the history H is the tuple hP; P N V i. In practice, H is dynamically augmented
with new events that happen. Given set Y of events, if one is interested in identifying
the kind of event, a postfix (to be omitted if irrelevant) can provide this indication. I.e.,
XE is an external event, XA is an action and XI an internal event. As soon as X is
perceived by the agent, it is recorded in P in the form XP Y : Ti, Y 2 fE; A; Ig. In
[
tics "Ag of Ag is a tuple hH; P E; M Ei, where H is the history of Ag, and P E and
The next definition introduces the notion of instant view of "Ag, at a certain stage of the evolution (which is in principle of unlimited length).
tionary semantics "Ag = hH; P E; M Ei. The snaphot at stage i of "iAg is the tuple hHi; Pi; Mii, where Hi is the history up to the events that have determined the transition from Pi 1 to Pi.
For defining properties that are supposed to be respected by an evolving system, a
well-established approach is that of Temporal Logic (introduced in Computer Science
by Pnueli [
LTL enriches an underlying propositional logic language with a set of temporal
connectives composed of a number of unary and binary connectives referring to future-time
and past-time. In prior work (see e.g., [
In this section we introduce Evolutionary LTL Expressions, which are aimed at
checking an agent’s behavior at run-time under partially specified sequences of past and future
events. This extends our past work [
According to the evolutionary semantics summarized above, time instants s0s1 : : : concerning an agent’s “life” can be understood in terms of the events that happen. In fact, at the i-th evolution step we have an history Hi, an agent program Pi and its intended semantics Mi, determined by events E1; : : : ; Ei occurred so far. The next evolution step will take place in accordance to the perception of next event Ei+1. Then, any property ' which holds w.r.t. "iAg, i.e. w.r.t. the agent evolutionary semantics up to step i, will keep holding until next event will determine a transition to the next snapshot. In other words, the agent understands the world only in terms of the events that it perceives. Therefore we can define a state si as
si = "iAg = hHi; Pi; Mii: that is, a state is taken to be the snapshot at stage i of the evolutionary semantics of the agent.
In model-checking, the aim is to establish if some LTL formula Op ' or ' Op (where Op can be, for instance, N for “never”, E for “eventually”, etc.) can be established to be true, given a description of the system at hand from which the system evolution can be somehow elicited. In order to cope with the many cases where this evolution cannot be fully foreseen, we propose to exploit temporal logic operators in a different way than before, so as to take into account the events that have happened already and those that are expected to happen or not to happen in the future and that are relevant to the property that we intend to check.
of the form Op ' if operator Op is unary or ' Op if operator Op is binary, where
Evolutionary LTL Expression, is of the form
operator Op occurring in with the following special cases.
– contains an interval operator Opz;x: in this case, x is the state until which is required to hold; – one of the Ji’s happens at state sw, w < x: then, is not required to hold after sw. Notice that both the Fi’s and the Ji’s are optional Notice also that, in general, we cannot foresee when (and in which order) the expected relevant events Fi’s will happen.
In many practical cases, we are unable to provide a full sequence of the expected
events, and in particular to be aware of how many times they will occur. Sometimes, we
will be interested in specifying the (partial) order in which they should occur. Thus, in
the above definition, to be able to indicate the sets of past and future events in a more
flexible way we admit in part the syntax of regular expressions [
zero or more occurrences of E, and E+ one or more occurrences. Given events E1 and
that E1 must occur immediately before E2 (i.e., the two events must be consecutive).
For instance, E1+ X E2; E3 X E4 means that, after a certain (non-zero) number of occurrences of E1 and, possibly, of some unknown event X, E2 and E3 can occur in any order, immediately followed by some unknown event X and, immediately afterwards, by E4. Notice that, for an agent, an event “occurs” when the agent perceives it. This is only partially related to when events actually happen in the environment where the agent is situated. In fact, the order of perceptions can be influenced by many factors. However, either events are somehow time-stamped (in a reliable way) whenever they happen so as to certify the exact time of their origin (as sometimes it may be the case), or an agent must rely on its own subjective experience.
Evolutionary LTL Expressions are easily given a semantics in the context of the Evolutionary Semantics of an agent. Therefore, a given Evolutionary LTL Expression can be evaluated w.r.t. a state, i.e. (as seen above), a snapshot "iAg and will hold whenever Hi encompasses the sequence of events that have been supposed to have occurred (i.e., they occur in Hi in the given order) and holds (i.e., i belongs to the given interval and the formula is true w.r.t. i). According to agent’s activities the agent will evolve to a new snapshot, in particular when a new event happens, either expected or unwanted. In the new snapshot, the given expression can be re-evaluated. This constitutes a “punctual” evaluation of the expression. An expression involving Opz;x can be finally deemed to hold whenever either the interval has expired and has been true in all points, or an unwanted event (one of the Jis) has occurred. Instead, an expression can be deemed not to hold (or, as we often say, to be violated as far as it expresses a wished-for property) whenever is false in some point.
In Definition 3 we do not require the EPi ’s, the Fi’s and the Ji’s to be ground terms. Instead, we admit each of them to contain variables if we are not interested in precisely specifying some of their parameters. For instance, the expression consumeA+(r; Q) (where postfix A as specified before indicates an action) stands for a sequence of events where the action of consuming (some resource r) occurs at least once. Each action will refer to an unspecified quantity Q. All variables occurring in evolutionary LTL expressions are implicitly universally quantified, as customary in datalog- and prologlike logic languages. An evolutionary LTL expression could be for instance (where N stands for the LTL operator “never”):
supplyP +(r; s) : N (quantity (r; V ); V < th) :: consumeA+(r; Q) stating that, after having provided a supply of resource r for a certain total quantity, the agent is expected to consume unknown quantities of the resource itself. The expression defines a constraint requiring that the available quantity of resource r must remain over a certain threshold th. Evolutionary LTL expressions are in fact supposed to act as constraints to be verified at run-time whenever new events are perceived. Notice in fact that the “supply” event is supposed to occur at least once, possibly an unlimited number of times. Interval-LTL formula = N (quantity (r; V ); V < th) will be (re-)evaluated after each occurrence. A violation will happen whenever does not hold.
As another example, consider the following expression stating that, after a car has been submitted to a checkup, it is assumed to work properly for (at least) six months, even in case of (repeated) long trips, unless an accident occurs.
checkupP (Car) : t1 : Gt1;t1+6monthswork ok(Car) :: long trip+(Car) ::: accident (Car)
In the above example we have used the operator Gt1;t2, t2 = t1 + 6months which is an interval LTL operator, G standing for “always”.
We may notice the similarity between evolutionary LTL expressions and
eventcalculus formulations. The Event Calculus has been proposed by Kowalski and Sergot
[
In our opinion, evolutionary LTL expressions might in perspective be considered as a useful programming construct in datalog and prolog (and their extensions). In fact, also by means of interval LTL operators, propositions holding over intervals in a dynamic setting can be expressed in a direct and compact way. Below we state when an evolutionary LTL expression is defined to hold.
Definition 5. An evolutionary LTL expression E , of the form holds in state si whenever (i) some of the EP1 ; : : : ; EPl has happened, some (or none) of the F1; : : : ; Fm has happened, none of the J1; : : : ; Jr has happened, and holds or (ii) some of the J1; : : : ; Jr has happened.
As said before, whenever an unwanted event (one of the Jis) should happen, is not required to hold any longer (though it might). The proposition below formally allows for dynamic run-time checking of evolutionary LTL expressions. In fact, it states that, if a given expression holds in a certain state and is supposed to keep holding after the first expected event has happened, then checking this expression amounts to checking the modified expression where: (i) the occurred event has become a past event, and (ii) subsequent events are still expected. fEP1 ; : : : ; EPl ; FiP g : holds iff EFi holds.
Proposition 1. Given evolutionary LTL expression E = fEP1 ; : : : ; EPl g : :: F :::
J , where F = fF1; : : : ; Fmg and J is the list of unexpected events, assume that E
holds at state sn and that it still holds after the occurrence of event Fi 2 F at state sv
(v n), and that none of the events in J has happened. Let F1 = F n Fi. Given EFi =
:: F1 ::: J we have that for every state sw with (w v) E
In prior work (see e.g., [
Definition 6. An evolutionary LTL expression E , of the form is violated in state si whenever some of the EP1 ; : : : ; EPl has happened, some (or none) of the F1; : : : ; Fm has happened, none of the J1; : : : ; Jr has happened, and does not hold.
Definition 7. An evolutionary LTL expression E , of the form is broken in state si whenever some of the EP1 ; : : : ; EPl has happened, some (or none) of the F1; : : : ; Fm has happened, some of the J1; : : : ; Jr has happened, and does not hold.
Whenever an evolutionary LTL expression is either violated or broken, a repair can be attempted with the aim of recovering the agent’s state. LTL expressions will be “hosted” in some logic agent-oriented programming language L. The repairs will be program fragments written in L to be executed upon violations.
Definition 8. An evolutionary LTL expression with repair E R is of the form:
E jR1 jjR2 where E is an evolutionary LTL expression adopted in a language L, and R1; R2 are program fragments written in L. R1 will be executed whenever F R is violated, and R2 will be executed whenever F R is broken.
Going back to the example of the car, let us assume that, if before six months after a checkup we have a malfunctioning, then one is entitled to get free assistance; in case of an accident instead, one has (say) to call the police. Again, let’s assume that postfix ’A’ indicates actions.
checkupP (Car) : t1 : Gt1;t1+6monthswork ok(Car) :: long trip+(Car) ::: accident (Car) j call f ree assistanceA(Car; Address) jj call policeA(Address) Let us now assume that language L provides distinguished preconditions to actions, i.e., distinguished predicates defining preconditions that are implicitly added to every action. Let us assume that prevent (Action), whenever true, prevents an action from being performed, and allow (Action; Condition) allows an action to be performed only if the specified condition holds2. Then, we assume that an action can be performed only if not prevented and allowed.
The evolutionary LTL expression with improvement listed below states that no more consumption can take place if the available quantity of resource r is scarce. supplyP +(r; s) : N (quantity (r; V ); V < th) :: consumeA+(r; Q) j prevent (consumeA(r; Q)) We might instead adopt another (softer) constraint, that forces the agent to limit consumption to small quantities (say less than quantity q) if it is approaching the threshold (say that the remaining quantity is th + f , for some f ).
supplyP +(r; s) : N (quantity (r; V ); V < th + f ) :: consumeA+(r; Q) j allow (consumeA(r; Q); Q < q) 4
Verification of agent programs can to some extent be performed statically (i.e., prior
to agent activation), by checking the system against any possible input
configuration, sequence of external events, etc., Static verification can be accomplished through
model-checking techniques [
However, the literature reports fully-implemented promising static verification
frameworks (e.g., [
The issue of run-time verification has been considered in recent work. The SCIFF
proof procedure, based on abduction, allows for checking the compliance of a narrative
of events w.r.t. a specification, by matching events w.r.t. expectations, ie., by performing
a form of run-time monitoring (see, e.g., [
We have implemented and we have been experimenting the proposed approach within the DALI multi-agent system (the DALI interpreter is freely available at http://www.di.univaq.it/stefcost/Sito-Web-DALI/WEB-DALI/). In this system, a frequency can be associated to each constraint by means of directives (a default frequency is otherwise provided). One can also establish since when and until when a constraint has to be checked.
An important aspect to be experimentally verified is whether constraints actually empower the agent ability to cope with events without introducing too much overhead, that would lead an agent to that “brittleness” that it is so important to avoid. For performing dynamic checking without specific constructs, one has build, within an agent program, a suitable cyclic structure to perform the needed checks. Our solution therefore, by exploiting the underlying basic cycle of the interpreter, avoids adding this further layer. In this sense, the overhead is in any case alleviated. Nonetheless, a crucial point to consider is that one, when adding new constraints and/or increasing the frequency of checks, has to experimentally verify that the addition/increment is “sustainable” by the interpreter. The experimental evaluation is in fact mandatory under this respect.
In the Appendix we present a basic experiment. Namely, we have implemented an agent that manages a FIFO queue, thus accepting requests of pushing and popping elements on/from the queue. This example is in our opinion significant because it models in an abstract way the very general and widely used architecture where an agent provides a service to a number of consumer. The instance size of our experiments (set by the user) coincides with the number of elements that are pushed/popped (at most 500). We establish the constraint, represented below in our formalism, that the queue must not contain any duplicated elements e1 and e2. The possible actions are pushA(V; Q) that inserts a generic value V in the queue (as the e-th elements) and popA(Q) that extracts the oldest element from the queue (pushP (V; Q) is the past event recording this action having been performed). The constraint considers an unknown number of pushing actions happened in the past (and thus now recorded as past events) and can foresee an unknown number of popping actions.
pushP +(V; Q) : N (in queue(e1 ; V ); in queue(e2 ; V ); e1 6= e2 ) :: popA+(Q)
In particular, in the Appendix we present in Section A the pure prolog code, and in Section B the DALI code. Then, in Figure 1 and Figure ?? we show the execution time of the two solutions at the growth of the instance size. In Figure ?? we show the difference in percentage between the execution times. It is possible to identify an initial “unstable” stage and then a trend that further consolidates with the growth of the instance size. In fact, what we can conclude beyond any doubt is that, when the number of events that we consider is small, the two solutions are more or less equivalent, the prolog one a bit better as it involves no overhead (while the DALI implementation of 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 implementation. 6
In this paper, we have presented an approach to detection and correction of run-time behavioral anomalies by using dynamic constraints. The runtime observation of actual anomalous behavior with dynamic possible correction of detected problems, as opposed to full prior classical program verification and validation on all inputs, can be a key to bringing down the well-known computational burden of the agent behavior assurance problem. Suitable experiments, performed in the DALI language, have shown that the proposed approach is computationally effective, and constitutes and improvement also in terms of efficiency. However, as it happens in all the environments where static and dynamic checks are equally applicable, none of the two forms of verification may substitute the other: indeed, the only possible solution is given by a synergy aimed at creating an integrated, reliable and lightweight verification environment. A
Below we report the code of the version of the Queue agent implemented in DALI (by Alessio Paolucci, that we thank), but using only prolog constructs. The single DALI feature that is exploited is related to the activation of the agent by means of a message. The test agent in fact gets active and performs a test session whenever it receives from the user a message with content run pure test(N um Items) where N um items specifies the number of elements to be pushed/popped on/from the queue.
When the agent receives event run pure test it reacts, thus invoking the run pure testing goal with Times (=Size) as parameter, which starts the ’pushing’ phase. The pushing(T imes) goal pushes an item (through push item subgoal), when T imes > 0, otherwise it ends.
push item as first step retrieves the data structure pqueue(Q). Then, it randomly generates an item, and checks if that item is already present in the queue. If so, then push item fails, and this (and only this) item pushing is skipped. If the new item is not in the queue, then it is added in the head. The old queue is removed from memory (retract(pqueue(Q))), and the new one is stored in the knowledge base (assert(pqueue(N Q)). popping is then invoked, to perform items removal from the queue. It makes use of pop item, a goal that retrieves and unifies the queue through clause(pqueue(Q); ), and the extracts the head of the queue Q. After the ’popping’ phase, the test ends. run pure testE(T imes):> run pure testing(T imes): run pure testing(T imes):- pretty start; now(StartT ime); T 1 is T imes + 1; nl; write(0P U SHIN G:::0); nl; pushing(T 1); nl; write(0P OP P IN G:::0); nl; popping(T 1); now(EndT ime); T estT iming is EndT ime StartT ime; nl; write(0T ime :0); write(T estT iming); nl; pretty end: pushing(0): pushing(T imes):push item:popping(0): popping(T imes):- pop item; T 1 is T imes 1; popping(T 1): pop item:- clause(pqueue(Q); ); nl; write(0P opping :0);
Q = [HjT ]; write(H); retract(pqueue(Q)); assert(pqueue(T )); nl; write(0Queue :0); write(T ); nl: pop item:- assert(pqueue([])): pretty start:- nl; write(0Start testing:::0); nl: pretty end:- nl; write(0T est f inished:::0); nl: B
The DALI implementation makes use of DALI advanced features, and in particular exploits actions, and the ability to remember what happened in the past (past actions). Basically, the power of the DALI infrastructure made us able to write the program in a very comfortable manner: each pushing is an action, so every time the action is performed, the DALI engine takes care, for the future, of this action as a past event. We exploited this feature so as to perform pushing actions in the present. Then, we use parameters of the action to take care of the items that have been pushed and of the order, through an index. When a pop needs to be performed, we use the power of DALI past events to retrieve actions previously performed, and thus retrieve the correct item from the head of the queue, in a very elegant manner. The DALI implementation allows us to concentrate on the problem, without focusing that much on the data structure, in a very strict declarative fashion.
Below we report the code of the proper version of the Queue agent implemented in DALI. The test agent gets active and performs a test session whenever it receives from the user a message with content run dali test(N um Items) where N um items specifies the number of elements to be pushed and popped on the queue. run dali testE(T imes):> dali test startA; run dali testing(T imes): run dali testing(T imes):< dali test startP: run dali testing(T imes):- dali start pushingA; dali pushing(T imes); dali end pushingA; dali start popA; dali popping(T imes); dali end popA; dali end testingA: dali pushing(0):- true: dali pushing(T imes):- dali remember(T imes); T 1 is T imes dali remember(T imes):- random(1; 300; Item); not(clause(do action(dali push queue(Item; ); ); )); get push index(P I); dali push queueA(Item; P I): get push index(I1):- clause(push index(Index); );
I1 is Index + 1; retract(push index(Index)); assert(push index(I1)): get push index(Index):- assert(push index(1));
Index = 1: 1; dali pushing(T 1): C
In Figure 1 below we show the execution time of the two solutions reported in previous sections at the growth of the instance size. It can be observed that as the instance size grows, the DALI solution becomes significantly better.