=Paper=
{{Paper
|id=Vol-1195/long6
|storemode=property
|title=Specification and Verification of Commitment-Regulated Data-Aware Multiagent Systems
|pdfUrl=https://ceur-ws.org/Vol-1195/long6.pdf
|volume=Vol-1195
|dblpUrl=https://dblp.org/rec/conf/cilc/MontaliCG14
}}
==Specification and Verification of Commitment-Regulated Data-Aware Multiagent Systems==
https://ceur-ws.org/Vol-1195/long6.pdf
Specification and Verification of Commitment-Regulated
Data-Aware Multiagent Systems ?
Marco Montali1 , Diego Calvanese1 , and Giuseppe De Giacomo2
1
Free University of Bozen-Bolzano, Piazza Domenicani 3, 39100 Bolzano, Italy
lastname@inf.unibz.it
2
Sapienza Università di Roma, Via Ariosto, 25, 00185 Rome, Italy
lastname@dis.uniroma1.it
Abstract. 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.
1 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
[8]. Intuitively, a social commitment CC(d, c, qp , qd ) models a relationship between a
debtor agent d and a creditor agent c, in which d commits towards c that, whenever
condition qp holds in the system, it will bring about condition qd in the following
course of interaction. Commitments provide a semantics for the agent interaction that
abstracts away from the internal agent implementation, and can be thus employed to
specify business protocols and contracts. The establishment of commitments is regulated
by contracts, which depend on domain-specific events and conditions. Established
commitments, in turn, have a lifecycle that is regulated by a so-called commitment
machine [12] on the basis of such contracts. While in the literature, virtually all the work
is based on propositional contents for such commitments [8], here we explicitly manage
data described through first-order formalisms, in line with [7]. In other words, we study
how data maintained by the agents impact on the dynamics of such systems, and on the
evolution of their commitments. Technically, this requires to lift to first-order the notions
related to contracts, commitments, and commitment machines.
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 [10], to be presented at AAMAS 2014.
84
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
but in a rich, data-aware context. In our framework, the commitment machine itself
becomes a special agent, called institutional, which is a agent, in charge of supporting the
evolution of the system according to the commitments. In addition, this agent manages
core information about the MAS itself, such as the list of participating agents, which
changes over time as the system unfolds. In this light, it maintains and manipulates a
common knowledge base, of interest for all the interacting agents. The data manipulated
by the agents are described in terms of a domain ontology, expressed in a lightweight
description logic (DL), tailored towards ontology-based data access. This ontology
provides a common ground for the agent interaction and commitments, establishing the
vocabulary that is shared by all of them. In particular, we rely on DLR-Lite [5], which is
the n-ary version of the DL at the base of the OWL 2 QL profile of the OWL 2 semantic
web standard. Each agent has its own data about the domain and the contracts it is
involved in, expressed in terms of such ontology. Such data are manipulated through
actions, in response to events and according to the commitments in place. At each point
in time, only a finite number of data is present in the system. However, such data change
over time: old data are removed by the agents, and new data (coming from a countably
infinite domain ) are inserted.
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 [2], and reducing verification of state-bounded DACMASs to finite-state
model checking through a faithful form of abstraction, essentially obtained by replacing
real data items with a finite number of symbolic values, while correctly preserving the
relationships among the real data items themselves.
2 Preliminaries
Description Logics (DLs) [1] are logics that represent the domain of interest in terms of
objects, concepts, denoting sets of objects, and relations between objects. We consider
here the DL DLR-Lite [5], which is a DL that belongs to the DL-Lite family of lightweight
DLs and that is equipped with relations of arbitrary arity. In DLR-Lite, concepts C and
relations R are built from atomic concepts N and atomic relations P (of arity 2):
C ! 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 C I 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}}
85
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
(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 aI1 6= aI2 .
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 [11,5].
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 aI1 2 N I ; and P (a1 , . . . , an ), if (aI1 , . . . , 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 con-
junctive
Wn queries (UCQ) q over an ontology hT , Ai is a FOL formula of the form
i=1 9y i .conj i (x, y i ) with free variables x and existentially quantified variables
y 1 , . . . , y n . Each conj i (x, y i ) 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, y 1 , . . . , y n . 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) [5]. Such result is based on the FOL
rewritability property of DLR-Lite [5], which states that for every UCQ q and TBox T , we
can rewrite q into a new UCQ rew T (q) such that ANS (q, T , A) = ANS (rew T (q), ;, A),
for every ABox A. In other words, the TBox can be “compiled away”.
We also consider ECQs, which are FOL queries whose atoms are UCQs evaluated
according to the certain answer semantics above [4]. An ECQ over T and A is a possibly
open formula of the form (where q is a UCQ):
Q ! [q] | ¬Q | Q1 ^ Q2 | 9x.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
86
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
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 [4].
3 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 specifica-
tions; (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[1] v Agent,
hasSpec[2] v Spec.
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.
87
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
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 specifi-
cation 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)
88
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
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 ap-
plied 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 [2].
89
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
3.3 Institutional Agent Specification
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[1] v
¬Agent is part of T , and enforces that a new agent has indeed a new name. The behaviour
is defined in two steps. In the first step, inst reacts to a creation request by choosing an
agent name (using Skolem term n()). The reaction is applied only if there is no pending
new agent to be processed.
on AG REQ(s) from a if ¬(9x9y.NewA(x, y)) then create(s)
create(s) : { [true] add{NewA(n(), s))} }
Note that axiom NewA[1] v ¬Agent ensures that the update is blocked if the chosen
name is already used in the system.
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:
NewA(a, s) enables INSERT AG(a, s) to self
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 Contractual Specification
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
90
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
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 spe-
cific events (such as a commitment cancellation or delegation), or implicitly when the
commitment precondition or discharge condition becomes true. The allowed commit-
ment manipulations, together with the resulting commitment states, are captured by
means of a commitment machine [12]. In this work, we consider a simple commitment
machine, inspired by [12,13], and show how to lift it to a first-order setting, taking into
account that in our framework the precondition and the discharge condition are specified
through queries over the data of the involved agents. More elaborated commitment
machines, in terms of events and states, can be seamlessly incorporated.
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
91
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
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:
on ACCEPT REG from s to c if MyCust@s(c)
then CCDelivery (s, c, [Item@s(i) ^ Paid@s(i, c)], Owns@c(i))
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 Commitment Box
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 base-
level 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 Commitment Machine Formalization
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
92
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
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
93
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
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), ac-
tion 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.
94
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
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 ⌥S 0 is given in Figure 1.
5 Verification of DACMAS
To specify dynamic properties over DACMASs, we use a first-order variant of µ-calculus
[14,6]. µ-calculus is virtually the most powerful temporal logic used for model checking
of finite-state transition systems, and is able to express both linear time logics such as
LTL and PSL, and branching time logics such as CTL and CTL* [9]. In our variant of
µ-calculus, local properties are expressed as ECQ ` queries over the current state of the
DACMAS. We allow for a controlled form of first-order quantification across states,
inspired by [2], where the quantification ranges over data items across time only as long
ECQ
as such items persist in the active domain. Formally, we define the logic µLp ` as:
::= Q` | ¬ | 1 ^ 2 | 9x. LIVE (x)^ | LIVE(x)^h i | LIVE(x)^[ ] | Z | µZ.
where Q is a (possibly open) ECQ ` query, in which the only constants that may appear
are those in the initial state of the system, Z is a second order predicate variable (of arity
V ECQ
0), and LIVE(x1 , . . . , xn ) abbreviates i2{1,...,n} LIVE(xi ). For µLp ` , the following
assumption holds: in LIVE(x) ^ h i and LIVE(x) ^ [ ] , the variables x are exactly
the free variables of , once we substitute to each bounded predicate variable Z in its
bounding formula µZ. 0 . We adopt the usual abbreviations, including ⌫Z. for greatest
ECQ
fixpoints. Intuitively, the use of LIVE(·) in µLp ` ensures that data items are only
considered if they persist along the system evolution, while the evaluation of a formula
with data that are not present in the current state trivially leads to false or true. This is
in line with DACMASs, where the evolution of a commitment instance persists until
the commitment is discharged or canceled, and where an agent name is meaningful
only while it persists in the system: when an agent leaves the system and its name a is
canceled by inst, inst could reuse a in the future to identify another agent.
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).
95
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
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)) . New inst ABox
11: ⌃ := ⌃ [ { 0 } . Tentatively add a new state 0
12: for all x 2 {ag | Agent(ag) 2 Ai } do
0
13: .abox(x) := APPLY(S, , x, a, b, EV(e))
14: if for every x 2 {ag | Agent(ag) 2 Ai }, hT , 0 .abox(x)i is satisfiable then
15: ) := ) [ h , 0 i
16: else ⌃ := ⌃ \ { 0 } . Inconsistent execution step
17: function APPLY(S, , x, a, b, EV(e))
18: output: new ABox for x after reacting to EV(e) from a to b
19: if x 62 {inst, a, b} then return .abox(x)
20: Fetch all current behavioural rules for x
21: if x = a then . x is the sender agent
22: Fetch on-send and “self” on-receive rules and compute actions with actual params
23: if x = b then . x is the receiver agent
24: Fetch on-receive and “self” on-send rules and compute actions with actual param
25: if x = inst then . x is the institutional agent
26: Fetch matching/“any-event” on-exchange rules and compute actions with actual param
27: TOADD := ;, TODEL := ;
28: for all ↵(v) 2 ACT do . ACT = set of fetched actions
29: TOADDSK := ;
30: for all effect “[q + (p, x)] ^ Q (p, x) add A, del D” in the definition of ↵ do
31: for all ✓ 2 ANS` ([q + (v, x)] ^ Q (v, x), T , , x) do
32: TOADDSK := TOADDSK [ A✓[p/v]
33: TODEL := TODEL [ D✓[p/v]
34: pick a substitution ✓sk of the Skolem terms with data
35: TOADD := TOADD [ TOADDSK ✓sk
36: if x = inst then TOADD := TOADD [ {Agent(inst)}
37: return ( .abox(x) \ TODEL) [ TOADD
Fig. 1. Transition system construction
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.
ECQ
The semantics of µLp ` 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.
ECQ
Since µLp ` 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
96
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
(Q` )⌥v,V = { 2 ⌃ | T , , inst, v |= Q` }
(¬ )⌥v,V = ⌃ \ ( )⌥v,V
( 1 ^ 2 )⌥v,V = ( 1 )⌥v,V \ ( 2 )⌥v,V
(9x.LIVE(x) ^ )⌥v,V = { 2 ⌃ | 9d 2 ADOM( ). 2 ( )⌥v[x/d],V }
(LIVE(x) ^ h i )⌥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 = VT(Z)
(µZ. )⌥v,V = {E ✓ ⌃ | ( )⌥v,V [Z/E] ✓ E}
ECQ `
Fig. 2. Semantics of µLp
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 ( )⌥ .
ECQ
In this case, we write ⌥, s |= . Given DACMAS S, an initial state 0 and a µLp `
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
ECQ
customers are seller customers: MyGoldCust v MyCust. The µLp ` property
⌫Z.(8s, c, i.DeliveryC(s, c, active, i) ^ MyGoldCust@s(c)
! µY.(DeliveryC(s, c, sat, i)) _ (LIVE(s, c, i) ^ h iY )) ^ [ ]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 proposi-
tional) temporal properties of simple forms (e.g., reachability) turns out to be undecidable
[2,6]. This calls for identifying interesting classes of DACMASs for which verification is
decidable. Recently, the notion of state-bounded system has been proposed in the context
of both data-aware business processes [2] and MASs [3], as an interesting condition
that ensures decidability of verification for rich first-order temporal properties, while
reflecting naturally occurring working assumptions in real-world systems. Intuitively,
state-boundedness allows for encountering infinitely many different data during the
evolution of the system, provided that such data do not accumulate in a single state.
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:
ECQ `
Theorem 1 ([10]). Verifying state-bounded DACMASs against µLp properties is
decidable and reducible to finite-state model checking.
This means that state-bounded DACMASs can be verified, in principle, using standard
model checkers for propositional µ-calculus.
97
M. Montali et al. Specification and Verification of Commitment-Regulated Data-Aware MAS
6 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 [7], which
employs data-aware commitments to monitor a system execution and track the state of
commitment instances, but cannot be exploited for static analysis.
We consider extending our framework with the possibility of checking epistemic
properties, in the line of [3]. Notice that, if instead of relying on the µ-calculus, we
rely on CTL, we can relax the persistence requirement in the logic, as in [3]. We also
intend to study how to derive skeletons for the local agent specifications from a global,
choreographic commitment-based protocol.
References
1. Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The
Description Logic Handbook:. Cambridge University Press (2003)
2. Bagheri Hariri, B., Calvanese, D., De Giacomo, G., Deutsch, A., Montali, M.: Verification of
relational data-centric dynamic systems with external services. In: Proc. of PODS (2013)
3. Belardinelli, F., Lomuscio, A., Patrizi, F.: An abstraction technique for the verification of
artifact-centric systems. In: Proc. of KR (2012)
4. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: EQL-Lite: Effective
first-order query processing in description logics. In: Proc. of IJCAI (2007)
5. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Data complexity of
query answering in description logics. Artificial Intelligence 195, 335–360 (2013)
6. Calvanese, D., De Giacomo, G., Montali, M., Patrizi, F.: Verification and synthesis in descrip-
tion logic based dynamic systems. In: Proc. of RR (2013)
7. Chesani, F., Mello, P., Montali, M., Torroni, P.: Representing and monitoring social commit-
ments using the event calculus. AutonȦgent and Multi-Agent Syst. 27(1), 85–130 (2013)
8. Chopra, A.K., Singh, M.P.: Multiagent Systems: A Modern Approach to Distributed Artificial
Intelligence, chap. Agent Communication. MIT Press (2013)
9. Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press (1999)
10. Montali, M., Calvanese, D., De Giacomo, G.: Verification of data-aware commitment-based
multiagent systems. In: Proc. of AAMAS (2014), to appear
11. Poggi, A., Lembo, D., Calvanese, D., De Giacomo, G., Lenzerini, M., Rosati, R.: Linking
data to ontologies. J. on Data Semantics X, 133–173 (2008)
12. Singh, M.P.: Formalizing communication protocols for multiagent systems. In: Proc. of IJCAI
(2007)
13. Singh, M.P., Chopra, A.K., Desai, N.: Commitment-based service-oriented architecture. IEEE
Computer 42(11), 72–79 (2009)
14. Stirling, C.: Modal and Temporal Properties of Processes. Springer (2001)
98