Commitment Tracking via the Reactive Event Calculus

1 Introduction

Since the introduction of social semantics of agent interaction [Singh, 1998], social commitments have become a central notion in multiagent research. One of the main reasons why they became popular is that they lend themselves to verification. Agents are treated as if they were black boxes, which modify the environment via actions, and send/receive messages. Interaction protocols are specified outside of agents, independently of their architecture. Whether agents interact properly or not, that depends on their external behaviour, but not on their internal status.

By interacting or by performing actions, agents manipulate commitments [Singh, 1999], whose status could be inspected to verify how agents are behaving, or what is expected of them. This form of verification should ideally be carried out at runtime, and it is what we call commitment tracking. Being verifiability one of social semantics' main motivations, one would expect that commitment tracking is a routine task which makes use of well-known procedures: but this is not the case, and runtime verification is an open issue to date. 1

We thus propose a framework for commitment tracking based on SCIFF and on the Event Calculus. The framework features a flexible, declarative encoding of the Event Calculus and of the theory of commitments, which can easily be customized and extended. The commitment theory we implement is mainly based on Yolum and Singh's formalization [2002], but it also has temporal elements in the style of Mallya and Huhns [2003] since it features an explicit treatment of time. This is necessary for real-world applications, where temporal constraints and deadlines are ubiquitous.

∗Work supported by the FIRB RBNE05BFRK project TOCAI.it. 1 Notably, two EU projects, FP5's "SOCS" and FP6's "CONTRACT" are largely concerned with runtime verification.

After giving the necessary background notions, we informally discuss the requirements of a commitment tracking framework. We then present our language and procedure, discuss its formal properties, and show a working example.

2 The Event Calculus

The Event Calculus (EC) was introduced by Kowalski and Sergot [1986] for representing and reasoning about events and their effects. Basic concepts are that of event, happening at a point in time, and property (or fluent), holding during time intervals. Fluents are initiated/terminated by occurring events. There are many different axiomatizations of the EC. A simple one, taken from [Chittaro and Montanari, 2000], is the one below (P stands for Property, E for Event):

Axioms ec1 and ec2 are the general ones of EC, whereas ec3 and ec4 are used-defined, domain-specific axioms. Sometimes initially(P) is used to define properties that hold at the beginning of time. Dual axioms and predicates, such as declipped can be added to define when properties do not hold and to model actions with duration [Shanahan, 1999].

The EC framework has been extensively used in the literature to carry out two main reasoning tasks: deductive narrative verification, to check whether a certain fluent holds, given a narrative (set of events) [Kowalski and Sergot, 1986], and abductive planning, to simulate a possible narrative which satisfies some requirements [Shanahan, 2000]. These tasks take place after or prior to execution, but not during execution. The reason why the EC-in its above formulationis not used at runtime is that each time an event occurs, it enables a straightforward update of the theory (it suffices to add happens fact), but it incurs a substantial increase of the query time, since backward reasoning has to be restarted from scratch. However, runtime reasoning tasks, such as monitoring, would greatly benefit from such a powerful framework. For this reason, Chittaro and Montanari [1996] proposed a mechanism to cache the outcome of the inference process every time the knowledge base is updated by a new event. The Cached Event Calculus (CEC) computes and stores the maximum validity intervals (MVIs) of fluents, i.e., the maximum time intervals in which fluents hold, according to the known events. The set of cached MVIs is then extended/revised as new events occur or get to be known.

3 Social commitments

Social commitments are commitments made from an agent to another agent to bring about a certain property. They are a well-known concept in Multi-Agent Systems (MAS) research [Castelfranchi, 1995; Singh, 1999]. Representing the commitments that the agents have to one another and specifying constraints on their interactions in terms of commitments provides a principled basis for agent interactions [Torroni et al., 2009]. Commitments also serve as a natural tool to resolve design ambiguities. Finally, the formal semantics enables verification of conformance and reasoning about the MAS specifications to define core interaction patterns and build on them by reuse, refinement, and composition.

Central to the whole approach is the idea of manipulation of commitments: their creation, discharge, delegation, assignment, cancellation, and release. Commitments are stateful objects that change in time as events occur. Time and events are, therefore, essential elements. Some authors distinguish between base-level commitments, written C(x, y, p), and conditional commitments, written CC(x, y, p, q) (x, y are agents, called debtor and creditor; p, q are properties). CC(x, y, p, q) signifies that if p is brought out, x will be committed towards y to bring about q.

The EC is a suitable formalism to specify the effects of commitment manipulation and reason upon such operations. Yolum and Singh [2002] have shown how commitments can be embedded in a logical framework based on the EC. As a sample fragment of such a formalization, consider a create operation, whose purpose is to establish a commitment, and can only be performed by the debtor. To express that an event e(x) carried out by x at time t creates a commitment c, Yolum and Singh define the operation create(e(x),C(x, y, p)) in terms of happens(e(x), t) ∧ initiates(e(x), C(x, y, p), t).

4 Tracking social commitments

Example 1. A customer has signed a service agreement with a printer supplier: if a printer breaks down, the supplier guarantees to send a technician on site. The technician must intervene within three days from the call. Any delay in the intervention will incur from the supplier's side an obligation to pay a $10 penalty per day of delay, as of the fourth day.

The supplier's contractual obligations could be represented by commitments. Commitment tracking is the automated process of verifying the status of commitments. In the example above, it can serve to verify that the service agreement is respected and, in case of delays, that the corresponding penalty is paid. A commitment tracking framework should comprise a language and a procedure, implemented into a tool.

The language must be expressive enough to define (i) obligations (commitments), (ii) deadlines to be respected, and (iii) compensations actions, such as those arising from deadline expiration.

The procedure keeps track of the obligations at each given moment. It should lend itself to an efficient implementation, to enable early detection of expiring deadlines. Most importantly, it must provide some guarantees. First of all, its output must be provably sound. Moreover, it should be complete, in the sense that it should provide all the relevant information about the relevant commitments. A tool that sometimes "forgets" to indicate some duties cannot be trusted. Finally, it must provide stable, irrevocable answers.

5 The Reactive Event Calculus

The EC can be elegantly formalized using logic programming, but as we mentioned above, that would be suitable for top-down, backward computation, and not for runtime monitoring. For this reason, we resort to a framework which reconciles backward with forward reasoning: the SCIFF language and proof-procedure [Alberti et al., 2008].

SCIFF is an extension of Fung an Kowalski's IFF proofprocedure for abductive logic programming [1997], in which abduction is adopted to enable forward reasoning via integrity constraints. SCIFF has two primitive notions: events (mapped as H atoms) and expectations (mapped as E/EN atoms). H(E, T) means that an event E has occurred at time T , and it is a ground atom. Atoms E(E, T ) and EN(E, T ) instead are not necessarily ground. They can contain variables with domains and be associated with constraint logic programming (CLP) constraints. E(E, T) denotes that an event unifying with E is expected to occur at some time in the range of T. EN(E, T) denotes that all events unifying with E are expected to not occur, at all times in the range of T .

SCIFF accommodates existential and universal variable quantification and quantifier restriction, CLP constraints, dynamic update of event narrative and it has a built-in runtime protocol verification procedure. The verification features of SCIFF are discussed in relation with alternative temporal logic-based approaches by Montali et al. [2008].

A SCIFF specification is composed of a knowledge base P, a set of ICs (integrity constraints) IC, a set of abducible expectations A, and a goal G. P consists of backward rules head ← body (see ax1 below), whereas the ICs in IC are forward implications body → head (see ax2). ICs are interpreted in a reactive manner; the intuition is that when the body of an IC becomes true (i.e., the events in its body occur), then the rule fires, and the expectations in the head are generated by abduction. For example, H(a, T) → EN(b, T ′ ) defines a relation between events a and b, saying that if a occurs at time T, b should not occur at any time; H(a, T) → E(b, T ′ ) ∧ T ′ ≤ T + 300 says that if a occurs, then an event b should occur no later than 300 time units after a.

To exhibit a correct behavior, given a goal G and a triplet 〈P,A, IC〉, a set of abduced expectations must be fulfilled by corresponding events. The SCIFF semantics [Alberti et al., 2008] is given for a given specification and a narrative, denoted by H, i.e., a set of H atoms. Intuitively, it states that P, together with the abduced expectations, must entail G ∧ IC, E expectations must have a corresponding matching happened event, and EN expectations must not have a corresponding matching event. The distinguishing feature of our SCIFF implementation of the EC is that, thanks to SCIFF, it is not goal-directed but event-driven, thus reactive. Thus its name, reactive event calculus (REC). The status of fluents is updated at runtime as events occur. In this sense, we draw inspiration from Chittaro and Montanari's idea of MVIs.

The basic predicates of the calculus are presented below (Axioms ax1 through ax7). Events and fluents are terms and times are integer (CLP) variables, 0 being the "initial" time. REC uses the abduction mechanism to generate MVIs and define their persistence. As opposed to CEC, which is implemented by a special-purpose algorithm, REC has a fully declarative axiomatization, and thanks to the SCIFF framework no ad-hoc implementation is needed. REC uses two special internal events (clip/declip) to model that a a fluent is initiated/can be terminated. The expressive power of REC is the same as the one of CEC, specifically it enables the definition of a context. A use case will be shown later below.

Axiom 1. A fluent F holds at time T if an MVI containing T has been abduced for F : 2

Axiom 2. If (Ts, Te] is an MVI for F, then F must be declipped at time Ts and clipped at time Te, and no further declipping/clipping must occur in between:

Axiom 3. If a fluent initially holds, a corresponding declipping event is generated at time 0:

Axiom4. If an event E initiating a fluent F occurs at time T, either F already holds or it is declipped:

Note that (ax4) does not use the holds at predicate and it does not incur a newMVI.

Axiom 5. The happening of a declip(F) event causes fluent F to start holding:

2 A fluent F does not hold at the time it is declipped but it holds at the time it is clipped, i.e., MVIs are left-open and right-closed.

Axiom 6. If an event E terminates a fluent F, F is clipped: 3

Axiom 7. A (special) complete event terminates all fluents:

6 Formal properties of REC

REC is implemented on top of SCIFF, it thus inherits its soundness and completeness results of the declarative semantics with respect to the SCIFF's operational semantics.

Theorem 1 (Soundndess and completeness of REC). REC is sound and complete. Specifically, the SCIFF proofprocedure will derive all and only the answers defined by its declarative semantics, augmented with the REC axioms ax1ax7.

These are important results. The REC operational behaviour of is faithful to its specifications, i.e., it returns all and only correct answers with respect to the EC axiomatization given in Section 5. We are unaware of other reactive implementations of the EC that provide such a guarantee.

The next results concern uniqueness and irrevocability, and they are especially significant for the commitment tracking application. We thus need to introduce some information about the operational behaviour of SCIFF.

6.1 Open, closed and semi-open reasoning

SCIFF features two main forms of derivation, called open and closed. Given a specification S and two narratives Hi and Hf ⊇ Hi , if there exists an open successful derivation [Chesani, 2007] for a goal G that leads from Hi to Hf we write SHi∼Hf Δ G, where Δ is the computed abductive explanation. 4 If S is a REC specification, Δ includes the abduced MVIs. When SCIFF executes an open derivation, it assumes that the acquired execution trace is partial. Thus E atoms without a matching H atom are not considered to be violated but only pending: further events may still occur to fulfill them. EN atoms can instead be evaluated, because they must never have a matching H atom. This approach is used when SCIFF is used for runtime verification, with events occuring dynamically, and the narrative is incomplete. SCIFF can also perform closed derivations, to reason upon narratives known to be complete, or to close the reasoning process when the flow of events comes to an end. In that case, both E and EN atoms are evaluated: a closed world assumption is made about the collected execution trace, and pending expectations are considered to be violated, because no further event will occur to fulfill them.

SCIFF is sound and complete independently of the order in which it acquires and processes events. However, there are many important domains in which we can safely assume that events are acquired in increasing order of time. In that case, reasoning is partially open: open on the future, when events may still occur, but closed on the past. Expectations on the past can thus be evaluated immediately. This form of semi-open reasoning is achieved by a rule, inside the SCIFF proof-procedure, which states that if an execution trace has reached time t, then all pending expectations must be fulfilled by some time t′ ≥ t. Semi-open derivation is denoted by ∼.

3 Although (ax6) could be defined symmetrically to (ax4), the present (equivalent) formulation produces a better performance.

4 Below we omit Hi since Hf ⊇ Hi and Δ only depends on Hf .

6.2 Irrevocability of REC

The commitment tracking domain enables semi-open derivation. It would be desirable that MVIs once generated are never retracted. If that is the case, the inference process is said to be irrevocable.

We restrict ourselves to cases in which tracking makes sense. To this end, we define "well-formed" theories, which capture the notion of causality (today's events have no impact on yesterday's status of fluents). We then show that semiopen reasoning from such theories is irrevocable.

Definition 1 (Well-formed REC theory). A well-formed REC theory T is a set of clauses 5

which satisfies the following properties:

1. negation is not applied to holds at predicates;
2. for initiates/3 clauses, fluent F must always be resolved with a ground substitution.
3. ∀holds at(F2, T2) predicate used in body, T2 ≤ T .

Definition 2 (REC specification). Given a well-formed REC theory T , the correspondingREC specificationRT is defined as the following SCIFF specification: 6

where KBREC = {(ax1), (ax7)}, {E,EN, mvi} is the set of all possible expectations and MVIs, and ICREC = {(ax2), (ax3), (ax4), (ax5), (ax6)}.

The following three lemmas establish some interesting properties of REC, defining the link between MVIs and the internal events used to clip and declip them.

Lemma 1. For each well-formed REC theory T and execution trace H, given the goal true, the abduced MVIs always have a ground starting time, i.e.,

Lemma 2. The expectation about the clipping of an MVI can be fullfilled by exactly one happened event, in particular the nearest one occurring after the declipping of the MVI.

Lemma 3. In order for a fluent to be declipped by two distinct events, at least one clipping event must occur in between.

We are now ready to state the following:

Theorem 2 (Uniqueness of derivation). For each wellformed REC theory T and for each execution trace H, there exists exactly one successful semi-open derivation computed by SCIFF for the goal true, i.e. ∃1Δ s.t. S ∼HΔ true.

5 The body can be omitted when true.

6 Below, R denotes a generic REC specification. For brevity, we will say that a REC specification is well-formed when its theory is.

Theorem 2 ensures that exactly one Δ is produced by a semi-open derivation of SCIFF; this, in turn, means that there exists exactly one "configuration" for the MVIs of each fluent. We give a precise definition of this notion of state, which is the one of interest when evaluating the irrevocability of the reasoning process, and define the notion of progressive extension between states, which formally defines irrevocability.

Definition 3 (Current time). The current time of an execution trace H, ct(H), is the latest time of its events:

Definition 4 (MVI State). Given a REC specification R and an execution trace H, the MVI state at time ct(H) is defined as the set of mvi abducibles contained in the computed explanation generated by SCIFF with goal true:

Definition 5 (State sub-sets). Given a REC specification R and a (partial) execution trace H, the current state MVI(RH) is split into two sub-sets:

• MVI (RH), is the set of MVIs whose termination is a ground time (closed MVIs):

• MVI (RH), is the set of MVIs whose termination is a variable time (open MVIs):

Definition 6 (Trace extension). Given two execution traces H1 and H2 , H2 is an extension of H1 , written H1 ≺ H2 , iff

Definition 7 (State progressive extension). Given a wellformed REC specification R and two execution traces H1 and H2 , the state of RH2 is a progessive extension of the state of RH1 , written MVI(RH1 ) ⊴ MVI(RH2 ), iff

1. the set of closed MVIs is maintained in the new state: MVI (RH1) ⊆MVI (RH2);
2. if the set of MVIs is extended with new elements, these are declipped after ct(H1 ):

∀ mvi(f, [s, t]) ∈ MVI(RH2 )\MVI(RH1 ), s > ct(H1 )

1. ∀ mvi(f, [s, Te]) ∈ MVI (RH1), either
2. (a) it remains untouched in the new state:
3. mvi(f, [s, Te]) ∈ MVI (RH2), or
4. (b) it is clipped after ct(H1 ): mvi(f, [s, e]) ∈ MVI (RH2), e > ct(H1 ).

Progressive extensions capture the intuitive notion that a state extends another one if it keeps the already computed closed MVIs as they are, and it affects only the status that fluents assume after the latest time of the first state. The extension is determined by adding new MVIs and by clipping fluents which used to hold at the previous state. We can state the main result related to irrevocability: extending a trace results in a progressive extension of the state of MVIs.

Lemma 4. Given a well-formed REC specification R and two execution traces H1 and H2 ,

Theorem 3 (Irrevocability of REC). Given a well-formed REC specification with goal true and a temporally ordered narrative, each time a new event is processed by SCIFF, the new MVI state is a progressive extension of the previous one.

Therefore REC, used in combination with a theory of commitments, fulfills all the requirements identified in Section 4. The language offers a declarative, intuitive language for representing obligations, deadlines, and compensation actions. The inference procedure provides sound, complete and irrevocable answers at runtime.

7 Commitment tracking via REC

We demonstrate the features of REC using the example introduced in Section 4. We adopt the formalization of commitments in EC given by Yolum and Singh [2002]. The resulting framework accommodates conditional commitments, although for lack of space we do not illustrate them. We focus instead on deadlines and compensations. To enable runtime monitoring, we assume that an external clock is available, and that special tic events signal the passing of time.

7.1 Detecting deadline expiration

To illustrate flexibility and expressiveness, we extend the commitments theory-twice: by adding temporal constraints, and by introducing a finer-grained notion of violation. This notion distinguishes between a "partial" violation (a deadline has expired but there may be a belated make-up action) and a "full" violation (too late). We consider a very common temporal constraint: a relative deadline about the discharging of the commitment. The idea is that the user can specify that a certain commitment must be fulfilled within a certain interval TD, as of the time the commitment has been established. The user specifies TD, and if the commitment has been established at (absolute) time T, then it should be satisfied within the (absolute) time (T +TD).

We first introduce the fluents representing the status of commitments.

For each c(X, Y, P), a fluent waiting(c(X, Y, P)) holds if c(X, Y, P) has been established, and the deadline has not expired yet. An commitment discharging event has two effects: it terminates the waiting(c(X, Y, P)) fluent, and it instantiates a new satisfied(c(X, Y, P )) fluent, meaning that the commitment has been successfully discharged.

We then introduce a fluent d check(F, TD), meaning that a commitment F should be satisfied by TD.

The fluent can be instantiated as follows:

where deadlines(c(X, Y, P),Delay) is a user-defined fact stating that commitment c should be satisfied within Delay time units from its instantiation.

If the deadline expires and the commitment is still waiting, the status of the commitment becomes partially violated: partially, because the deadline has expired, but something discharging the commitment could still happen. A fluent p viol(c(X, Y, P),When) indicates that a deadline for c has expired, while c should have been satisfied by time When.

Axioms ex1-ex5 represent this new "theory of deadlines" for social commitments. It is a fully customizable theory, which a user can define and apply to many problems.

A domain-specific knowledge base specifying the example discussed in Section 4 is instead specified as follow:

ex6 states that the event printer broken establish the commitment of the supplier, towards us, to repair the printer; ex7 adds the information that such type of commitment should fulfilled within 3 days form the commitment establishment; finally, ex8 specifies that the event work on printer satisfies any commitment about the repair action.

7.2 Compensation

Users can also define compensation axioms. Compensation mechanisms come in hand when commitments are violated. They are important to tackle undesired situations, and to add robustness to the overall system. In our example, a compensation consists of a new commitment for the supplier to pay a penalty fee, whose amount depends on how many days have passed since the deadline expired at the time the printer is repaired. Note that until the technician is on site, it is not possible to correctly evaluate the extent of the new commitment. Such a situation is captured by the following axiom:

where the new commitment pay penalty is instantiated by any event E discharging the repair commitment, if such a repair commitment has a deadline expired at time When. The penalty is calculated based on a difference between two variables.

7.3 Running a monitoring process

Let the following events be observed at runtime:

h(event(printer broken), 12) h(event(work on printer), 19) h(event(tic), 16) h(event(end monitoring), 22)

h(event(tic), 18)

In this narrative, the printer breaks down, and the technician arrives on site seven days later. Our example includes a penalty for each day passed after the third one. We then expect the printer supplier to be charged $40 as a compensation.

Figure 1 shows the runtime output of REC+SCIFF. At time 12 the printer breaks down (printer broken). Three fluents are thus instantiated: c(shop, us, repair), meaning that the shop gets committed to repair the printer, following ex6; waiting(c(. . .)), meaning that the commitment is waiting to be satisfied (ex1); and d check(c(. . .), 15), meaning that the commitment c must be satisfied by time 15 (ex4).

Nothing happens until the clock signals time 16 (tic), when the deadline check fluent is clipped (it stops holding), because of the deadline expiring (the axiom about such fluent's termination has not been reported here). At the same time the fluent p viol(c(. . .), 15) is initiated (and waiting terminated), meaning that commitment c(shop, us, repair) has been partially violated, i.e., it has not been discharged within the deadline (following ex5). Note that the commitment is not clipped. That is an arbitrary choice we made in this example, and implementing a different behaviour could be achieved by simply adding a termination axiom.

At time 19, a technician arrives on site and repairs the printer, which terminates c(shop, us, repair). A repair fluent is initiated and indicates that such a property has been achieved. The waiting fluent is instead terminated. Since the commitment to repair the printer was partially violated, a new commitment about paying the fee is created (ex9). Note that since the technician arrived at time 19, while he was supposed to intervene by time 15, shop must pay a four-day, $40 fee.

8 Conclusions

We identified the problem of commitment tracking in multiagent systems. We observed that there is no solution to it in the state of the art. Specifically, we are not aware of any other work directly related to commitment tracking which satisfies some fundamental requirements of the language and of the formal implement. Related work on runtime verification of commitments and contracts mainly consist of ad-hoc, tailored procedures that are not easily modifiable and whose formal properties are not easy to determine. We therefore provided the first formal and operational approach to the problem. We showed that in order to address it one can use a REC implementation in SCIFF. Future work will focus on performance evaluation and on the integration of REC with the other forms of reasoning enabled by SCIFF, mainly with abduction.