In this paper we investigate the specification and verification of information systems with an organizational structure. Such systems are modelled as a normative multiagent system. To this end we use KBDIO_CTL, an extension of BDI_CTL in which obligations and permissions are represented by directed modal operators. We illustrate how the logic can be used by introducing and discussing various properties of normative systems and individual agents which can be represented in the logic. In particular we discuss the enforcement of norms.

Keywords: deon04

We present an algorithm and its implementation for the verification of correct behaviour and epistemic states in multiagent systems. The verification is performed via model checking techniques based on OBDD's. We test our implementation by means of a communication example: the bit transmission problem with faults.

Keywords: deon04

In an organizational context the norms that apply to an agent depend on the roles he holds in the organization. The deontic characterization of structural roles is defined when the organization is created. But an organization is not a static entity. Among the dynamic phenomena that occur in an organization there are interactions between agents consisting in a transference of obligations or permissions from an agent to another. These kind of interactions are called delegation. In this paper we analyze different ways in which delegation occurs in an organizational context. We argue that the concept of agent in a role is relevant to understand delegation. A deontic and action modal logic is used to specify this concept.

Keywords: deon04

We use non-Kripkean quasi-matrix semantics for the formalization of the systems S_3d, S_3dp and S_3dq of deontic logic. The system S_3d is weaker than the standard logic . The semantics for S_3dp represents combination of quasi-matrix semantics and the semantics of truth value gluts, which allows S_3dp to avoid deontic explosion O A /\O ¬B O B. The system S_3dq rejects both deontic explosion and the formula O A /\O ¬A O A /\O ¬A, thus it allows to consider deontic dilemmas without classical contradictions. The systems S_5d, S_5dp and S_5dq in which the two types of deontic operators are used, namely, strong and weak obligation (permission), can be built as an extension of the correspondent systems S_3d, S_3dp and S_3dq .

Keywords: deon04

In this paper I propose a simple modification of standard deontic logic that will enable the system to accommodate deontic dilemmas without inconsistency and without deontic explosion, while at the same time preserving the range of genuinely valid inferences. The proposal applies both to monadic deontic logic and to a dyadic logic of conditional obligation. In the Appendix these systems are proved to be sound and complete with respect to an appropriate semantics and also to be decidable.

Keywords: deon04

In this paper, we combine deontic logic with Alternating-time Temporal Logic (ATL) into a framework that makes it possible to model and reason about obligations and abilities of agents. The way both frameworks are combined is technically straightforward: we add deontic accessibility relations to ATL models (concurrent game structures), and deontic operators to the language of ATL (an additional operator is proposed for unconditionally permitted properties, similar to the all I know operator from epistemic logic). Our presentation is rather informal: we focus on examples of how obligations (interpreted as requirements) can be confronted with ways of satisfying them by actors of the game. Though some formal results are presented, the paper should not be regarded as a definite statement on how logics of obligation and strategic ability must be combined; instead, it is intended for stimulating discussion about such kinds of reasoning, and the models that can underpin it.

Keywords: deon04

Often a set of imperatives or norms seems satisfiable from the outset, but conflicts arise when ways to fulfill all are ruled out by unfortunate circumstances. Semantic methods to handle normative conflicts were devised by B. van Fraassen and J. F. Horty, but these are not sensitive to circumstances. The present paper extends these resolution mechanisms to circumstantial inputs, defines according dyadic deontic operators, and provides a sound and (weakly) complete axiomatic system for such a deontic semantics.

Keywords: deon04

This paper is a preliminary investigation into the application of the formal-logical theory of normative positions to the characterisation of normative-informational positions, pertaining to rules that are meant to regulate the supply of information.

Keywords: deon04

We propose a computationally oriented non-monotonic multi-modal logic arising from the combination of agency, intention and obligation. We argue about the defeasible nature of these notions and then we show how to represent and reason with them in the setting of defeasible logic.

Keywords: deon04

We consider the logical representation of obligations on stative expressions such as The yard must be clean in the context of legal contract formation, execution, and monitoring (cf. Wyner ([28])). In a contract, the expression may understood as an obligation to maintain a property. We use a Deontic Action Logic to represent obligations over the course of time (Khosla and Maibaum ([13]) and Meyer ([17])). Our analysis is in contrast to dAltan, Meyer, and Wieringa ([6]), who reduce deontic operators to an Alethic Logic plus a violation proposition (Anderson and Moore ([1]), which has no temporal component. In addition, they use a Deontic Action Logic to represent obligations on actions. We claim the Alethic component of the logic is redundant for the purposes of representing obligations on stative expressions in a contract. In the course of the analysis, we introduce polynormativity, which contrasts with the binormativity of standard DAL or alethic logic plus a violation proposition. We discuss the advantages of polynormativity in reasoning from violations and fulfillments.

Keywords: deon04

Obligation change raises the frame problem which is to characterise what obligations remain unchanged after an action has been performed. Many general solutions have been proposed but even if they are attractive from a thoretical point of view they have practical drawbacks. In this paper simple solutions are proposed thanks to the restriction to obligations that take the form of modal literals. These solutions are presented in the framework of dependence logic and of situation calculus, and it is shown that they are based on the same intuitive idea. This idea is to express that we have a complete representation of actions and circumstances that can change an obligation.

Keywords: deon04

In this paper we consider the relation between desires and obligations in normative multiagent systems. We introduce a model of their relation based on what we call the social delegation cycle, which explains the creation of norms from agent desires in three steps. First individual agent desires generate group goals, then a group goal is individualized in a social norm, and finally the norm is accepted by the agents when it leads to the fulfilment of the desires the cycle started with. We formalize the social delegation cycle by formalizing goal generation as a merging process of the individual agent desires, we formalize norm creation as a planning process for both the obligation and the associated sanctions or rewards, and we formalize the acceptance relation as both a belief of agents that the fulfilment of the norm leads to achievement of their desires, and the belief that other agents will act according to the norm.

Keywords: deon04

This paper studies the logic of a dyadic modal operator for being obliged to meet a condition ρ before a condition δ becomes true. Starting from basic intuitions we arrive at a simple semantics for deadline obligations in terms of branching time models. We show that this notion of deadline obligation can be characterized in the branching time logic CTL. The defined operator obeys intuitive logic properties, like monotony w.r.t. ρ and anti-monotony w.r.t. δ, and avoids some counter-intuitive properties like agglomeration w.r.t ρ and weak agglomeration w.r.t. δ. However, obligations of this type are implied by the actual achievement of ρ before the deadline. We argue that this problem is caused by the fact that we model the obligation only from the point of view of its violation conditions. We show that the property might be eliminated by considering success conditions also.

Keywords: deon04

We consider three infinite hierarchies of what I call two-dimensional temporal logics with explicit realization operators, viz. (i) one without historical or deontic modalities, (ii) one with historical but without deontic modalities, and (iii) one with historical and with dyadic deontic modalities for conditional obligation and permission. Sound and complete axiomatizations are obtained for all three hierarchies relative to a simplified version of the finite co-ordinate system semantics given for so-called T x W logic of historical necessity in (1999).

Keywords: deon04

Since it was first proposed by Moses, Shoham, and Tennenholtz, the social laws paradigm has proved to be one of the most compelling approaches to the offline coordination of multiagent systems. In this paper, we make three key contributions to the theory and practice of social laws in multiagent systems. First, we show that the Alternating-time Temporal Logic of Alur, Henzinger, and Kupferman provides an elegant and powerful framework within which to express and understand social laws for multiagent systems. Second, we show that the effectiveness, feasibility, and synthesis problems for social laws may naturally be framed as atl model checking problems, and that as a consequence, existing atl model checkers may be applied to these problems. We illustrate the concepts and techniques developed by means of a running example. (joint with with Wiebe van der Hoek and Mark Roberts)

Keywords: deon04

Many obligations can be seen as arising from contractual arrangements (or from situations resembling contractual arrangements) among agents. My obligation to repay you the 100 I borrowed is associated with a simple (quite possibly tacit and informal) contractual arrangement between us. My obligations as an employee of my university are associated with contractual arrangements with my university, which may be considered a collective agent. My university in turn has certain obligations to me. But some obligations change over time as a result of changing circumstances, and in at least some cases the changes that occur can be thought of as involving a renegotiation of a contract among the parties involved. When I pay back half the money I owe you, I have not fulfilled my original obligation; but neither does that original obligation to pay you 100 still stand. Instead, we may consider, we have renegotiated my contract with you so that my remaining obligation is to pay you 50 (or, depending on details of the negotiation, perhaps 50 plus interest or a late fee). Analogous, though usually more explicit, renegotiations of contracts are commonplace in the corporate world as well. As we examine this way of looking at normative situations, we find a number of complications which must be considered, many of which we are accustomed to set aside in simpler treatments of deontic logic. We must consider the relationships among distinct agents, not just consider the normative positions of one agent at a time. We need to make room for corporate agents, i.e. agents which are organizations or groups of other agents. We need to consider that a single agent may be involved in multiple contractual arrangements, and thus may have a number of different normative roles simultaneously. As a result, we must make room for conflicting obligations. And we must allow for various kinds of modifications of contractual arrangements over time, including negotiation and renegotiation. Moreover, ultimately we must consider ways in which complex organizations are related to their changing roster of participant agents, whose roles within the organization alter over time. In this paper, I will discuss a number of the issues which arise in any attempt to formalize a contractual model of our changing normative situations.

Keywords: deon04

This work addresses the issue of obligations directed to groups of agents. Our main concern consists in providing a formal analysis of the structure connecting collective obligations to individual ones: which individual agent in a group should be held responsible if an obligation directed to the whole group is not fulfilled? To this aim, concepts from planning literature (like plan and task allocation) are first used in order to conceptualize collective agency, and then formalized by means of a dynamic deontic logic framework. Within this setting, a formal account of the notion of coordination, intended as management of interdependencies among agents activities, is also provided.

Keywords: deon04

Keywords: deon04