Scrip systems, where users pay for service with an artificial currency (scrip) created for the system, are an attractive solution to a variety of problems faced by P2P and distributed systems. Despite the interest in building scrip systems, relatively little work has been done to help answer basic design questions. For example, how much money should there be in the system? What will happen if some of the users start hoarding money? I present a game-theoretic model of a scrip system and show that this model has Nash equilibria where all agents use simple strategies known as threshold strategies. In fact, the same techniques provide an efficient method of computing these equilibria as well as the equilibrium distribution of wealth. I show how these results provide practical insights into the design of scrip systems. For example, social welfare is maximized by increasing the money supply up to the point that the system experiences a "monetary crash," where money is sufficiently devalued that no agent is willing to perform a service. Hoarders generally decrease social welfare but, surprisingly, they also promote system stability by helping prevent monetary crashes. Furthermore, the effects of hoarders can be mitigated simply by printing more money.

This represents joint work with Ian Kash and Eric Friedman.

Multi-agent systems describe interactions of multiple entities called agents, often assumed to be intelligent and autonomous. Alternating-time temporal logic (ATL*) and its fragment ATL are logics which allow for reasoning about strategic interactions in such systems, by extending the framework of temporal logic with the game-theoretic notion of strategic ability. While model checking of ATL under perfect information seems to be feasible in practice, model checking of ATL under imperfect information is still applicable only to small and medium size systems. This lecture is about selected approaches which can make model checking ATL*, ATL and its discrete time extension TATL more efficient. We start with multi-valued versions of ATL* and show the general method for translation from multi-valued to two-valued model checking. Next, we investigate ATL* without the next step operator, interpreted in asynchronous systems and show that for memoryless imperfect information contrary to memoryless perfect information, one can apply partial order reduction methods. Finally, we build a hierarchy of strategies for TATL comparing the expressive power of the logic against ATL and discuss a possible impact of this hierarchy on improving efficiency of model checking TATL