It is useful to prove that an implementation correctly follows a specification. But even with a provably correct implementation, given a choice, would a node choose to follow it? This paper explores how to create distributed system specifications that will be faithfully implemented in networks with rational nodes, so that no node will choose to deviate. Given a strategyproof centralized mechanism, and given a network of nodes modeled as having rational-manipulation faults, we provide a proof technique to establish the incentive-, communication-, and algorithm-compatibility properties that guarantee that participating nodes are faithful to a suggested specification. As a case study, we apply our methods to extend the strategyproof interdomain routing mechanism proposed by Feigenbaum, Papadimitriou, Sami, and Shenker (FPSS) [7] , defining a faithful implementation.  Categories and Subject Descriptors Algorithms, Design, Economics. Distributed Algorithmic Mechanism Design, Computational Mechanism Design, Rational Manipulation, Algorithm Compatibility, Communication Compatibility, Incentive Compatibility, Failure Models, Rational Failure This paper considers how to create provably faithful specifications that are implemented on networks of rational nodes. In these networks, a node acts in self-interested fashion to better its outcome in some distributed mechanism. It is not hard to find evidence of rational behavior in existing distributed systems. Internet users can game their TCP settings to obtain better service at the expense of others [27] . Users cheat in distributed computations in order to Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. This behavior can be classified as a type of failure, which should stand independently from other types of failures in distributed systems and is indicative of an underlying incentive problem in a system's design when run on a network with rational nodes. Whereas traditional failure models are overcome by relying on redundancy, rational manipulation can also be overcome with design techniques such as problem partitioning, catch-and-punish, and incentives. In such a network one can state a strong claim about the faithfulness of each node's implementation. This claim of faithfulness, like traditional distributed systems claims (e.g: safety and liveness [35]), is made with particular assumptions about the knowledge available to network participants. Typical distributed systems knowledge assumptions include node failure characteristics: for instance, a given specification might state safety properties on the assumption that no link failures will occur in the network. The knowledge assumptions particularly relevant to our scenario are drawn from economics and known as equilibrium concepts. This paper focuses on (and justifies) the use of ex post Nash (without collusion) as a reasonable knowledge assumption. The ex post Nash solution concept does not require nodes to have any knowledge of the private information of other nodes, but does assume that nodes are rational utility-maximizers and model other participants as such. When one can prove that a specification will be faithfully followed by rational nodes in a distributed network, one can certify the system to be incentive-, communication-, and algorithm-compatible (IC, CC and AC). Such a system is provably robust against rational manipulation. We introduce a general decomposition proof technique, that splits a distributed algorithm into disjoint phases, each of which can be proven IC, CC, and AC by showing that a node cannot benefit from any combination of deviation from the specification relevant to that phase. To ensure that one phase is disjoint from the next, a phase is certified before the subsequent phase begins.
The authors of REF considered the problem of creating distributed system specifications that will be faithfully implemented in networks with rational (i.e., self-interested) nodes so that no node will choose to deviate from the specification.
Specification faithfulness in networks with rational nodes
PODC '04
Computer Science