TY - JOUR
AB - Social dilemmas occur when incentives for individuals are misaligned with group interests 1-7 . According to the 'tragedy of the commons', these misalignments can lead to overexploitation and collapse of public resources. The resulting behaviours can be analysed with the tools of game theory 8 . The theory of direct reciprocity 9-15 suggests that repeated interactions can alleviate such dilemmas, but previous work has assumed that the public resource remains constant over time. Here we introduce the idea that the public resource is instead changeable and depends on the strategic choices of individuals. An intuitive scenario is that cooperation increases the public resource, whereas defection decreases it. Thus, cooperation allows the possibility of playing a more valuable game with higher payoffs, whereas defection leads to a less valuable game. We analyse this idea using the theory of stochastic games 16-19 and evolutionary game theory. We find that the dependence of the public resource on previous interactions can greatly enhance the propensity for cooperation. For these results, the interaction between reciprocity and payoff feedback is crucial: neither repeated interactions in a constant environment nor single interactions in a changing environment yield similar cooperation rates. Our framework shows which feedbacks between exploitation and environment - either naturally occurring or designed - help to overcome social dilemmas.
AU - Hilbe, Christian
AU - Šimsa, Štepán
AU - Chatterjee, Krishnendu
AU - Nowak, Martin
ID - 157
IS - 7713
JF - Nature
TI - Evolution of cooperation in stochastic games
VL - 559
ER -
TY - JOUR
AB - Reciprocity is a major factor in human social life and accounts for a large part of cooperation in our communities. Direct reciprocity arises when repeated interactions occur between the same individuals. The framework of iterated games formalizes this phenomenon. Despite being introduced more than five decades ago, the concept keeps offering beautiful surprises. Recent theoretical research driven by new mathematical tools has proposed a remarkable dichotomy among the crucial strategies: successful individuals either act as partners or as rivals. Rivals strive for unilateral advantages by applying selfish or extortionate strategies. Partners aim to share the payoff for mutual cooperation, but are ready to fight back when being exploited. Which of these behaviours evolves depends on the environment. Whereas small population sizes and a limited number of rounds favour rivalry, partner strategies are selected when populations are large and relationships stable. Only partners allow for evolution of cooperation, while the rivals’ attempt to put themselves first leads to defection. Hilbe et al. synthesize recent theoretical work on zero-determinant and ‘rival’ versus ‘partner’ strategies in social dilemmas. They describe the environments under which these contrasting selfish or cooperative strategies emerge in evolution.
AU - Hilbe, Christian
AU - Chatterjee, Krishnendu
AU - Nowak, Martin
ID - 419
JF - Nature Human Behaviour
TI - Partners and rivals in direct reciprocity
VL - 2
ER -
TY - JOUR
AB - Direct reciprocity is a mechanism for cooperation among humans. Many of our daily interactions are repeated. We interact repeatedly with our family, friends, colleagues, members of the local and even global community. In the theory of repeated games, it is a tacit assumption that the various games that a person plays simultaneously have no effect on each other. Here we introduce a general framework that allows us to analyze “crosstalk” between a player’s concurrent games. In the presence of crosstalk, the action a person experiences in one game can alter the person’s decision in another. We find that crosstalk impedes the maintenance of cooperation and requires stronger levels of forgiveness. The magnitude of the effect depends on the population structure. In more densely connected social groups, crosstalk has a stronger effect. A harsh retaliator, such as Tit-for-Tat, is unable to counteract crosstalk. The crosstalk framework provides a unified interpretation of direct and upstream reciprocity in the context of repeated games.
AU - Reiter, Johannes
AU - Hilbe, Christian
AU - Rand, David
AU - Chatterjee, Krishnendu
AU - Nowak, Martin
ID - 454
IS - 1
JF - Nature Communications
TI - Crosstalk in concurrent repeated games impedes direct reciprocity and requires stronger levels of forgiveness
VL - 9
ER -
TY - CONF
AB - A model of computation that is widely used in the formal analysis of reactive systems is symbolic algorithms. In this model the access to the input graph is restricted to consist of symbolic operations, which are expensive in comparison to the standard RAM operations. We give lower bounds on the number of symbolic operations for basic graph problems such as the computation of the strongly connected components and of the approximate diameter as well as for fundamental problems in model checking such as safety, liveness, and coliveness. Our lower bounds are linear in the number of vertices of the graph, even for constant-diameter graphs. For none of these problems lower bounds on the number of symbolic operations were known before. The lower bounds show an interesting separation of these problems from the reachability problem, which can be solved with O(D) symbolic operations, where D is the diameter of the graph. Additionally we present an approximation algorithm for the graph diameter which requires Õ(n/D) symbolic steps to achieve a (1 +ϵ)-approximation for any constant > 0. This compares to O(n/D) symbolic steps for the (naive) exact algorithm and O(D) symbolic steps for a 2-approximation. Finally we also give a refined analysis of the strongly connected components algorithms of [15], showing that it uses an optimal number of symbolic steps that is proportional to the sum of the diameters of the strongly connected components.
AU - Chatterjee, Krishnendu
AU - Dvorák, Wolfgang
AU - Henzinger, Monika
AU - Loitzenbauer, Veronika
ID - 310
TI - Lower bounds for symbolic computation on graphs: Strongly connected components, liveness, safety and diameter
ER -
TY - CONF
AB - Probabilistic programs extend classical imperative programs with real-valued random variables and random branching. The most basic liveness property for such programs is the termination property. The qualitative (aka almost-sure) termination problem asks whether a given program program terminates with probability 1. While ranking functions provide a sound and complete method for non-probabilistic programs, the extension of them to probabilistic programs is achieved via ranking supermartingales (RSMs). Although deep theoretical results have been established about RSMs, their application to probabilistic programs with nondeterminism has been limited only to programs of restricted control-flow structure. For non-probabilistic programs, lexicographic ranking functions provide a compositional and practical approach for termination analysis of real-world programs. In this work we introduce lexicographic RSMs and show that they present a sound method for almost-sure termination of probabilistic programs with nondeterminism. We show that lexicographic RSMs provide a tool for compositional reasoning about almost-sure termination, and for probabilistic programs with linear arithmetic they can be synthesized efficiently (in polynomial time). We also show that with additional restrictions even asymptotic bounds on expected termination time can be obtained through lexicographic RSMs. Finally, we present experimental results on benchmarks adapted from previous work to demonstrate the effectiveness of our approach.
AU - Agrawal, Sheshansh
AU - Chatterjee, Krishnendu
AU - Novotny, Petr
ID - 325
IS - POPL
TI - Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs
VL - 2
ER -
TY - CONF
AB - Partially observable Markov decision processes (POMDPs) are widely used in probabilistic planning problems in which an agent interacts with an environment using noisy and imprecise sensors. We study a setting in which the sensors are only partially defined and the goal is to synthesize “weakest” additional sensors, such that in the resulting POMDP, there is a small-memory policy for the agent that almost-surely (with probability 1) satisfies a reachability objective. We show that the problem is NP-complete, and present a symbolic algorithm by encoding the problem into SAT instances. We illustrate trade-offs between the amount of memory of the policy and the number of additional sensors on a simple example. We have implemented our approach and consider three classical POMDP examples from the literature, and show that in all the examples the number of sensors can be significantly decreased (as compared to the existing solutions in the literature) without increasing the complexity of the policies.
AU - Chatterjee, Krishnendu
AU - Chemlík, Martin
AU - Topcu, Ufuk
ID - 34
TI - Sensor synthesis for POMDPs with reachability objectives
VL - 2018
ER -
TY - CONF
AB - We consider planning problems for graphs, Markov decision processes (MDPs), and games on graphs. While graphs represent the most basic planning model, MDPs represent interaction with nature and games on graphs represent interaction with an adversarial environment. We consider two planning problems where there are k different target sets, and the problems are as follows: (a) the coverage problem asks whether there is a plan for each individual target set; and (b) the sequential target reachability problem asks whether the targets can be reached in sequence. For the coverage problem, we present a linear-time algorithm for graphs, and quadratic conditional lower bound for MDPs and games on graphs. For the sequential target problem, we present a linear-time algorithm for graphs, a sub-quadratic algorithm for MDPs, and a quadratic conditional lower bound for games on graphs. Our results with conditional lower bounds establish (i) model-separation results showing that for the coverage problem MDPs and games on graphs are harder than graphs and for the sequential reachability problem games on graphs are harder than MDPs and graphs; and (ii) objective-separation results showing that for MDPs the coverage problem is harder than the sequential target problem.
AU - Chatterjee, Krishnendu
AU - Dvorák, Wolfgang
AU - Henzinger, Monika
AU - Svozil, Alexander
ID - 35
T2 - 28th International Conference on Automated Planning and Scheduling
TI - Algorithms and conditional lower bounds for planning problems
ER -
TY - CONF
AB - Smart contracts are computer programs that are executed by a network of mutually distrusting agents, without the need of an external trusted authority. Smart contracts handle and transfer assets of considerable value (in the form of crypto-currency like Bitcoin). Hence, it is crucial that their implementation is bug-free. We identify the utility (or expected payoff) of interacting with such smart contracts as the basic and canonical quantitative property for such contracts. We present a framework for such quantitative analysis of smart contracts. Such a formal framework poses new and novel research challenges in programming languages, as it requires modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior and modeling utilities which are not specified as standard temporal properties such as safety and termination. While game-theoretic incentives have been analyzed in the security community, their analysis has been restricted to the very special case of stateless games. However, to analyze smart contracts, stateful analysis is required as it must account for the different program states of the protocol. Our main contributions are as follows: we present (i)~a simplified programming language for smart contracts; (ii)~an automatic translation of the programs to state-based games; (iii)~an abstraction-refinement approach to solve such games; and (iv)~experimental results on real-world-inspired smart contracts.
AU - Chatterjee, Krishnendu
AU - Goharshady, Amir
AU - Velner, Yaron
ID - 311
TI - Quantitative analysis of smart contracts
VL - 10801
ER -
TY - CONF
AB - We present a secure approach for maintaining andreporting credit history records on the Blockchain. Our ap-proach removes third-parties such as credit reporting agen-cies from the lending process and replaces them with smartcontracts. This allows customers to interact directly with thelenders or banks while ensuring the integrity, unmalleabilityand privacy of their credit data. Additionally, each customerhas full control over complete or selective disclosure of hercredit records, eliminating the risk of privacy violations or databreaches. Moreover, our approach provides strong guaranteesfor the lenders as well. A lender can check both correctness andcompleteness of the credit data disclosed to her. This is the firstapproach that can perform all credit reporting tasks withouta central authority or changing the financial mechanisms*.
AU - Goharshady, Amir Kafshdar
AU - Behrouz, Ali
AU - Chatterjee, Krishnendu
ID - 6340
SN - 978-1-5386-7975-3
T2 - Proceedings of the IEEE International Conference on Blockchain
TI - Secure Credit Reporting on the Blockchain
ER -
TY - JOUR
AB - We study algorithmic questions wrt algebraic path properties in concurrent systems, where the transitions of the system are labeled from a complete, closed semiring. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time.
Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.
AU - Chatterjee, Krishnendu
AU - Ibsen-Jensen, Rasmus
AU - Goharshady, Amir Kafshdar
AU - Pavlogiannis, Andreas
ID - 6009
IS - 3
JF - ACM Transactions on Programming Languages and Systems
SN - 0164-0925
TI - Algorithms for algebraic path properties in concurrent systems of constant treewidth components
VL - 40
ER -