In this paper we investigate multiagent systems whose agent interaction is based on social commitments that evolve over time, in presence of (possibly incomplete) data. In particular, we are interested in modeling and verifying how data maintained by the agents impact on the dynamics of such systems, and on the evolution of their commitments. This requires to lift the commitment-related conditions studied in the literature, which are typically based on propositional logics, to a first-order setting. To this purpose, we propose a rich framework for modeling data-aware commitment-based multiagent systems. In this framework, we study verification of rich temporal properties, establishing its decidability under the condition of “state-boundedness”, i.e., data items come from an infinite domain but, at every time point, each agent can store only a bounded number of them.
Introduction
In this paper we investigate multiagent systems (MASs) whose agent interaction is based
on social commitments that evolve over time, in presence of possibly incomplete data.
MASs based on social commitments have been extensively studied in the literature
[
As a result, we obtain a powerful framework of data-aware commitment-based
MASs (DACMASs), which incorporates the typical notions of commitment-based MASs
? This paper is a short version of [
Our main result is that, when a DACMAS is state-bounded, i.e., the number of
data that are simultaneously present at each moment in time is bounded, verification
of rich temporal properties becomes decidable. More specifically, we are able to check
DACMASs against properties expressed in a sophisticated first-order variant of
µcalculus with a controlled form of quantification across states. We do this by exploiting
recent results in [
Preliminaries
Description Logics (DLs) [
N | P [i] | C u C
R !
P | P [i1, . . . , ih] where h 2 and for i1, . . . , ih, which denote pairwise distinct components of relation P , we have that {i1, . . . , ih} ✓ { 1, . . . , n}, where n is the arity of P . Similarly, i 2 {1, . . . , n}. Intuitively, u denotes concept conjunction, while P [i1, . . . , im] denotes the projection of relation P on its components i1, . . . , im. This results in a concept if m = 1 and in a relation otherwise.
Formally, the semantics of DLs is given in terms of first-order interpretations I = ( I , ·I ), where I is a nonempty interpretation domain, and ·I is an interpretation function, assigning to each concept C a subset CI of I , and to each n-ary relation R an n-ary relation RI over I such that
(C1 u C2)I = C1I \ C2I (P [i1, . . . , im])I = {(o01, . . . , o0m) | there is o 2 P I s.t. o[ij ] = o0j , for j 2 { 1, . . . , m}} (Here, o[i] denotes the i-th component of tuple o.) Also, ·I assigns to each constant a an object aI of I . We adopt the unique name assumption, i.e., a1 6= a2 implies a1I 6= a2I .
In DLs, knowledge about the domain of interest is encoded in an ontology O = hT , Ai, which is formed by a TBox T , encoding intensional knowledge, and an ABox A, encoding extensional knowledge about individuals objects.
A DLR-Lite TBox is a finite set of assertions of the form:
E1 v E2 (concept/relation inclusion assertion),
E1 v ¬E2 (concept/relation disjointness assertion),
(key i1, . . . , i`: R) (key assertion),
where R has arity n, and 1 i1 < i2 < · · · < i` n. To ensure decidability of
inference, and good computational properties, we require that no relation P can appear
both in a key assertion and in the right hand side of a relation inclusion assertion [
A DLR-Lite ABox is a finite set of assertions of the form:
N (a1) (concept membership assertion),
P (a1, . . . , an) (relation membership assertion), where P has arity n, and a1, . . . , an denote constants.
The semantics of an ontology is given by stating when an interpretation I satisfies an assertion, where I satisfies: E1 v E2, if E1I ✓ E2I ; E1 v ¬E2, if E1I \ E2I = ; ; (key i1, . . . , i`: R), if there are no two distinct tuples in RI that agree on all their components i1, . . . , i`; N (a1), if a1I 2 N I ; and P (a1, . . . , an), if (a1I , . . . , aIn) 2 P I . A model of an ontology O = hT , Ai is an interpretation that satisfies all assertions in T and A. An ontology O is satisfiable if it has at least one model, and it logically implies an assertion ↵ , written O |= ↵ , if all models of O satisfy ↵ .
Next we introduce queries, whose answers, as usual in ontologies, are formed by constants denoting individuals explicitly mentioned in the ABox. A union of conjunctive queries (UCQ) q over an ontology hT , Ai is a FOL formula of the form Wn
i=1 9 yi.conj i(x, yi) with free variables x and existentially quantified variables
y1, . . . , yn. Each conj i(x, yi) in q is a conjunction of atoms of the form N (z), P (z),
where N and P respectively denote a concept and a role name occurring in T , and z, z
are constants of A or variables in x, y1, . . . , yn. The (certain) answers to q over hT , Ai
is the set ANS(q, T , A) of substitutions ✓ of the free variables of q with constants in A
such that q✓ evaluates to true in every model of hT , Ai, denoted hT , Ai |= q✓ . DLR-Lite
enjoys nice computational properties, in particular w.r.t. query evaluation: computing the
certain answers to a UCQ can be done in polynomial time in the size of hT , Ai, and in
AC0 in the size of A alone (i.e., in data complexity) [
We also consider ECQs, which are FOL queries whose atoms are UCQs evaluated
according to the certain answer semantics above [
Q !
[q] | ¬Q | Q1 ^ Q2 | 9 x.Q
The (certain) answers to Q over hT , Ai, is the set of substitutions ✓ of the free variables
of Q with constants in A defined by composing the certain answers of the UCQs q in Q
through first-order constructs, and interpreting existential variables as ranging over the
constants in A. Hence, the first-order constructs in ECQs are interpreted under a (weaker)
epistemic semantics. ECQs over DLR-Lite ontologies enjoy the same computational
properties as UCQs, in particular FOL rewritability of query answering [
Framework We introduce now our framework for modeling DACMASs. Formally, a DACMAS is a tuple hT , E , X , I, C, Bi, where: (i) T is a global DLR-Lite TBox; (ii) E is a set of predicates denoting events (where the predicate name is the event type, and the arity determines the content/payload of the event); (iii) X is a finite set of agent specifications; (iv) I is a (partial) specification for the institutional agent; (v) C is a contractual specification; (vi) and B is a Commitment Box (CBox). 3.1
The Global TBox
The global TBox represents the key concepts, relations and constraints characterizing
the domain in which the agents operate, so as to provide a common ground for the agent
interaction. Part of this TBox is fixed for every agent system, and is used to model core
notions related to the system itself. The extension of such core notions is maintained
by a single, special institutional agent, which is also responsible for the manipulation
of commitments (cf. Section 3.6). The data maintained by such an agent are publicly
available and can be queried by the other agents, but only modified by the institutional
agent. Specifically, the institutional agent maintains data about the following relations:
– Agent denotes the set of (names of) agents that currently participate to the system.
Since the institutional agent is always part of the system, we fix its name as inst, and
enforce that inst always belongs to the extension of Agent.
– Spec, whose extension is immutable, denotes the set of agent specification names
mentioned in X (cf. Section 3.2).
– hasSpec connects agents with their current specification(s): hasSpec[
Each agent, including the institutional agent, maintains a proprietary DLR-Lite ABox, in which it stores its own data. Such data can be queried only by the agent itself and by the institutional agent, which exploits the results of such queries to keep track of the evolution of commitments. Furthermore, each agent progresses its own ABox during the execution in such a way that it is always consistent with the global TBox T . Notice that the overall collection of ABoxes is not assumed to be consistent with the TBox, i.e., the TBox assertions are only required to be satisfied by each agent individually.
Since, in general, queries may involve the ABoxes of several agents, to disambiguate to which ABox a query atom refers, we augment the vocabulary of the TBox with a location argument that points to an agent. We use R@a(x) to denote an atomic query returning the extension of R in the ABox of a. If a does not point to an agent currently in the system, then R@a(x) evaluates to empty. Beside the special constant inst, we also use self to implicitly refer to the agent that is posing the query (similarly to “this” in object-oriented programming). When clear from the context, we omit @self and just use relations without the location argument. We denote with UCQ ` (resp., ECQ `) the language obtained from UCQ (resp., ECQ) by extending atoms with a location argument. 3.2
Agent Specifications In a DACMAS, agents interact by exchanging messages. A message is sent by a sender agent to a receiver agent, and is about the occurrence of an event with a payload, containing data to be communicated. All agents but the institutional one are only aware of the events they send and receive. As for data, the institutional agent has instead full visibility of all exchanged messages, so as to properly handle the evolution of commitments. Agents determine the events they may send, and also how they react to events, through proactive and reactive rules. Such rules are grouped into behavioural profiles called agent specifications, and model: (i) the possible, proactive emission of an event, directed to another agent (communicative rule); (ii) conditional internal (re)actions, which lead to update the agent ABox when sending/receiving an event to/from another agent (update rule). The update could result in the insertion of new data items (from the countably infinite domain ), not already present in the system.
The exchange of a message represents a synchronization point among the sender, receiver and institutional agent. Hence, the reaction of the three agents is interpreted as a sort of transaction, such that each of them effectively enforces the update on its own ABox only if each of the three resulting ABoxes is consistent with T . An inconsistency could potentially arise when reacting to an event either because the same data item is asserted to be member of two disjoint classes, or because a key assertion is violated.
Formally, an agent specification is a tuple hsn, ⇧ i, where sn is the specification name, and ⇧ is a set of communicative and update rules. Such rules are defined over the vocabulary of T and B, and are applied over the ABoxes of the agent and of inst. This allows the agent to query the status of commitments and obtain the names of the other participants. A communicative rule has the form
Q(r, x) enables EV(x) to r where Q is an ECQ `, and EV(x) is an event supported by the system, i.e., predicate EV/|x| belongs to E . The semantics of a communicative rule is as follows. Whenever Q(r, x) evaluates positively, the agent autonomously selects one of the answers ✓ returned by the query, using it to determine the event receiver and its payload. This states that the ground event EV(x)✓ can be sent by the agent to r✓ , provided that r✓ points to an actual agent name in the system (including the two special names inst and self). Example 1. Consider a DACMAS where customers and sellers interact to exchange goods. We model the behavioural rules for customers and sellers using two agent specifications. To buy from a seller, a customer must register to that seller. A registration request is modeled in the customer specification as:
Spec@inst(sel, seller) enables REQ REG to sel Assuming that each seller maintains its customers and items respectively in relations MyCust and Item, the proposal of an item to a customer is modeled in the seller specification as: MyCust(m) ^ Item(i) enables PROPOSE(i) to m.
Update rules are ECA-like rules of the form: – on EV(x) to r if Q(r, x) then ↵ (r, x) (on-send) – on EV(x) from s if Q(s, x) then ↵ (s, x) (on-receive) where EV/|x| is an event type from E , Q is an ECQ `, and ↵ is an update action with parameters (described below). Each such rule triggers when an event is sent to/received from another agent, and Q holds. This results in the application of ↵ using the actual event payload and receiver/sender. Action ↵ queries the ABox of the agent and of inst, using the answers to add and remove facts to the ABox.
Formally, an update action is an expression ↵ (p) : {e1, . . . , en}, where ↵ (p) is the action signature (constituted by the name ↵ and by a list p of parameters), and {e1, . . . , en} are update effects, each of which has the form [q+(p, x)] ^ Q (p, x) add A, del D – q+ is an UCQ `, and Q is an ECQ ` whose free variables occur all among those of q+; intuitively, q+ selects a set of tuples from the agent ABox and that of inst, while Q filters away some of them.3 During the execution, the effect is applied with a ground substitution d for the action parameters, and for every answer ✓ to the query [q+(d, x)] ^ Q (d, x). – A is a set of facts (over the alphabet of T and B) which include as terms: free variables x of q+, action parameters p and/or Skolem terms f (x, p). We use SKOLEM(A) to denote all Skolem terms mentioned in A. At runtime, whenever a ground Skolem term is produced by applying ✓ to A, the agent autonomously substitutes it with a possibly new data item taken from . This mechanism is exploited by the agent to inject new data into the system. The ground set of facts so obtained is added by the agent to its ABox. – D is a set of facts which include as terms free variables x of q+ and action parameters p. At runtime, whenever a ground fact in D is obtained by applying ✓ , it is removed from the agent ABox.
As in STRIPS, we assume that additions have priority over deletions (i.e., if the same fact is asserted to be added and deleted during the same execution step, then the fact is added). The “add A” (resp. “del D”) part can be omitted if A = ; (resp., if D = ; ). Example 2. Consider three possible reaction rules for the seller. The fact that the seller makes every agent that sends a request become one of its customers is modeled as: on ASK REG from c if true then makeCust (c) where makeCust (x) : {[true] add{MyCust(x)}}. Assume now that the seller maintains the item cart for a customer, using relation InCart(i, c) to model that item i is in the cart of c. The seller reaction to an “empty cart” request is modeled as: on EMPTY CART REQ from c if MyCust(c) then doEmpty (c) where doEmtpy (c) : {[InCart(i, c)] del{InCart(i, c)}}. Note that the effect is applied to each i in the cart of c. Consider now the case where the seller receives a new item i to be sold. It reacts by adding i and deciding its price (denoted with Skolem p(i)): on NEW ITEM(i) from a if true then addItem(i) where addItem(i) : {[true]
add{Item(i), Price(i, p(i))}}.
3 The distinction between q+ and Q is needed for technical reasons, borrowed from [
The institutional agent inst manages the core information of the DACMAS. Its behaviour is (partially) captured by the institutional agent specification I, which differs from the other agent specifications in two respects. First, since inst is aware of all messages exchanged by the other agents and can query their ABoxes, its specification is not only constituted by communicative rules and on-send/on-receive reactive rules, but also by on-exchange rules of the form:
on EV(x) from s to r if Q(s, r, x) then ↵ (s, r, x) where Q and ↵ can query the internal ABox of the institutional agent, and the ABoxes of s and r. To conveniently specify reactions of inst that do not depend on a specific event, but trigger whenever an event is exchanged, we use:
on any event from s to r if Q(s, r) then ↵ (s, r)
Second, I is only a partial specification for inst. In fact, inst is also responsible for the manipulation of commitments, which results in a set of additional on-exchange rules that, starting from the contractual specification (cf. Section 3.4), encode the commitment machines for the commitments involved in the contract. These rules are automatically extracted from the contractual specification (cf. Section 3.6).
Example 3. Consider a portion of institutional agent specification, modeling the creation
of a new agent whenever inst receives a request (whose payload denotes the specification
to be initially followed by that agent). To handle this request, inst uses relation NewA to
store a newly created agent together with is initial specification. The axiom NewA[
on AG REQ(s) from a if ¬(9 x9 y.NewA(x, y)) then create(s) create(s) : { [true]
add{NewA(n(), s))} }
Note that axiom NewA[
In the second step, inst informs itself that a new agent has to be processed; the corresponding reaction finalizes the insertion of the new agent, moving it to the set of participating agents:
on INSERT AG(a, s) from self if true then do ins(a, s) do ins(a, s) : { [true] add{Agent(a), Spec(a, s)}, del{NewA(a, s)} } 3.4
The contractual specification C consists of a set of commitment rules, which are reactive rules similar to on-exchange rules. The main difference is that, instead of actions, they describe (first-order) conditional commitments and their creation: on EV(x) from s to r if Qc(s, r, x) then CCn(s, r, [qp+(s, r, x, y)] ^ Qp (s, r, x, y), Qd(s, r, x, y)) (⇤ ) where n is the commitment name, the ECQ ` Qc is the condition for the creation of the conditional commitment, [qp]+ ^ Qp (where, as in update effects, qp+ is a UCQ `, and Qp is an ECQ ` whose free variables all occur among those of qp+) is the precondition determining the generation of a corresponding base-level commitment, and the ECQ ` Qd is the discharge condition for such base-level commitment. All the aforementioned queries can be posed over the ABoxes of s, r, and inst. We use GET-CC(C) to extract the set of conditional commitments contained in C.
According to the literature, commitments are manipulated either explicitly via
specific events (such as a commitment cancellation or delegation), or implicitly when the
commitment precondition or discharge condition becomes true. The allowed
commitment manipulations, together with the resulting commitment states, are captured by
means of a commitment machine [
Specifically, every commitment in GET-CC(C) is associated to a specific first-order commitment machine, which is activated using the corresponding commitment rule in C of the form above, instantiated possibly multiple times, depending on the agent data. The machine evolves as follows: 1. When an event of type EV is sent by agent a to agent b with payload d, if Qc(a, b, d) is satisfied, an instance of the conditional commitment n is created. The debtor, creditor, and payload of this instance are respectively a, b, and d. 2. Such instance is explicitly or implicitly manipulated by the involved agents. Explicit manipulation is done via specific message exchanges; we consider in particular the case of delegation from the debtor a to a new debtor, and the case of cancellation. Implicitly, instead, the instance can generate one or more corresponding base-level commitment instances: whenever [qp+(a, b, d, v)] ^ Qp (a, b, d, v) is satisfied with actual values v for variables y, the conditional commitment instance creates a base-level commitment instance with payload d and v. Such base-level instance is put into the active state. The discharge condition for this instance is the instantiation of Qd with the involved agents and specific payload, i.e., a is committed to bring about Qd(a, b, d, v). 3. Also a base-level commitment instance is explicitly and implicitly manipulated by the involved agents. Explicit manipulation of an active base-level instance resembles that of conditional commitment instances, with the difference that, when canceled, a base-level commitment instance enters into the violated state. Implicit manipulation determines instead the discharge of the instance as soon as Qd(a, b, d, v) holds, moving the instance from active to satisfied.
Example 4. Consider a commitment rule establishing a conditional commitment that the seller takes whenever it accepts the registration of a customer c. The conditional commitment is about the delivery of items paid by c. Specifically, for each item sold by the seller, if c has paid that item, then the seller commits to ensure that c will hold that item. Note that the two conditions are correlated by the same item, and that a base-level commitment is created for each paid item. This cannot be expressed in propositional logic. Assuming that the seller stores a fact Paid(i, c) if c has paid for i, and that the customer stores a fact Owned(i) whenever it owns i, the commitment rule can be specified as: Note the use of location arguments, reflecting that payments are maintained by the seller, whereas the items owned by the customer are maintained by the customer itself. 3.5
The commitment box B is a set of relations used by inst to maintain the concrete instances of conditional commitments, and the instances of their corresponding baselevel commitments (with their states). In fact, due to the presence of data, commitments do not only require to keep track of the involved agents, but also of the payload associated to each of their instances. Such relations are extracted from the contractual specification as follows. Each commitment CCn(s, r, [qp+(s, r, x, y)] ^ Qp (s, r, x, y), Qd(s, r, x, y)) in GET-CC(C) induces two relations in B, on the basis of the commitment name n and the payloads x and y: (i) nCC/ar, where ar = 2 + |x| for debtor, creditor, and conditional commitment payload; (ii) nC/ar, where ar = 3 + |x| + |y| for debtor, creditor, state, and base-level commitment payload.
Example 5. The commitment in Example 4 induces the following relations in B: DeliveryCC(debtor, creditor) and DeliveryC(debtor, creditor, state, item). 3.6
As anticipated in Section 3.3, the specification of inst must be complemented with a set of additional on-exchange rules, used to properly manipulate the evolution of commitments as the interaction unfolds. Commitment instances are stored by inst using the vocabulary of the CBox B, and evolved through the application of these rules. Specifically, these rules ground the (first-order) commitment machine described in Section 3.4 to each specific commitment of GET-CC(C), according to the “templates” described in the remainder of this section. We denote with CC-RULES(C) all the commitment manipulation rules produced from C.
When discussing the templates, we refer to a commitment rule ⇢ 2 C of the form (⇤ ) in Section 3.4. Notice that, when n, x and y are mentioned in the rule templates, they are meant to be replaced with the actual commitment name and payload variables. CC creation. For each ⇢ 2 C , a corresponding creation rule is obtained, depending on n and x. When the rule triggers, a new instance of the conditional commitment nCC is created, with the actual agents and payload: on EV(x) from s to r if Qc(s, r, x) then create nCC (s, r, x) create nCC (s, r, x) : { [true] add{nCC(s, r, x)} } CC delegation. The delegation of a conditional commitment instance for commitment n is triggered when the old debtor do sends to the new debtor dn a DELEGATE nCC event, specifying in the event payload the creditor and the payload of the instance to be delegated. If such an instance exists, the debtor is updated by inst: on DELEGATE nCC(c, x) from do to dn if nCC(do, c, x) then changedeb nCC (do, dn, c, x) changedeb nCC (do, dn, c, x) : { [true]
add{nCC(dn, c, x)}, del{nCC(do, c, x)}} CC cancelation. The cancelation of a conditional commitment instance for commitment n is triggered when the debtor sends to the creditor a CANCEL nCC event, providing the instance payload. If the instance exists, it is removed: on CANCEL CC(x) from d to c if nCC(d, c, x) then delete nCC (d, c, x) delete nCC (d, c, x) : { [true]
del{nCC(d, c, x)} } C creation. Every conditional commitment instance for relation nCC creates a base-level commitment instance whenever the precondition (whose variables x are grounded with the instance payload) holds with an answer substitution ✓ for variables y. This results in the creation of a new tuple for relation nC with the actual, full payload. This does not depend on the specific exchanged event, but only on the actual configuration of the data. Hence, a single “any-event” rule can be used to manage the creation of all base-level instances at once:
on any event from d to c if true then createC (d, c) where, for each commitment CCn(s, r, [qp+(s, r, x, y)] ^ Qp (s, r, x, y), Qd(s, r, x, y)) in GET-CC(C), action createC (d, c) contains the following detachment effect: [nCC(d, c, x) ^ qp+(d, c, x, y)] ^ Qp (d, c, x, y) add {nC(d, c, active, x, y)} Differently from the propositional formalization of a commitment machine, in which the conditional commitment detaches to a base-level one, in our setting the conditional commitment instance is maintained, and keeps waiting for other situations matching the precondition with different data.
C delegation. It resembles the CC delegation: on DELEGATE nC(c, x, y) from do to dn if nC(do, c, active, x, y) then changedeb nC (do, dn, c, x) changedeb nC (do, dn, c, x, y) : {[true] add{nC(dn, c, active, x, y)}, del{nC(do, c, active, x, y)}} C cancelation. It determines a transition for the base-level commitment instance from the active to the violated state: on CANCEL C(x, y) from d to c if nC(d, c, x, y) then viol nC (d, c, x, y) viol nC (d, c, x, y) : {[true]
add{nC(d, c, viol, x, y)}, del{nC(d, c, active, x, y)}} C discharge. Similarly to the case of C creation, the discharge of base-level commitment instances is handled by a single “any-event” rule, which checks the discharge condition for each active commitment instance with the actual payload, evolving the instance to the satisfied state if it holds:
on any event from d to c if true then dischargeC (d, c) where, for each CCn(s, r, [qp+(s, r, x, y)] ^ Qp (s, r, x, y), Qd(s, r, x, y)) in CC(C), action dischargeC (d, c) contains: [nC(d, c, active, x, y)] ^ Qd(d, c, x, y)
add{nC(d, c, sat, x, y)}, del{nC(d, c, active, x, y)} C removal. A last “any-event” reactive rule is used by inst to remove those instances of base-level commitments that already achieved a final state (sat or viol):
on any event from a to b if true then removeFinal () where, for each base-level commitment relation nC in B, action removeFinal () contains: [nC(d, c, s, x, y)] ^ (s = sat _ s = viol) del{nC(d, c, s, x, y)} Example 6. Assume that the only rule in C is that of Example 4. The following CC creation rule is produced on ACCEPT REG from s to c if MyCust@s(c) then create DeliveryCC (s, c) create DeliveryCC (s, c) : {[true]
add{DeliveryCC(s, c)}} Furthermore, the following C creation and C discharge update actions are produced: createC (d, c) : {[DeliveryCC(d, c) ^ Item@d(i) ^ Paid@d(i, c)]
add{DeliveryC(d, c, active, i)}} dischargeC (d, c) : {[DeliveryC(d, c, active, i)] ^ Owns@c(i)
add{DeliveryC(d, c, sat, i)}, del{DeliveryC(d, c, active, i)}} 4
Execution Semantics The execution semantics of a DACMAS is defined in terms of a transition system that, starting from a given initial state, accounts for all the possible system dynamics, considering all the (possibly infinite) sequences of message exchanges, and all the possible substitutions that the agents choose during the application of update actions to provide concrete values for the Skolem terms. Given a DACMAS S = hT , E , X , I, C, Bi and an initial state 0, the execution semantics of S over 0 is defined by a transition system ⌥ S 0 = h, T [ B , ⌃, 0, )i , where: – ⌃ is a (possibly infinite) set of states. Each state 2 ⌃ is equipped with a function abox that, given the name a of an agent, returns the ABox .abox (a) of a in , if and only if a participates to the system in state , i.e., a belongs to the extension Agent in .abox (inst). Hence, .abox (inst) is always defined. – 0 2 ⌃ is the initial state. We assume that every ABox A in 0 is such that (T , A) is satisfiable, and that Spec(sn) 2 0.abox(inst) if and only if hsn, i 2 X . – ) ✓ ⌃ ⇥ ⌃ is a transition relation.
Instrumental to the definition of the transition system is the extension of answering ECQ ` queries so as to take into account location arguments. Formally, given a TBox T , we define that R@b(x) holds in state from the perspective of agent a under substitution ✓ for x, written T , , a, ✓ |= R@b(x), if:4 n.abox (a) is defined and (T , .abox (a)) |= R(x)✓, if b✓ = self
.abox (b✓ ) is defined and (T , .abox (b✓ )) |= R(x)✓, if b✓ 6= self Note that the semantics supports a sort of dynamic binding of location arguments, using ✓ to substitute a variable location argument with an agent name. This relation extends in the natural way to UCQ ` and ECQ `, considering that quantification ranges over the active domain ADOM( ) of , which is defined as the union of the active domains of the ABoxes maintained by the agents present in . This, in turn, allows us to define the certain answers to Q obtained by agent a in state , denoted ANS`(Q, T , , a), as the set of substitutions ✓ for the free variables in Q such that Q holds in state from the perspective of a, i.e., ANS`(Q, T , , a) = {✓ | T , , a, ✓ |= Q}..
The construction of the transition system ⌥ 0 is given in Figure 1.
S 5
Verification of DACMAS
To specify dynamic properties over DACMASs, we use a first-order variant of µ-calculus
[
The formula µZ. denotes the least fixpoint of the formula . As usual in µ-calculus, formulae of the form µZ. must obey to the syntactic monotonicity of w.r.t. Z, which 4 We assume that ✓ is the identity on data items (including the special constants self and inst). 1: procedure BUILD-TS 2: input: DACMAS S = hT , E , X , I, C, Bi and initial state 0 3: output: Transition system h, T [ B , ⌃, 0, )i 4: ⌃ := { 0}, ) := ; 5: while true do 6: pick 2 ⌃ and a 2 { ag | Agent(ag) 2 .abox (inst)} 7: Fetch all current behavioural rules for a; Calculate enabled events with receivers for a 8: if There exists at least an enabled event then 9: pick an enabled event EV(e) for a with receiver b 10: Ai := APPLY(S, , inst, a, b, EV(e)) 11: ⌃ := ⌃ [ { 0} 12: for all x 2 { ag | Agent(ag) 2 A i} do 13: 0.abox(x) := APPLY(S, , x, a, b, EV(e)) . New inst ABox . Tentatively add a new state 0 TOADD := ; , TODEL := ; for all ↵ (v) 2 ACT do
TOADDSK := ; for all effect “[q+(p, x)] ^ Q (p, x) add A, del D” in the definition of ↵ do for all ✓ 2 ANS`([q+(v, x)] ^ Q (v, x), T , , x ) do
TOADDSK := TOADDSK [ A✓ [p/v] TODEL := TODEL [ D✓ [p/v] . ACT = set of fetched actions pick a substitution ✓ sk of the Skolem terms with data
TOADD := TOADD [ TOADDSK ✓ sk if x = inst then TOADD := TOADD [ { Agent(inst)} return (.abox (x) \ TODEL) [ TOADD states that every occurrence of the variable Z in must be within the scope of an even number of negation symbols. This ensures that the least fixpoint µZ. always exists.
The semantics of µLpECQ` formulae is defined over a possibly infinite transition system ⌥ = h, T [ B , ⌃, 0, )i (cf. Section 4), assuming that ECQ ` queries are posed from the point of view of inst. This does not prevent the possibility to query the ABoxes of the other agents, thanks to the dynamic binding for location arguments. Since µLpECQ` contains formulae with both individual and predicate free variables, we introduce an individual variable valuation v, i.e., a mapping from individual variables x to , and a predicate variable valuation V , i.e., a mapping from the predicate variables Z to subsets of ⌃ . With these three notions in place, we assign meaning to formulae by (Q`)⌥v,V = { 2 ⌃ | T , , inst, v |= Q`} (¬ )⌥v,V = ⌃ \ ( )⌥v,V 2)⌥v,V = ( 1)⌥v,V \ ( 2)⌥v,V )⌥v,V = { 2 ⌃ | 9 d 2 ADOM( ). 2 ( )⌥v[x/d],V } )⌥v,V = { 2 ⌃ | x/d 2 v implies d ✓ ADOM( )
and 9 0. ) 0 and 0 2 ( )⌥v,V } (LIVE(x) ^ [ ] )⌥v,V = { 2 ⌃ | x/d 2 v implies d ✓ ADOM( )
and 8 0. ) 0 implies 0 2 ( )⌥v,V } (Z)⌥v,V = V (Z) (µZ. )⌥v,V = T{E ✓ ⌃ | ( )⌥v,V [Z/E] ✓ E }
Fig. 2. Semantics of µLpECQ` associating to ⌥ , v, and V an extension function (·)⌥v,V , which maps formulae to subsets of ⌃ . Formally, the extension function (·)⌥v,V is defined inductively as shown in Figure 2. When is a closed formula, ( )⌥v,V does not depend on v or V , and we denote the extension of simply by ( )⌥ . A closed formula holds in a state s 2 ⌃ if s 2 ( )⌥ . In this case, we write ⌥, s |= . Given DACMAS S, an initial state 0 and a µLpECQ` formula , we are interested in the following verification problem: ⌥ S 0 , 0 |= . Example 7. Consider the contract of Example 4. Assume that T contains that gold customers are seller customers: MyGoldCust v MyCust. The µLpECQ` property ⌫Z. (8 s, c, i.DeliveryC(s, c, active, i) ^ MyGoldCust@s(c)
! µY.(DeliveryC(s, c, sat, i)) _ (LIVE(s, c, i) ^ hi Y )) ^ [ ]Z models that, for every delivery commitment instance a seller has towards a gold customer, there must exist a run where the instance persists in the system until it is satisfied.
The number of states of ⌥ S 0 is in general infinite, and verification of (even
propositional) temporal properties of simple forms (e.g., reachability) turns out to be undecidable
[
We take this general notion and adapt it to DACMASs. In particular, a DACMAS
is state-bounded if, for every agent active in the system, there exists a bound on the
number of data items simultaneously stored in its ABox. Since the ABox of inst stores
the names of the active agents, this implicitly bounds also the number of simultaneously
active agents. Observe, however, that the overall number of data items (and hence also
agents) encountered across and along the runs of the system can still be infinite. With
this notion in place, we obtain the following fundamental result:
Theorem 1 ([
This means that state-bounded DACMASs can be verified, in principle, using standard model checkers for propositional µ-calculus.
Conclusion
DACMASs are readily implementable in standard technologies such as JADE (which
supports dynamic agent creation) and lightweight ontologies. Observe that a system
execution requires polynomial time at each step (actually logspace w.r.t. the data, as
any system based on relational databases). Only offline verification of the system is (as
usual) exponential in the representation. Our framework complements that of [
We consider extending our framework with the possibility of checking epistemic
properties, in the line of [