Abstract

To investigate the interdependencies existing among deontic positions (like powers and obligations) and the ontology de ned by an institution, we have proposed to model institutions in terms of status functions imposed on agents and de ned as aggregates of deontic positions. In this paper we present a metamodel of institutional reality which introduces a set of concepts necessary to describe an institution and their intended meaning. A main advantage of our approach resides in the fact that institutions modelled in terms of such concepts can be veri ed by applying model checking techniques. In particular, in our framework it is possible to state and verify a set of properties stemming from our metamodel to enhance the development of sound institutions.

1 Introduction

Institutions and normative systems have been put forward as a means for regulating open interaction systems where agents' internal states cannot be accessed or agents are implemented by different parties. In such systems, norms play a fundamental role because they create positive expectations in the outcomes of interactions and make more predictable the behavior of other agents which are assumed to be autonomous [ 7, 15, 9, 10, 22, 26 ]. But while in [ 7 ] institutions de ne only norms, following [ 25 ] in [ 9 ] we have suggested that institutions also describe the ontology of the interaction context. For instance, the institution of the English Auction de nes the very concept of winning an auction, which also implies that the winner ought to follow a set of norms.

To investigate the interdependencies existing among deontic positions (like institutionalized powers [ 16 ] and obligations) and the ontology de ned by an institution, in [ 28 ] we have proposed to model institutions in terms of status functions imposed on agents and de ned as aggregates of deontic positions. Our main tenet is that institutional facts are such only because they provide agents with possibilities of actions which are attributed to them only thanks to the common agreement of a community of agents. In particular, we characterize institutional events in terms of what status functions they impose or revoke, which re ect the powers and obligations created or cancelled in the system.

Once we have formalized an institution, we have also to ensure that it is sound and allows agents to reach the desired states of affairs. Furthermore, as soon as institutions become complex, without the aid of an automated techniques it is prohibitive to foresee all possible evolutions and states in which a system may evolve. For this reason in [ 28 ] we have de ned FIEVeL (Functions for Institutionalized Environments Veri cation Language), a high level language to model institutions in terms of status functions and which is amenable to model checking [ 4 ], either by translating it into the input language of an existing tool (e.g. Promela, the input language of SPIN [ 14 ] as in [ 28 ]) or by implementing a new model checker.

In this paper we focus our attention on the de nition of a metamodel of institutions which de nes a set of legal and philosophical concepts that we perceive as essential to describe institutional reality. In our framework, institutions are described with FIEVeL, a modelling language which provides a concrete syntax to formalize institutions in terms of such concepts. For this reason we say that such set of concepts and their relations de ne a metamodel [ 17 ], since they constitute a model of our modelling language. On the other hand, the institutional metamodel represents the upper ontology of institutional reality, since it introduces concepts that are extended to describe the ontology of institutions. For instance, any domain-dependent status function extends the notion of status function, which is abstractly de ned as an aggregate of deontic position, by detailing what powers and obligations are associated to it.

The introduction of a metamodel allows us to de ne a library of domain-independent properties which not necessarily affect the functionality of an institution, but re ect the intended meaning of institutional concepts. For instance, if we empower agents participating to an auction to make bids but we always forbid them to do so, we obtain that it may be the case that agents make offers, but they will always violate the system of norms. Although such institution is functional (it allows agents to make bids), it is clearly irrational.

The remainder of this paper is structured as follows. Section 2 presents our metamodel, Section 3 discusses few domain-independent properties which can be veri ed by the tool presented in Section 4. In Section 5 we provide an example of veri cation activities that can be carried out in our framework by verifying the institution of property as it has been modelled and analyzed in [ 5 ], and nally in Section 6 we provide a comparison of our approach with related works. 2

The Institutional Metamodel

Many researches on institutions and normative systems [ 5, 9, 10, 22, 26 ] share several common or strongly related notions such as the concepts of role, norms, and institutionalized powers [ 16 ]. In this section we introduce our metamodel of institutions, that is, the set of concepts that we perceive as essential to specify an institution, the relationships existing between them, and their intended meaning. For the sake of brevity, we focus our attention on those aspects that are more relevant for the de nition of what we call domainindependent properties, which, as we will see in Section 3, re ect important aspects of the institutional metamodel.

We express the semantics of the metamodel in terms of an order many-sorted rst-order logic with temporal operators (OMSFOL). An order many-sorted rst-order temporal logic is de ned on a tuple S = h§; ·§; V; C; F; P; »i, which constitutes the signature of the logic, where § is a nite nonempty set of sort symbols; ·§ is a partial order on § determining a hierarchy of sorts; V is a nite set of (individual) variables, including a denumerable variables for every sort; C is a nite set of (individual) constants; F is an nite set of function symbols; P is an nite set of predicate symbols; » is a function that assigns a sort to every variable and every constant, and a signature (i.e. a sequence of sorts) to every function symbol and every predicate symbol; signatures of predicate symbols may be empty sequences, while signatures of function symbols have at least one component. Sets §, V, C, F, and P are mutually disjoint and we will write ¾1 ·§ ¾2 to say that ¾1 is a subsort of ¾2.

Given sorts §, the set T¾ of terms of sorts ¾ is the smallest set such that: ² v 2 T¾ if v 2 V and »(v) ·§ ¾ ² c 2 T¾ if c 2 C and »(c) ·§ ¾ ² f (t1; :::; tn) 2 T¾ if f 2 F, »(ti) ·§ [»(f )]i for 1 · i · n and [»(f )]0 ·§ ¾ where [»(q)]i refers to the i-th sort of the signature of a predicate or function symbol q.

The set T of terms is the union of the sets T¾ for all ¾ 2 § and the set A of atomic formulae is the smallest set such that: ² (t1 = t2) 2 A if there exists sort ¾ such that »(t1) ·§ ¾ and »(t2) ·§ ¾; ² P (t1; :::; tn) 2 A if P 2 P and »(ti) ·§ [»(P )]i for 1 · i · n

The set of formulae is de ned according to the following grammar:

' ::= ® j :' j ' ^ ' j X' j ['U'] j E' where ® is an atomic formula. Expressions true, false, (' _ Ã), (Ã ! '), (' $ Ã), 9x', 9·nx', 9¸nx', F', G', A', and t1 = t2 are introduced as abbreviations as usual.

The semantics of an order many-sorted rst-order temporal logic is de ned as usual [ 20 ] by providing a set of states, a total transition relation among states, a set of domains (one for each sort), and an interpretation function I which maps, for each state, constants to individuals, and function and predicate symbols to functions and relations on domains.

Despite OMSFOL models and formulae can be translated into classical rst-order logic with temporal operators (FOL) or, under certain conditions, into temporal propositional logic like CTL¤ [ 4 ] (see Section eventX 1 * Convention

1..* eventY

1 Event Action 1 1 1

Institutional entity 0..1

* * Status-function 1 1

State * 4), we adopt OMSFOL for two main reasons: i) it represents an abbreviated form for long and complex FOL or CTL¤ formulae and ii) OMSFOL guarantees syntactic type checking of formulae. Moreover, institutions describe rules that typically are independent of the number of agents, objects, etc. involved in the interaction, which can be naturally expressed by allowing quanti cation over sorts.

In the remainder of this section we will introduce the semantics of the institutional metamodel by explaining what sorts, functions, and predicates are induced by each institutional concept. For predicates and functions we also provide their signature ». Figure 1 depicts some of the main sorts used in our approach (e.g. status function, obligation, event) and their relations, which are typically represented by introducing predicates or functions. For instance, relation actor is re ected in our logic by function actor, which refers to the actor of the current action (see below). Finally, we report a set of axioms which characterize institutional reality by imposing a set of restrictions A on the admissible valuations of institutional models [ 1 ]. In the sequel we will represent such restrictions in terms of OMSFOL formulae (corresponding to LTL formulae), while in Section 3 we will introduce a set of properties that can be translated into CTL formulae.

Before starting the analysis of the concepts which constitute our metamodel, it is worth to mention few basic sorts like integers, agents (¾AID), and objects, which are introduced to describe types of domaindependent attributes associated to status functions and events. Designers can also de ne context dependent basic sorts.

As shown in Figure 1, our metamodel is based on the notion of agent status function, that is, a status imposed on an agent and recognized as existing by a set of agents. Typical examples of status functions are not only the concept of auctioneer, participant, or winner of an auction, but also being the owner of a good, being the husband or the wife of somebody. The concept of status function shares several features with the concept of role as it has been discussed in the literature (refer to [ 2 ] for an overview). Despite that, we prefer to use the term “status function” for three reasons: (i) the term role has been used with different meanings and it has been characterized in terms of very different concepts such as mental states, tasks, duties, etc; (ii) the term status function better represents the fact that we are concerned with status whose existence depends on those agents that recognize them as existing and which are assigned to agents to create new institutional powers or to regulate their use; (iii) the concept of status function is broader than the concept of role as used, for example, in [ 2 ]. In fact, it seems to be dif cult to describe in terms of a “preexisting organization” being the owner of a good or being under age, while it is quite natural to regard them as status functions imposed by a group of agents.

Status functions induce sort ¾SF , which represents the supertype of all status functions described by an institution. ¾SF de nes function subject which refers to the agent the status function has been assigned to (»(subject) = h¾AID; ¾SF i) and predicate assigned (»(assigned) = h¾SF i) which evaluates to true

[start] Unfired

Activated [violation or fulfillment] [revoked]

Inactive when a status function is currently assigned. Status functions are imposed (or revoked) when an institutional event happens (see below), otherwise they continue to be assigned (unassigned).

Status functions are possibly empty aggregates of deontic positions that can be expressed in terms of two main concepts, institutionalized power [ 16 ] 1 and obligations. Obligations induce sort ¾o whose individuals reify norms of institutions in such a way that it is possible to classify institutional states with respect to agents' compliance with norms, or adopting the terminology used in [ 19, 23, 26 ], it is possible to classify states as red (violating at least a norm) or green states (all norms are respected). Obligations can be also used to express prohibitions by specifying suitable violation expression, while we do not de ne a speci c construct to explicitly represent the fact that an agent is permitted to perform an action as in [ 5, 10, 22 ]. Instead, we consider that every action, if it is not prohibited, is also permitted.

Given sort ¾state, which introduces constants unf ired, activated, and inactive, obligation sort ¾o is characterized by function state (»(state) = h¾state; ¾oi) and by a set of predicate (start, ful llment, and violation of signature »(violation) = h¾oi) which are used to specify conditional obligations and when a norm should be considered ful lled or violated according to the state machine represented in Figure 2. An obligation is created because a status function is imposed, changes its state when its conditions are satis ed, and eventually reaches a nal state (inactive) either because it is ful lled (violated) or because it is associated to a revoked status function. Figure 2 graphically describes a set of axioms which regulate the temporal evolution of an obligation individual: for instance, the following axiom states that if an obligation has been activated and in the following state violation or f ulf illment are evaluated to true, then the next state is inactive:

G8o8sf (state(o) = activated ^ X(assigned(sf ) ^ of StatusF unction(o) = sf ^(violation(o) _ f ulf illment(o))) ! X(state(o) = inactive)) (1)

To record whether an obligation has been violated, we introduce predicate violated of signature »(violated) = h¾oi. Predicate violated is evaluated to true in a given state if an obligation was activated and the violation expression is evaluated to true:

G8ob(state(ob) = activated ^ Xviolation(ob) ! Xviolated(ob))

Given that at the moment our metamodel does not provide any support for the de nition of recovery policies or sanctions [ 19 ], we assume that once an obligation has been violated, predicate violated is always evaluated to true. Formally:

G8ob(violated(ob) ! Xviolated(ob))

1In [ 9, 28 ] we used to name institutionalized power “authorization”, but to enhance a comparison with other works we adopt the more widely used term “power” [ 16, 5, 22, 26 ]. (2) (3) The de nition of axioms that regulate the temporal evolution of an obligation and when a norm is violated allows us to automatically classify states as red or green with respect to every norm, while in [ 23 ] the designer is required to manually specify which states are red or green.

According to Figure 1, obligations are associated to status functions and not directly to agents. In general, an agent is responsible for the state of affairs described by a ful llment or violation expression because it has been assigned a speci c status function. For this reason we introduce function liable(ob), which is de ned as follows:

liable(ob) $ subject(of StatusF unction(ob)) where given an obligation, function of StatusF unction (»(of StatusF unction) = h¾SF ; ¾oi) returns the associated status function.

The metamodel de nes two kinds of events, base-level events (¾BE ) and institutional events (¾ie), which are characterized by an ontological difference: while the former exist because they re ect changes that are produced in the physical world or that are relative to lower level institutions, like time events and exchangemessage events, the latter exist because they are recognized as existing by a community of agents and cannot be directly produced by the environment or by an agent [ 25, 9 ]. Despite that, we de ne both types of events as subsort of sort event (¾ev) which de nes predicate happens (»(happens) = h¾evi) and which is evaluated to true when event ev has caused the last transition. Analogously, sort ¾ia represents common features of base-level actions and of institutional actions, e.g. “actions are always performed by an actor” (»(actor) = hAID; ¾acti). For convenience we de ne predicate done as an abbreviation to say that “agent x has performed action act”:

done(act; x) $ (happens(act) ^ actor(act) = x) It is important to observe that in the literature only agent actions have been considered relevant to describe institutions [ 5, 9, 22, 26 ], and the attention has been focused on a single action type, namely the act of exchanging a message [ 7, 9 ]. In contrast, we are also interested in modelling the institutional effects of events that are not generated by agents, like for instance time events, which not only are important for the management of obligations, but also may count as institutional events. For instance, in most cultures the 18th birthday imposes new status functions on a person.

We regard time aspects in two distinct ways: (i) as in classical temporal logic, to de ne qualitative aspects (it is always the case that a revoked status function is associated only to inactive obligations), and (ii) as in RTTL [ 21 ] to express quantitative aspects (e.g. an obligation will be violated in 2 time instants since now). To de ne quantitative aspects, we consider the perspective of a single centralized component which makes the institutional (normative) state evolve: therefore, we consider the existence of a unique timer that generates time events such that two consecutive time events ti and ti+1 may be separated by a sequence (possible empty) of other base-level events, which are assumed to occur at time ti. Hence the institutional state may change due to the occurrence of other events even if the timer has not generated new ticks of the clock. Although multiagent systems are distributed in nature, which makes problematic the assumption of unique notion of time or the adoption of an architecture where a single centralized manager control the evolution of the institutional state, to cope with the state explosion problem [ 4 ] we decide to introduce such simpli cation. It is worth noticing that centralized managers of the institutional states have been also proposed in several prototypes of institutions [ 6, 11 ] and normative systems [ 8 ].

Institutional events are de ned by an institution and represent changes in the institutional environment. Essentially, their occurrence means that new status functions have been imposed on agents or existing status functions have been revoked. Sort ¾ie de nes two predicates, prec and ef f which express the preconditions and effects of an institutional event. More precisely, for every institutional event prec (»(prec) = h¾iei) describes a condition that must be satis ed before institutional event ie occurs, while ef f describes a condition satis ed after ie has occurred. But how agents recognize when an institutional event happens?

Following [ 25 ], we regard the occurrence of an institutional event by subordinating it the occurrence of another event conventionally associated to it. We represent the existence of a convention2 among two events by introducing predicate conv which associates the occurrence of an event to the occurrence of an institutional event (»(conv) = h¾ev; ¾iei). We are now in position to de ne under what conditions 2As studied in [ 16, 12 ] conventions are related to the counts-as relation, which tipically is de ned relative to a certain institution. The extension of our approach to the treatment of multiple institutions is an interesting topic of research that we intend to tackle in our future works. For the purpose of this paper we limit our attention to a single institution, and therefore we omit the institution in which such relation holds. an institutional event ie which is not also an institutional action may happen. An institutional event ie conventionally bounded to event ev happens when:

G8ie9ev(prec(ie) ^ conv(ev; ie) ^ Xhappens(ev) ! Xhappens(ie))

(4)

Instead, in the case of institutional actions a further condition must be satis ed, namely, the actor must be empowered to perform the institutional action [ 16 ]. According to Figure 1 status functions are constituted by a set of powers, which are represented through predicate empowered (»(empowered) = h¾SF ; ¾iai) which means that status function sf is empowered to perform institutional actions of type ia. An institutional action happens when:

G8ia8aid9act(prec(ia) ^ 9sf (subject(sf ) = aid ^ empowered(sf; ia) ^ assigned(sf )) ^X(happens(act) ^ actor(act) = aid ^ conv(act; ia)) ! X(happens(ia)) (5)

Assuming that institutions are asynchronous systems and according to axiom (5), which ensures that if the agent that brings about action act is empowered to perform ia, then action ia is successfully performed, we require that given two action symbols act1 and act2, if they are conventionally bounded and if they happen, the actor must be the same. Formally:

G8act18act2(conv(act1; act2) ^ happens(act1) ^ happens(act2) !

actor(act1) = actor(act2)) (6)

Our treatment of the conventional generation of events extends the treatment presented in [ 9 ], since we do not take as our unique primitive to specify conventions the act of exchanging a message. Instead, any event can be used to de ne a new convention. In particular, our metamodel allows institutional events to be conventionally associated to other institutional events. For instance, the institutional act of transfer the possession may be conventionally bounded to the act of transfer the property. 3

Domain-Independent Properties

Once an institution has been de ned in terms of the concepts described by our metamodel and the corresponding model has been generated by a model checker, there are two kinds of properties that a designer may want to verify, domain-independent properties and domain-dependent properties [ 28 ]. Domain-dependent properties stem from peculiar features of the speci ed model and regard the functionality of an institution: for instance, we may want to ensure that an auctioneer cannot win an auction. Instead, domain-independent properties are de ned to guarantee the rationality of an institution with respect to the intended semantics of the concepts provided by our metamodel. Notice that, in contrast with axioms discussed in Section2 which characterize the semantics of institutional concepts and cannot be falsi ed, domain-independent properties are veri ed by a model checker and may be unsati ed by institutions. In this case we say that an institution is irrational with respect to such properties. For instance, a rational institution should be characterized by the fact that every institutional event must eventually happen in at least an execution:

8ie EFhappens(ie)

where ie is a variable of type ¾ie. If this property does not hold, then it means that either the preconditions of an institutional event are never met or that the designer has not de ned the necessary powers or conventions for its performance.

Analogously, given a convention which relates events of type x and y, it should be the case that there exists a path where eventually both of them contemporary happen:

8evx8evy(conv(evx; evy) ! EF(happens(evx) ^ happens(evy)))

(1) (2)

If this property does not hold, it means that agents cannot exploit the convention binding events of type x to events of type y, for instance because preconditions of such events are never contemporary satis ed or, in the case of actions, because status functions empowered to execute them are never assigned to an agent.

Let us now move our attention to a set of properties that should characterize norms. Norms are introduced in open multiagent systems to constrain possible agents' behaviour, and therefore it must be the case that each norm can be eventually activated:

8obEF(state(ob) = activated) If we assume that agents are autonomous, it should be possible for an agent both to violate and ful ll its obligations (and prohibitions), which means that norms regulate aspects of (social) reality which are contingent. It would be irrational to de ne an obligation characterized by a violation expression that makes it impossible to violate it:

8obAF(state(ob) = activated ! Estate(ob) = activatedUviolated(ob)) Similarly, we can specify that all obligations may be eventually ful lled. Moreover, it should be the case that once a norm is activated, it ought to eventually reach a nal state (inactive), which guarantees that the whole life-cycle of a norm is limited and regulated only by the institution that de nes it: AG8ob(state(ob) = activated ! A[state(ob) = activatedUstate(ob) = inactive]) (5) Notice that any obligation which is not characterized by a deadline (not necessarily a time expression) violates property (5). For instance, if an agent ought to maintain inde nitely a state, as a consequence the whole institution would not satisfy property (5).

Obligations are de ned to indicate whether a given behaviour is accepted by an institutions and typically “involve sacri ce and renunciation” [ 13 ]. For this reason, under the hypothesis that internal mental states are not accessible, it seems natural to assume that if an agent is obliged to a certain state of affairs it should not be provided with the possibility of revoking its own obligations. Otherwise, it could avoid complying with its duties without incurring in any sanction or blame. We formalize this fact as follows: AG8ob(state(ob) = activated ! :EX(state(ob) = inactive ^ :violation(ob) (3) (4) ^:f ulf illment(ob) ^ 9act done(act; liable(ob)))) (6) The fact that an institution does not satisfy a domain-independent property does not necessarily mean that its rules prevent any successful interaction. It may be the case that all domain-dependent properties are satis ed while there are domain-independent properties that are violated. In any case, it is important that the designer becomes aware of this fact, and consider how to modify the institution. For instance, if property (1) does not hold, we can eliminate the institutional event or change powers and preconditions associated to it, otherwise its de nition would be useless and the institution would be irrational. 4

A Symbolic Model Checker for Verifying Institutions

Figure 1 represents not only the metamodel of the institutional reality, but also it constitutes the abstract syntax of FIEVeL (Functions for Institutionalized Environments Veri cation Language) [ 28, 29 ], a language that has been de ned to model institutions in terms of the concepts introduced by our metamodel and to verify them by applying model-checking techniques [ 4 ]. As exempli ed in Figure 3 and according to the institutional metamodel, an institution described in FIEVeL de nes a set of status functions, characterized by powers and obligations, a set of institutional events and conventions for their performance. The semantics of FIEVeL constructs is given by describing how each expression affects the signature or the interpretation function of an OMSFOL logic characterized also by symbols introduced by our metamodel (see [29] for more details about FIEVeL).

The adoption of an order many-sorted rst-order logic to describe the semantics of FIEVeL, its metamodel, and properties of institutions, naturally rises the question about how to verify OMSFOL models by applying model-checking techniques, which usually are applied to propositional models [ 4 ]. In the remainder of this section we will de ne an encoding E of OMSFOL models into propositional models and a translation ¿ of OMSFOL formulae into CTL¤ formulae which is exploited by our tool to verify institutions described in FIEVeL.

APf(x1;:::;xn)); px1;:::;xn ); ² each predicate P is encoded as the proposition induced by the current valuation (E[P (x1; :::; xn)] = A propositional model is de ned as a tuple Mc = where AdP is a set of atomic propositions, and Vb is a valuation function which, given a state sb 2 Sb and a proposition p 2 AdP , returns a value in f0; 1g. Let be ND¾ the cardinality of domain D¾ associated to sort ¾: the set of atomic proposition AdP is determined by introducing a set of propositions APfx1;::;xn 2 AP of cardinality log2(N[»(f)]0 ) for every function f and for every possible valuation, and a proposition px1;:::;xn for every predicate P and for every valuation. Moreover, for every domain we associate to each individual el a natural number nel such that 0 · nel < ND¾ . The encoding E of an OMSFOL model into a propositional model Mc is de ned as follows: ² each constant symbol c is encoded as a sequence of truth values corresponding to the binary representation of the number associated to the individual referenced by constant c (E[c] = binary(I(c; s))); ² each function f is encoded as the set of propositions induced by the current valuation (E[f (x1; :::; xn)] = The valuation function Vb is such that given an interpretation function I and a state s, propositions APfx1;::;xn are evaluated as the encoding of the element referred by f (x1; :::; xn) and proposition px1;:::;xn evaluates as the truth value corresponding to predicate P in state s.

Assuming that the language is rich, that is, there exists a constant symbol for each individual of every domain, and also assuming for simplicity that only variables and constants can appear as arguments of functions and predicates, the translation of a OMSFOL formula ' with temporal operators is de ned as follows: ² ¿ [t1 = t2] = Vi<N(»(t1)) :(E(t1)i © E(t2)i) where E(t)i refers to the i-th proposition (or equivai=0 lently the i-th truth value) corresponding to the encoding of term t; ² ¿ [P (x1; :::; xn)] = E(P (x1; :::; xn)) ² ¿ [8x'] = Vc2C»(x) ¿ ['[c=x]] where c ranges over constants of sort »(x) and '[c=x] is the result of replacing every free occurrence of x in ' with an occurrence of c; ² ¿ [:'] = :¿ ['] ² ¿ [' ^ '] = ¿ ['] ^ ¿ ['] ² ¿ [X'] = X¿ ['] ² ¿ ['U'] = ¿ [']U¿ ['] ² ¿ [E'] = E¿ [']

It can be demonstrated that:

Theorem 1 Given a model M, characterized by a OMSFOL signature and nite domains, and an OMSFOL formula ', M j= ' if and only if E[M] j= ¿ ['].

To verify domain-dependent and domain-independent properties we have implemented a symbolic model checker based on the CUDD library [ 27 ]. Our tool takes as its input an institution modelled with FIEVeL, a list of individuals composing each basic domain, and a set of status functions which are assumed to be imposed at the rst state. Domain-dependent properties are speci ed in a separate le, while domainindependent properties are selected by interacting with the tool. Starting from these inputs, the tool applies translation ¿ and encoding E to construct the corresponding Kripke structure, whose states and transition relation are symbolically represented as OBDDs [ 3 ]. To verify properties whose translation corresponds to CTL formulae, that is, formulae where path quanti ers (A and E) are immediately followed by temporal operators (X, F, and G), the tool applies symbolic algorithms as described in [ 4 ]. basic-types: priceD subtype-of INT;;

... base-events : message refuse(buyer:AID,good:OID,value:priceD);

... institution purchase f ...

status-function proposed(proposer:AID,good:OID,value:priceD) f key proposer,good powers ...

refuseRequest d <- TRUE; ... deontic: p1 obligation(TRUE,

done(transferPossession,subject)),activation>1); ... g// proposed

... institutional-events: ... institutional-action refuseRequest(buyer:AID,g:OID,price:priceD) pre exists p in proposed (((p.subject=actor and

and (p.proposer=buyer and p.value=price))); eff revoke proposed (subject=actor,proposer=buyer,good=g, value=price); ... conventions: exch-Msg(refuse) p [TRUE] =c=> refuseRequest [buyer =c=> buyer good =c=> g value =c=> price ]; ... g// institution

Modelling and Verifying the Institution of Property

In this section we report the results obtained during the veri cation process of the institution of property as it has been de ned in [ 5 ]. During the formalization of such institution (see Figure 3) we have slightly modi ed certain features of the original speci cation to adapt them to our concepts. Despite these changes, results obtained with our formalization can be extended to the institutions described in [ 5 ]. For the sake of brevity we will focus on those aspects that our analysis has shown to be problematic and which we deem highlight the importance of the de nition of a metamodel of institutions.

In [ 5 ] the institution of property de nes an institutional action, transfer ownership, which is “empowered if the initiator of the transfer is the owner of the object being transferred”. Furthermore a set of institutional actions are introduced, like requestGoods which allows a customer to request a good, sendPayment which can be performed by a customer to send a payment, refuseRequest which allows the merchant to refuse a request, and nally sendGoods which empowers the merchant to send a good. Notice that in [ 5 ] it is not required that institutional actions happen because agents have performed basic actions conventionally bounded to them, which obliged us to introduce a set of base-level events and conventions to enable agents to perform institutional actions described above.

According to [ 5 ] “sending a request for goods creates an obligation on the merchant to have sent the goods before the interaction ends” but “sending the refusal cancels the merchant's obligation to send goods”. Therefore, the merchant can cancel an obligation of itself which intuitively violates property (6) discussed in the previous section.

Let us now consider how agents can execute action transfer good, which is de ned in such a way that it can be successfully performed at time t if and only if either the merchant sends the good at time t and the customer has payed at time t1 < t, or the customer pays at time t and the merchant has sent the good at time t1 < t. Given such description it seems natural to introduce two conventions: conv1 which states that the performance of the institutional act sendGood counts as transf er property if the customer has payed, and conv2 such that sendP ayment counts as tranf er property if the merchant has sent the good. Such conventions re ect the fact that in [ 5 ] the execution of sending a good (or similarly sending a payment) implies the transfer of property. At this point it is important to notice that if transf er property, sendGoods, and sendP ayment are institutional actions, then they are successfully executed only if the actor is empowered (see axiom (5) which is similar to an inference rule in [ 5 ]). The concept of power adopted by [ 5 ] is similar to the one presented here, since it is de ned as “the capability of an agent to bring about a change” in the institutional state. But, the act of paying is performed by the customer, while the transfer of property is empowered to the merchant, and they cannot be the same agent in a given transaction. These considerations rise a problem of agency of the institutional actions: how can a payment of agent a count as an action performed by agent b? It would be possible if agent b had delegated its power to agent a, but the authors do not introduce delegation of powers in their formalization. Therefore, we should expect that property (2) does not hold, since according to axiom (6) the convention among the payment and the transfer of property can never produce the successful performance of both acts.

Figure 4 shows the veri cation results generated by our tool when it has been asked to verify properties described in Section 3 and where we can observe that properties (2) and (6) are violated. The generation of the transition system corresponding to the institution of property and the veri cation of all domainindependent properties required 0.25 seconds on a laptop with installed Linux and equipped with a pentium 1.66 GHz and 1 GB of RAM.

When a domain-independent property is not satis ed by an institution, we can consider what speci c features of the metamodel it re ects to get some clue about how to modify an institution in order to satisfy it. For instance, we know that all institutional events may eventually happen as ensured by property (1). Therefore, as we have also noted in the previous informal analysis, a way to satisfy property (2) is to change the institutional power of agents. In particular, here we propose to not classify the exchange of the property as an action but as an institutional event. This solution immediately solves the agency problem and eliminates the power attributed to the owner of a good.

To satisfy property (6), that is, agents cannot cancel their own obligations, we propose to model the act of requesting a good in such a way that it does not create an obligation for the merchant to send the good, but it creates an obligation to agree or reject the request of the customer. In both cases, an answer of the merchant satis es its obligation; in particular, a positive answer imposes on the involved agents a set of status functions which represent the obligation to transfer the possession (or perform the payment) and the powers to do so. Notice that such a formalization better represents the fact that a directive act (like a request) does not create obligations to the performance of the requested act [ 24 ], while a commissive (like the agree communicative act) commits the agent to the performance of the agreed action (see also [ 9 ]). 6

Discussion and Conclusions

In this paper we have presented a metamodel for verifying institutional reality based on the notion of status function, which is regarded as a (possibly empty) aggregate of deontic positions (powers, obligation, etc.). This approach provides for a uni ed view of institutional facts and deontic positions, which have been usually analyzed separately [ 5, 9, 22 ], and is motivated by the fact that institutional reality is such only because it is constituted by deontic positions attributed to agents. We have introduced the semantics of our institutional metamodel in terms of an order many-sorted rst-order logic, which allows us to formalize both axioms regulating the metamodel and a set of domain-independent properties which re ect the intended meaning of concepts de ned by our metamodel. Finally, we have tested our approach by verifying the institution presented in [ 5 ] with respect to a set of domain-independent properties and shown that the veri cation of such properties enhances the formalization of sound institutions.

In the literature there are several attempts to model and verify institutions and normative systems. In [ 9 ] the authors rely on an intuitive semantics to model institutional reality in terms of entities, roles, and norms. Instead, the approach presented in this paper provides a formal semantics of institutional concepts such that we can apply model checking techniques to verify institutions.

In [ 22 ] normative systems are described by using the Event Calculus [ 18 ]. The absence of an institutional metamodel, which for instance provides an axiom to state that every institutional action must be authorized in order to be successfully executed, obliges the authors of [ 22 ] to specify this fact for every single action and for every role. Therefore, the de nition of a metamodel provides a signi cant advantage, especially when many status functions (or roles, using the terminology of [ 22 ]) are authorized to perform the same institutional action. Furthermore, the de nition of an encoding of institutions described in FIEVeL into propositional models allows us to verify our systems, while in [ 22 ] the authors must rely on “systematic runs”.

In [ 15 ] the authors propose a framework to model check electronic institutions, a formalism proposed in [ 7 ] and which describes institutions as nite automata. Starting from this point, in [ 15 ] the authors limit their attention on the veri cation of properties of nite automata (e.g. “it is always possible to reach a nal state”). It is important to notice that in [ 15 ] arcs of electronic institutions (which in principle represent permitted acts [ 7 ]) are interpreted as obligatory moves of agents, which may lead the model checker to answer that a given property holds in an institution while it is not the case and vice versa.

We plan to extend our metamodel, and consequently our modelling language, to model different interdependent institutions like in [ 30 ], which raises, among others, two interesting research problems: rst, how to model interdependencies among different contexts, and second, how to design an institution which somehow depends on another institution.

Acknowledgments This research has been supported by Swiss National Science Foundation project 200020109525, “Arti cial Institutions: speci cation and veri cation of open distributed interaction frameworks”. The author would like to thank his Ph.D. advisor, Marco Colombetti, for fruitful discussions and criticisms about the contents presented in this paper and Alessio Lomuscio for his advices regarding the implementation of the tool discussed in the paper.

References

[1] P. Blackburn , M. de Rijke, and Y. Venema. Modal Logic . Cambridge University Press, 2001 .

[2] G. Boella and L. van der Torre. The ontological properties of social roles: De nitional dependence, powers and roles playing roles . In Proceedings of the ICAIL05 Workshop on Legal Ontologies and Arti cial Intelligence Techniques , 2005 .

[3] R. E. Bryant . Graph-based algorithms for boolean function manipulation . IEEE Trans. Comput. , 35 ( 8 ): 677 – 691 , 1986 .

[4] E. M. Clarke , O. Grumberg , and D. Peled . Model Checking. MIT Press, 1999 .

[5] O. Cliffe , M. D. Vos , and J. Padget . Specifying and Analysing Agent-based Social Institutions using Answer Set Programming . In Coordination, Organization, Institutions and Norms in Agent Systems I, number 3913 in LNCS , pages 99 – 113 , 2005 .

[6] M. Esteva , J. A. Rodr ´guez- Aguilar , B. Rosell , and J. L. Arcos. AMELI: An Agent-based Middleware for Electronic Institutions . In N. R. Jennings, C. Sierra , L. Sonenberg , and M. Tambe, editors, Proceedings of the 3rd International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2004 ), pages 236 – 243 . ACM Press, 2004 .

[7] M. Esteva , J. A. Rodr ´guez- Aguilar , C. Sierra , P. Garcia , and J. L. Arcos . On the Formal Speci - cation of Electronic Institutions . In Agent Mediated Electronic Commerce, The European AgentLink Perspective , volume 1991 of LNAI , pages 126 – 147 , 2001 .

[8] A. D. H. Farrell , M. J. Sergot , M. Salle´, and C. Bartolini . Using the Event Calculus for Tracking the Normative State of Contracts . Journal of Cooperative Information Systems , 14 ( 2-3 ): 99 – 129 , 2005 .

[9] N. Fornara , F. Vigano , and M. Colombetti . Agent Communication and Institutional Reality . In Agent Communication , volume 3396 of LNAI , pages 1 – 17 , 2005 .

[10] A. Garcia-Camino , P. Noriega , and J. A. Rodr ´guez-Aguilar. Implementing norms in electronic institutions . In Proceedings of the 4th International Joint Conference on Autonomous agents and Multi-Agent Systems , pages 667 – 673 , 2005 .

[11] A. Garc ´a- Camino , J. A. Rodr ´guez- Aguilar , C. Sierra , and W. W. Vasconcelos . A distributed architecture for norm-aware agent societies . In Declarative Agent Languages and Technologies III (DALT 2005 , volume 3904 of LNCS , pages 89 – 105 . Springer, 2005 .

[12] D. Grossi , J.-J. C. Meyer, and F. Dignum . Counts-as: Classi cation or constitution? an answer using modal logic . In Proceedings of the 8th International Workshop on Deontic Logic in Computer Science , volume 4048 of LNCS , pages 115 – 130 , 2006 .

[13] H. L. A. Hart . The Concept of Law . Oxford University Press, 1961 .

[14] G. Holzmann. The SPIN Model Checker : Primer and Reference Manual . Addison Wesley , 2003 .

[15] M.-P. Huget , M. Esteva , S. Phelps , C. Sierra , and M. Wooldridge . Model Checking Electronic Institutions . In Proceedings of the ECAI Workshop on Model Checking and Arti cial Intelligence (MoChArt I) , 2002 .

[16] A. Jones and M. J. Sergot . A formal characterisation of institutionalised power . Journal of the IGPL , 4 ( 3 ): 429 – 445 , 1996 .

[17] A. Kleppe , J. Warmer , and W. Bast . MDA Explained: The Model Driven Architecture–Practice and Promise . Addison-Wesley Professional , Reading, Massachusetts, USA, 1 edition , 2003 .

[18] R. A. Kowalski and M. J. Sergot . A Logic-based Calculus of Events. New Generation Computing , 4 : 67 – 95 , 1986 .

[19] A. Lomuscio and M. Sergot . A formulation of violation, error recovery, and enforcement in the bit transmission problem . Journal of Applied Logic (Selected articles from DEON02 - London) , 1 ( 2 ): 93 – 116 , 2002 .

[20] K. Meinke and J. V . Tucker, editors. Many-sorted logic and its applications . John Wiley & Sons, Inc., 1993 .

[21] J. S. Ostroff . Deciding properties of timed transition models . IEEE Transactions on Parallel Distributed Systems , 1 ( 2 ): 170 – 183 , 1990 .

[22] J. Pitt , L. Kamara , M. Sergot , and A. Artikis . Formalization of a voting protocol for virtual organizations . In Proceedings of the 4th International Joint Conference on Autonomous agents and Multi-Agent Systems (AAMAS 2005 ), pages 373 – 380 , 2005 .

[23] F. Raimondi and A. Lomuscio . Automatic veri cation of deontic interpreted systems by model checking via OBDDs . Journal of Applied Logic . To appear.

[24] J. R. Searle . Speech Acts: An Essay in the Philosophy of Language . Cambridge University Press, 1969 .

[25] J. R. Searle . The construction of social reality . Free Press, 1995 .

[26] M. J. Sergot and R. Craven . The Deontic Component of Action Language nC+ . In Proceedings of the 8th International Workshop on Deontic Logic in Computer Science , volume 4048 of LNCS , pages 222 – 237 , 2006 .

[27] F. Somenzi . Cudd: Cu decision diagram package . http://vlsi.colorado.edu/ fabio/CUDD/.

[28] F. Vigano . A Framework for Model Checking Institutions . In Proceedings of the ECAI Workshop on Model checking and Arti cial Intelligence (MoChArt IV) , 2006 .

[30] F. Vigano , N. Fornara , and M. Colombetti . An Event Driven Approach to Norms in Arti cial Institutions . In Coordination, Organization, Institutions and Norms in Multi-Agent Systems , volume 3913 of LNAI , pages 142 – 154 . Springer, 2006 .