We here describe research into the formal specification and implementation of resource-bounded agents. In particular, we provide an overview of our work on incorporating resource limitations into executable agent specifications. In addition, we outline future directions, highlighting both their promise and their problems.

In order to design and implement electronic institutions that incorporate norms governing the behavior of the participants of those institutions, some crucial steps should be taken. The first problem is that human norms are (on purpose) specified on an abstract level. This ensures applicability of the norms over long periods of time in many different circumstances. However, for an electronic institution to function according to those norms, they should be concrete enough to be able to check them run time. A (...) second problem is that norms describe which behavior is desirable and permitted, but not how this is achieved in an institution. In the “real world" regulations often indicate procedures for implementing and enforcing the law. Likewise we should devise means to annotate the norms with practical aspects such as enforcement mechanisms, sanctions, etc. in order to get requirements for an institution that will enforce norms (by either constraining behavior within the norms or reacting to violation of the norms). The choice of which kind of mechanism is chosen is not a normative one, but usually based on criteria of efficiency and/or feasibility of the mechanism. In this paper we present our view on how to approach these problems and other related issues to be solved in order to develop e-institutions capable to operate in complex, highly regulated scenarios. (shrink)

This paper introduces a multi-modal polymorphic type theory to model epistemic processes characterized by trust, defined as a second-order relation affecting the communication process between sources and a receiver. In this language, a set of senders is expressed by a modal prioritized context, whereas the receiver is formulated in terms of a contextually derived modal judgement. Introduction and elimination rules for modalities are based on the polymorphism of terms in the language. This leads to a multi-modal non-homogeneous version of a (...) type theory, in which we show the embedding of the modal operators into standard group knowledge operators. (shrink)