@inproceedings{325,
abstract = {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.},
author = {Agrawal, Sheshansh and Chatterjee, Krishnendu and Novotny, Petr},
location = {Los Angeles, CA, USA},
number = {POPL},
publisher = {ACM},
title = {{Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs}},
doi = {10.1145/3158122},
volume = {2},
year = {2018},
}
@inproceedings{34,
abstract = {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.},
author = {Chatterjee, Krishnendu and Chemlík, Martin and Topcu, Ufuk},
location = {Delft, Netherlands},
pages = {47 -- 55},
publisher = {AAAI Press},
title = {{Sensor synthesis for POMDPs with reachability objectives}},
volume = {2018},
year = {2018},
}
@inproceedings{35,
abstract = {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.},
author = {Chatterjee, Krishnendu and Dvorák, Wolfgang and Henzinger, Monika and Svozil, Alexander},
booktitle = {28th International Conference on Automated Planning and Scheduling },
location = {Delft, Netherlands},
publisher = {AAAI Press},
title = {{Algorithms and conditional lower bounds for planning problems}},
year = {2018},
}
@article{419,
abstract = {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.},
author = {Hilbe, Christian and Chatterjee, Krishnendu and Nowak, Martin},
journal = {Nature Human Behaviour},
pages = {469–477},
publisher = {Nature Publishing Group},
title = {{Partners and rivals in direct reciprocity}},
doi = {10.1038/s41562-018-0320-9},
volume = {2},
year = {2018},
}
@article{454,
abstract = {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.},
author = {Reiter, Johannes and Hilbe, Christian and Rand, David and Chatterjee, Krishnendu and Nowak, Martin},
journal = {Nature Communications},
number = {1},
publisher = {Nature Publishing Group},
title = {{Crosstalk in concurrent repeated games impedes direct reciprocity and requires stronger levels of forgiveness}},
doi = {10.1038/s41467-017-02721-8},
volume = {9},
year = {2018},
}
@inproceedings{5679,
abstract = {We study the almost-sure termination problem for probabilistic programs. First, we show that supermartingales with lower bounds on conditional absolute difference provide a sound approach for the almost-sure termination problem. Moreover, using this approach we can obtain explicit optimal bounds on tail probabilities of non-termination within a given number of steps. Second, we present a new approach based on Central Limit Theorem for the almost-sure termination problem, and show that this approach can establish almost-sure termination of programs which none of the existing approaches can handle. Finally, we discuss algorithmic approaches for the two above methods that lead to automated analysis techniques for almost-sure termination of probabilistic programs.},
author = {Huang, Mingzhang and Fu, Hongfei and Chatterjee, Krishnendu},
editor = {Ryu, Sukyoung},
isbn = {9783030027674},
issn = {03029743},
location = {Wellington, New Zealand},
pages = {181--201},
publisher = {Springer},
title = {{New approaches for almost-sure termination of probabilistic programs}},
doi = {10.1007/978-3-030-02768-1_11},
volume = {11275},
year = {2018},
}
@inbook{59,
abstract = {Graph-based games are an important tool in computer science. They have applications in synthesis, verification, refinement, and far beyond. We review graphbased games with objectives on infinite plays. We give definitions and algorithms to solve the games and to give a winning strategy. The objectives we consider are mostly Boolean, but we also look at quantitative graph-based games and their objectives. Synthesis aims to turn temporal logic specifications into correct reactive systems. We explain the reduction of synthesis to graph-based games (or equivalently tree automata) using synthesis of LTL specifications as an example. We treat the classical approach that uses determinization of parity automata and more modern approaches.},
author = {Bloem, Roderick and Chatterjee, Krishnendu and Jobstmann, Barbara},
booktitle = {Handbook of Model Checking},
editor = {Henzinger, Thomas A and Clarke, Edmund M. and Veith, Helmut and Bloem, Roderick},
isbn = {978-3-319-10574-1},
pages = {921 -- 962},
publisher = {Springer},
title = {{Graph games and reactive synthesis}},
doi = {10.1007/978-3-319-10575-8_27},
year = {2018},
}
@inproceedings{5967,
abstract = {The Big Match is a multi-stage two-player game. In each stage Player 1 hides one or two pebbles in his hand, and his opponent has to guess that number; Player 1 loses a point if Player 2 is correct, and otherwise he wins a point. As soon as Player 1 hides one pebble, the players cannot change their choices in any future stage.
Blackwell and Ferguson (1968) give an ε-optimal strategy for Player 1 that hides, in each stage, one pebble with a probability that depends on the entire past history. Any strategy that depends just on the clock or on a finite memory is worthless. The long-standing natural open problem has been whether every strategy that depends just on the clock and a finite memory is worthless. We prove that there is such a strategy that is ε-optimal. In fact, we show that just two states of memory are sufficient.
},
author = {Hansen, Kristoffer Arnsfelt and Ibsen-Jensen, Rasmus and Neyman, Abraham},
booktitle = {Proceedings of the 2018 ACM Conference on Economics and Computation - EC '18},
isbn = {9781450358293},
location = {Ithaca, NY, United States},
pages = {149--150},
publisher = {ACM Press},
title = {{The Big Match with a clock and a bit of memory}},
doi = {10.1145/3219166.3219198},
year = {2018},
}
@article{5993,
abstract = {In this article, we consider the termination problem of probabilistic programs with real-valued variables. Thequestions concerned are: qualitative ones that ask (i) whether the program terminates with probability 1(almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); andquantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) tocompute a boundBsuch that the probability not to terminate afterBsteps decreases exponentially (con-centration problem). To solve these questions, we utilize the notion of ranking supermartingales, which isa powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmicsynthesis of linear ranking-supermartingales over affine probabilistic programs (Apps) with both angelic anddemonic non-determinism. An important subclass of Apps is LRApp which is defined as the class of all Appsover which a linear ranking-supermartingale exists.Our main contributions are as follows. Firstly, we show that the membership problem of LRApp (i) canbe decided in polynomial time for Apps with at most demonic non-determinism, and (ii) isNP-hard and inPSPACEfor Apps with angelic non-determinism. Moreover, theNP-hardness result holds already for Appswithout probability and demonic non-determinism. Secondly, we show that the concentration problem overLRApp can be solved in the same complexity as for the membership problem of LRApp. Finally, we show thatthe expectation problem over LRApp can be solved in2EXPTIMEand isPSPACE-hard even for Apps withoutprobability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate theeffectiveness of our approach to answer the qualitative and quantitative questions over Apps with at mostdemonic non-determinism.},
author = {Chatterjee, Krishnendu and Fu, Hongfei and Novotný, Petr and Hasheminezhad, Rouzbeh},
issn = {0164-0925},
journal = {ACM Transactions on Programming Languages and Systems},
number = {2},
publisher = {Association for Computing Machinery (ACM)},
title = {{Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs}},
doi = {10.1145/3174800},
volume = {40},
year = {2018},
}
@article{5751,
abstract = {Because of the intrinsic randomness of the evolutionary process, a mutant with a fitness advantage has some chance to be selected but no certainty. Any experiment that searches for advantageous mutants will lose many of them due to random drift. It is therefore of great interest to find population structures that improve the odds of advantageous mutants. Such structures are called amplifiers of natural selection: they increase the probability that advantageous mutants are selected. Arbitrarily strong amplifiers guarantee the selection of advantageous mutants, even for very small fitness advantage. Despite intensive research over the past decade, arbitrarily strong amplifiers have remained rare. Here we show how to construct a large variety of them. Our amplifiers are so simple that they could be useful in biotechnology, when optimizing biological molecules, or as a diagnostic tool, when searching for faster dividing cells or viruses. They could also occur in natural population structures.},
author = {Pavlogiannis, Andreas and Tkadlec, Josef and Chatterjee, Krishnendu and Nowak, Martin A.},
issn = {2399-3642},
journal = {Communications Biology},
number = {1},
publisher = {Springer Nature},
title = {{Construction of arbitrarily strong amplifiers of natural selection using evolutionary graph theory}},
doi = {10.1038/s42003-018-0078-7},
volume = {1},
year = {2018},
}
@article{738,
abstract = {This paper is devoted to automatic competitive analysis of real-time scheduling algorithms for firm-deadline tasksets, where only completed tasks con- tribute some utility to the system. Given such a taskset T , the competitive ratio of an on-line scheduling algorithm A for T is the worst-case utility ratio of A over the utility achieved by a clairvoyant algorithm. We leverage the theory of quantitative graph games to address the competitive analysis and competitive synthesis problems. For the competitive analysis case, given any taskset T and any finite-memory on- line scheduling algorithm A , we show that the competitive ratio of A in T can be computed in polynomial time in the size of the state space of A . Our approach is flexible as it also provides ways to model meaningful constraints on the released task sequences that determine the competitive ratio. We provide an experimental study of many well-known on-line scheduling algorithms, which demonstrates the feasibility of our competitive analysis approach that effectively replaces human ingenuity (required Preliminary versions of this paper have appeared in Chatterjee et al. ( 2013 , 2014 ). B Andreas Pavlogiannis pavlogiannis@ist.ac.at Krishnendu Chatterjee krish.chat@ist.ac.at Alexander Kößler koe@ecs.tuwien.ac.at Ulrich Schmid s@ecs.tuwien.ac.at 1 IST Austria (Institute of Science and Technology Austria), Am Campus 1, 3400 Klosterneuburg, Austria 2 Embedded Computing Systems Group, Vienna University of Technology, Treitlstrasse 3, 1040 Vienna, Austria 123 Real-Time Syst for finding worst-case scenarios) by computing power. For the competitive synthesis case, we are just given a taskset T , and the goal is to automatically synthesize an opti- mal on-line scheduling algorithm A , i.e., one that guarantees the largest competitive ratio possible for T . We show how the competitive synthesis problem can be reduced to a two-player graph game with partial information, and establish that the compu- tational complexity of solving this game is Np -complete. The competitive synthesis problem is hence in Np in the size of the state space of the non-deterministic labeled transition system encoding the taskset. Overall, the proposed framework assists in the selection of suitable scheduling algorithms for a given taskset, which is in fact the most common situation in real-time systems design. },
author = {Chatterjee, Krishnendu and Pavlogiannis, Andreas and Kößler, Alexander and Schmid, Ulrich},
journal = {Real-Time Systems},
number = {1},
pages = {166 -- 207},
publisher = {Springer},
title = {{Automated competitive analysis of real time scheduling with graph games}},
doi = {10.1007/s11241-017-9293-4},
volume = {54},
year = {2018},
}
@inproceedings{79,
abstract = {Markov Decision Processes (MDPs) are a popular class of models suitable for solving control decision problems in probabilistic reactive systems. We consider parametric MDPs (pMDPs) that include parameters in some of the transition probabilities to account for stochastic uncertainties of the environment such as noise or input disturbances. We study pMDPs with reachability objectives where the parameter values are unknown and impossible to measure directly during execution, but there is a probability distribution known over the parameter values. We study for the first time computing parameter-independent strategies that are expectation optimal, i.e., optimize the expected reachability probability under the probability distribution over the parameters. We present an encoding of our problem to partially observable MDPs (POMDPs), i.e., a reduction of our problem to computing optimal strategies in POMDPs. We evaluate our method experimentally on several benchmarks: a motivating (repeated) learner model; a series of benchmarks of varying configurations of a robot moving on a grid; and a consensus protocol.},
author = {Arming, Sebastian and Bartocci, Ezio and Chatterjee, Krishnendu and Katoen, Joost P and Sokolova, Ana},
location = {Beijing, China},
pages = {53--70},
publisher = {Springer},
title = {{Parameter-independent strategies for pMDPs via POMDPs}},
doi = {10.1007/978-3-319-99154-2_4},
volume = {11024},
year = {2018},
}
@inbook{86,
abstract = {Responsiveness—the requirement that every request to a system be eventually handled—is one of the fundamental liveness properties of a reactive system. Average response time is a quantitative measure for the responsiveness requirement used commonly in performance evaluation. We show how average response time can be computed on state-transition graphs, on Markov chains, and on game graphs. In all three cases, we give polynomial-time algorithms.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan},
booktitle = {Principles of Modeling},
editor = {Lohstroh, Marten and Derler, Patricia and Sirjani, Marjan},
pages = {143 -- 161},
publisher = {Springer},
title = {{Computing average response time}},
doi = {10.1007/978-3-319-95246-8_9},
volume = {10760},
year = {2018},
}
@inproceedings{311,
abstract = {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.},
author = {Chatterjee, Krishnendu and Goharshady, Amir and Velner, Yaron},
location = {Thessaloniki, Greece},
pages = {739 -- 767},
publisher = {Springer},
title = {{Quantitative analysis of smart contracts}},
doi = {10.1007/978-3-319-89884-1_26},
volume = {10801},
year = {2018},
}
@inproceedings{6340,
abstract = {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*.},
author = {Goharshady, Amir Kafshdar and Behrouz, Ali and Chatterjee, Krishnendu},
booktitle = {Proceedings of the IEEE International Conference on Blockchain},
isbn = {978-1-5386-7975-3 },
location = {Halifax, Canada},
pages = {1343--1348},
publisher = {IEEE},
title = {{Secure Credit Reporting on the Blockchain}},
doi = {10.1109/Cybermatics_2018.2018.00231},
year = {2018},
}
@article{6009,
abstract = {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.
},
author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Goharshady, Amir Kafshdar and Pavlogiannis, Andreas},
issn = {0164-0925},
journal = {ACM Transactions on Programming Languages and Systems},
number = {3},
publisher = {Association for Computing Machinery (ACM)},
title = {{Algorithms for algebraic path properties in concurrent systems of constant treewidth components}},
doi = {10.1145/3210257},
volume = {40},
year = {2018},
}
@inproceedings{5977,
abstract = {We consider the stochastic shortest path (SSP)problem for succinct Markov decision processes(MDPs), where the MDP consists of a set of vari-ables, and a set of nondeterministic rules that up-date the variables. First, we show that several ex-amples from the AI literature can be modeled assuccinct MDPs. Then we present computationalapproaches for upper and lower bounds for theSSP problem: (a) for computing upper bounds, ourmethod is polynomial-time in the implicit descrip-tion of the MDP; (b) for lower bounds, we present apolynomial-time (in the size of the implicit descrip-tion) reduction to quadratic programming. Our ap-proach is applicable even to infinite-state MDPs.Finally, we present experimental results to demon-strate the effectiveness of our approach on severalclassical examples from the AI literature.},
author = {Chatterjee, Krishnendu and Fu, Hongfei and Goharshady, Amir and Okati, Nastaran},
booktitle = {Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence},
isbn = {978-099924112-7},
issn = {10450823},
location = {Stockholm, Sweden},
pages = {4700--4707},
publisher = {IJCAI},
title = {{Computational approaches for stochastic shortest path on succinct MDPs}},
doi = {10.24963/ijcai.2018/653},
volume = {2018},
year = {2018},
}
@inproceedings{66,
abstract = {Crypto-currencies are digital assets designed to work as a medium of exchange, e.g., Bitcoin, but they are susceptible to attacks (dishonest behavior of participants). A framework for the analysis of attacks in crypto-currencies requires (a) modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior; (b) concurrent interactions between participants; and (c) analysis of long-term monetary gains. Traditional game-theoretic approaches for the analysis of security protocols consider either qualitative temporal properties such as safety and termination, or the very special class of one-shot (stateless) games. However, to analyze general attacks on protocols for crypto-currencies, both stateful analysis and quantitative objectives are necessary. In this work our main contributions are as follows: (a) we show how a class of concurrent mean-payo games, namely ergodic games, can model various attacks that arise naturally in crypto-currencies; (b) we present the first practical implementation of algorithms for ergodic games that scales to model realistic problems for crypto-currencies; and (c) we present experimental results showing that our framework can handle games with thousands of states and millions of transitions.},
author = {Chatterjee, Krishnendu and Goharshady, Amir and Ibsen-Jensen, Rasmus and Velner, Yaron},
isbn = {978-3-95977-087-3},
location = {Beijing, China},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Ergodic mean-payoff games for the analysis of attacks in crypto-currencies}},
doi = {10.4230/LIPIcs.CONCUR.2018.11},
volume = {118},
year = {2018},
}
@inproceedings{1009,
abstract = {A standard objective in partially-observable Markov decision processes (POMDPs) is to find a policy that maximizes the expected discounted-sum payoff. However, such policies may still permit unlikely but highly undesirable outcomes, which is problematic especially in safety-critical applications. Recently, there has been a surge of interest in POMDPs where the goal is to maximize the probability to ensure that the payoff is at least a given threshold, but these approaches do not consider any optimization beyond satisfying this threshold constraint. In this work we go beyond both the “expectation” and “threshold” approaches and consider a “guaranteed payoff optimization (GPO)” problem for POMDPs, where we are given a threshold t and the objective is to find a policy σ such that a) each possible outcome of σ yields a discounted-sum payoff of at least t, and b) the expected discounted-sum payoff of σ is optimal (or near-optimal) among all policies satisfying a). We present a practical approach to tackle the GPO problem and evaluate it on standard POMDP benchmarks.},
author = {Chatterjee, Krishnendu and Novotny, Petr and Pérez, Guillermo and Raskin, Jean and Zikelic, Djordje},
booktitle = {Proceedings of the 31st AAAI Conference on Artificial Intelligence},
location = {San Francisco, CA, United States},
pages = {3725 -- 3732},
publisher = {AAAI Press},
title = {{Optimizing expectation with guarantees in POMDPs}},
volume = {5},
year = {2017},
}
@inproceedings{1011,
abstract = {Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly equivalent, are standard models for interprocedural analysis. Yet RSMs are more convenient as they (a) explicitly model function calls and returns, and (b) specify many natural parameters for algorithmic analysis, e.g., the number of entries and exits. We consider a general framework where RSM transitions are labeled from a semiring and path properties are algebraic with semiring operations, which can model, e.g., interprocedural reachability and dataflow analysis problems. Our main contributions are new algorithms for several fundamental problems. As compared to a direct translation of RSMs to PDSs and the best-known existing bounds of PDSs, our analysis algorithm improves the complexity for finite-height semirings (that subsumes reachability and standard dataflow properties). We further consider the problem of extracting distance values from the representation structures computed by our algorithm, and give efficient algorithms that distinguish the complexity of a one-time preprocessing from the complexity of each individual query. Another advantage of our algorithm is that our improvements carry over to the concurrent setting, where we improve the bestknown complexity for the context-bounded analysis of concurrent RSMs. Finally, we provide a prototype implementation that gives a significant speed-up on several benchmarks from the SLAM/SDV project.},
author = {Chatterjee, Krishnendu and Kragl, Bernhard and Mishra, Samarth and Pavlogiannis, Andreas},
editor = {Yang, Hongseok},
issn = {03029743},
location = {Uppsala, Sweden},
pages = {287 -- 313},
publisher = {Springer},
title = {{Faster algorithms for weighted recursive state machines}},
doi = {10.1007/978-3-662-54434-1_11},
volume = {10201},
year = {2017},
}
@article{1065,
abstract = {We consider the problem of reachability in pushdown graphs. We study the problem for pushdown graphs with constant treewidth. Even for pushdown graphs with treewidth 1, for the reachability problem we establish the following: (i) the problem is PTIME-complete, and (ii) any subcubic algorithm for the problem would contradict the k-clique conjecture and imply faster combinatorial algorithms for cliques in graphs.},
author = {Chatterjee, Krishnendu and Osang, Georg F},
issn = {00200190},
journal = {Information Processing Letters},
pages = {25 -- 29},
publisher = {Elsevier},
title = {{Pushdown reachability with constant treewidth}},
doi = {10.1016/j.ipl.2017.02.003},
volume = {122},
year = {2017},
}
@article{1080,
abstract = {Reconstructing the evolutionary history of metastases is critical for understanding their basic biological principles and has profound clinical implications. Genome-wide sequencing data has enabled modern phylogenomic methods to accurately dissect subclones and their phylogenies from noisy and impure bulk tumour samples at unprecedented depth. However, existing methods are not designed to infer metastatic seeding patterns. Here we develop a tool, called Treeomics, to reconstruct the phylogeny of metastases and map subclones to their anatomic locations. Treeomics infers comprehensive seeding patterns for pancreatic, ovarian, and prostate cancers. Moreover, Treeomics correctly disambiguates true seeding patterns from sequencing artifacts; 7% of variants were misclassified by conventional statistical methods. These artifacts can skew phylogenies by creating illusory tumour heterogeneity among distinct samples. In silico benchmarking on simulated tumour phylogenies across a wide range of sample purities (15–95%) and sequencing depths (25-800 × ) demonstrates the accuracy of Treeomics compared with existing methods.},
author = {Reiter, Johannes and Makohon Moore, Alvin and Gerold, Jeffrey and Božić, Ivana and Chatterjee, Krishnendu and Iacobuzio Donahue, Christine and Vogelstein, Bert and Nowak, Martin},
issn = {20411723},
journal = {Nature Communications},
publisher = {Nature Publishing Group},
title = {{Reconstructing metastatic seeding patterns of human cancers}},
doi = {10.1038/ncomms14114},
volume = {8},
year = {2017},
}
@inproceedings{1194,
abstract = {Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with probability~1 (almost-sure termination). A powerful approach for this qualitative problem is the notion of ranking supermartingales with respect to a given set of invariants. The quantitative problem (probabilistic termination) asks for bounds on the termination probability. A fundamental and conceptual drawback of the existing approaches to address probabilistic termination is that even though the supermartingales consider the probabilistic behavior of the programs, the invariants are obtained completely ignoring the probabilistic aspect. In this work we address the probabilistic termination problem for linear-arithmetic probabilistic programs with nondeterminism. We define the notion of {\em stochastic invariants}, which are constraints along with a probability bound that the constraints hold. We introduce a concept of {\em repulsing supermartingales}. First, we show that repulsing supermartingales can be used to obtain bounds on the probability of the stochastic invariants. Second, we show the effectiveness of repulsing supermartingales in the following three ways: (1)~With a combination of ranking and repulsing supermartingales we can compute lower bounds on the probability of termination; (2)~repulsing supermartingales provide witnesses for refutation of almost-sure termination; and (3)~with a combination of ranking and repulsing supermartingales we can establish persistence properties of probabilistic programs. We also present results on related computational problems and an experimental evaluation of our approach on academic examples. },
author = {Chatterjee, Krishnendu and Novotny, Petr and Zikelic, Djordje},
issn = {07308566},
location = {Paris, France},
number = {1},
pages = {145 -- 160},
publisher = {ACM},
title = {{Stochastic invariants for probabilistic termination}},
doi = {10.1145/3009837.3009873},
volume = {52},
year = {2017},
}
@article{1407,
abstract = {We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study.},
author = {Svoreňová, Mária and Kretinsky, Jan and Chmelik, Martin and Chatterjee, Krishnendu and Cěrná, Ivana and Belta, Cǎlin},
journal = {Nonlinear Analysis: Hybrid Systems},
number = {2},
pages = {230 -- 253},
publisher = {Elsevier},
title = {{Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games}},
doi = {10.1016/j.nahs.2016.04.006},
volume = {23},
year = {2017},
}
@article{1294,
abstract = {We study controller synthesis problems for finite-state Markov decision processes, where the objective is to optimize the expected mean-payoff performance and stability (also known as variability in the literature). We argue that the basic notion of expressing the stability using the statistical variance of the mean payoff is sometimes insufficient, and propose an alternative definition. We show that a strategy ensuring both the expected mean payoff and the variance below given bounds requires randomization and memory, under both the above definitions. We then show that the problem of finding such a strategy can be expressed as a set of constraints.},
author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Forejt, Vojtěch and Kučera, Antonín},
journal = {Journal of Computer and System Sciences},
pages = {144 -- 170},
publisher = {Elsevier},
title = {{Trading performance for stability in Markov decision processes}},
doi = {10.1016/j.jcss.2016.09.009},
volume = {84},
year = {2017},
}
@article{464,
abstract = {The computation of the winning set for parity objectives and for Streett objectives in graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness conditions, the verification of open systems, checking interface compatibility, well-formedness of specifications, and the synthesis of reactive systems. We show how to compute the winning set on n vertices for (1) parity-3 (aka one-pair Streett) objectives in game graphs in time O(n5/2) and for (2) k-pair Streett objectives in graphs in time O(n2+nklogn). For both problems this gives faster algorithms for dense graphs and represents the first improvement in asymptotic running time in 15 years.},
author = {Chatterjee, Krishnendu and Henzinger, Monika and Loitzenbauer, Veronika},
issn = {18605974},
journal = {Logical Methods in Computer Science},
number = {3},
publisher = {International Federation of Computational Logic},
title = {{Improved algorithms for parity and Streett objectives}},
doi = {10.23638/LMCS-13(3:26)2017},
volume = {13},
year = {2017},
}
@article{1066,
abstract = {Simulation is an attractive alternative to language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. While fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable in general, whereas the (quantitative) simulation reduces to quantitative games, which admit pseudo-polynomial time algorithms.
In this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games, yet they still admit pseudo-polynomial time algorithms.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan and Velner, Yaron},
journal = {Information and Computation},
number = {2},
pages = {143 -- 166},
publisher = {Elsevier},
title = {{Quantitative fair simulation games}},
doi = {10.1016/j.ic.2016.10.006},
volume = {254},
year = {2017},
}
@article{466,
abstract = {We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem. },
author = {Chatterjee, Krishnendu and Křetínská, Zuzana and Kretinsky, Jan},
issn = {18605974},
journal = {Logical Methods in Computer Science},
number = {2},
publisher = {International Federation of Computational Logic},
title = {{Unifying two views on multiple mean-payoff objectives in Markov decision processes}},
doi = {10.23638/LMCS-13(2:15)2017},
volume = {13},
year = {2017},
}
@article{467,
abstract = {Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata or in any other known decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata, which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in runtime verification. We establish an almost-complete decidability picture for the basic decision problems about nested weighted automata and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan},
issn = {15293785},
journal = {ACM Transactions on Computational Logic (TOCL)},
number = {4},
publisher = {ACM},
title = {{Nested weighted automata}},
doi = {10.1145/3152769},
volume = {18},
year = {2017},
}
@article{465,
abstract = {The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 with edit distance at most k . We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite. },
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Ibsen-Jensen, Rasmus and Otop, Jan},
issn = {18605974},
journal = {Logical Methods in Computer Science},
number = {3},
publisher = {International Federation of Computational Logic},
title = {{Edit distance for pushdown automata}},
doi = {10.23638/LMCS-13(3:23)2017},
volume = {13},
year = {2017},
}
@article{512,
abstract = {The fixation probability is the probability that a new mutant introduced in a homogeneous population eventually takes over the entire population. The fixation probability is a fundamental quantity of natural selection, and known to depend on the population structure. Amplifiers of natural selection are population structures which increase the fixation probability of advantageous mutants, as compared to the baseline case of well-mixed populations. In this work we focus on symmetric population structures represented as undirected graphs. In the regime of undirected graphs, the strongest amplifier known has been the Star graph, and the existence of undirected graphs with stronger amplification properties has remained open for over a decade. In this work we present the Comet and Comet-swarm families of undirected graphs. We show that for a range of fitness values of the mutants, the Comet and Cometswarm graphs have fixation probability strictly larger than the fixation probability of the Star graph, for fixed population size and at the limit of large populations, respectively. },
author = {Pavlogiannis, Andreas and Tkadlec, Josef and Chatterjee, Krishnendu and Nowak, Martin},
issn = {20452322},
journal = {Scientific Reports},
number = {1},
publisher = {Nature Publishing Group},
title = {{Amplification on undirected population structures: Comets beat stars}},
doi = {10.1038/s41598-017-00107-w},
volume = {7},
year = {2017},
}
@inproceedings{551,
abstract = {Evolutionary graph theory studies the evolutionary dynamics in a population structure given as a connected graph. Each node of the graph represents an individual of the population, and edges determine how offspring are placed. We consider the classical birth-death Moran process where there are two types of individuals, namely, the residents with fitness 1 and mutants with fitness r. The fitness indicates the reproductive strength. The evolutionary dynamics happens as follows: in the initial step, in a population of all resident individuals a mutant is introduced, and then at each step, an individual is chosen proportional to the fitness of its type to reproduce, and the offspring replaces a neighbor uniformly at random. The process stops when all individuals are either residents or mutants. The probability that all individuals in the end are mutants is called the fixation probability, which is a key factor in the rate of evolution. We consider the problem of approximating the fixation probability. The class of algorithms that is extremely relevant for approximation of the fixation probabilities is the Monte-Carlo simulation of the process. Previous results present a polynomial-time Monte-Carlo algorithm for undirected graphs when r is given in unary. First, we present a simple modification: instead of simulating each step, we discard ineffective steps, where no node changes type (i.e., either residents replace residents, or mutants replace mutants). Using the above simple modification and our result that the number of effective steps is concentrated around the expected number of effective steps, we present faster polynomial-time Monte-Carlo algorithms for undirected graphs. Our algorithms are always at least a factor O(n2/ log n) faster as compared to the previous algorithms, where n is the number of nodes, and is polynomial even if r is given in binary. We also present lower bounds showing that the upper bound on the expected number of effective steps we present is asymptotically tight for undirected graphs. },
author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Nowak, Martin},
booktitle = {Leibniz International Proceedings in Informatics},
isbn = {978-395977046-0},
location = {Aalborg, Denmark},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Faster Monte Carlo algorithms for fixation probability of the Moran process on undirected graphs}},
doi = {10.4230/LIPIcs.MFCS.2017.61},
volume = {83},
year = {2017},
}
@inproceedings{552,
abstract = {Graph games provide the foundation for modeling and synthesis of reactive processes. Such games are played over graphs where the vertices are controlled by two adversarial players. We consider graph games where the objective of the first player is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a meanpayoff condition). There are two variants of the problem, namely, the threshold problem where the quantitative goal is to ensure that the mean-payoff value is above a threshold, and the value problem where the quantitative goal is to ensure the optimal mean-payoff value; in both cases ensuring the qualitative parity objective. The previous best-known algorithms for game graphs with n vertices, m edges, parity objectives with d priorities, and maximal absolute reward value W for mean-payoff objectives, are as follows: O(nd+1 . m . w) for the threshold problem, and O(nd+2 · m · W) for the value problem. Our main contributions are faster algorithms, and the running times of our algorithms are as follows: O(nd-1 · m ·W) for the threshold problem, and O(nd · m · W · log(n · W)) for the value problem. For mean-payoff parity objectives with two priorities, our algorithms match the best-known bounds of the algorithms for mean-payoff games (without conjunction with parity objectives). Our results are relevant in synthesis of reactive systems with both functional requirement (given as a qualitative objective) and performance requirement (given as a quantitative objective).},
author = {Chatterjee, Krishnendu and Henzinger, Monika and Svozil, Alexander},
booktitle = {Leibniz International Proceedings in Informatics},
isbn = {978-395977046-0},
location = {Aalborg, Denmark},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Faster algorithms for mean payoff parity games}},
doi = {10.4230/LIPIcs.MFCS.2017.39},
volume = {83},
year = {2017},
}
@inproceedings{553,
abstract = {We consider two player, zero-sum, finite-state concurrent reachability games, played for an infinite number of rounds, where in every round, each player simultaneously and independently of the other players chooses an action, whereafter the successor state is determined by a probability distribution given by the current state and the chosen actions. Player 1 wins iff a designated goal state is eventually visited. We are interested in the complexity of stationary strategies measured by their patience, which is defined as the inverse of the smallest non-zero probability employed. Our main results are as follows: We show that: (i) the optimal bound on the patience of optimal and -optimal strategies, for both players is doubly exponential; and (ii) even in games with a single non-absorbing state exponential (in the number of actions) patience is necessary. },
author = {Chatterjee, Krishnendu and Hansen, Kristofer and Ibsen-Jensen, Rasmus},
booktitle = {Leibniz International Proceedings in Informatics},
isbn = {978-395977046-0},
location = {Aalborg, Denmark},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Strategy complexity of concurrent safety games}},
doi = {10.4230/LIPIcs.MFCS.2017.55},
volume = {83},
year = {2017},
}
@misc{5455,
abstract = {A fundamental algorithmic problem at the heart of static analysis is Dyck reachability. The input is a graphwhere the edges are labeled with different types of opening and closing parentheses, and the reachabilityinformation is computed via paths whose parentheses are properly matched. We present new results for Dyckreachability problems with applications to alias analysis and data-dependence analysis. Our main contributions,that include improved upper bounds as well as lower bounds that establish optimality guarantees, are asfollows:First, we consider Dyck reachability on bidirected graphs, which is the standard way of performing field-sensitive points-to analysis. Given a bidirected graph withnnodes andmedges, we present: (i) an algorithmwith worst-case running timeO(m+n·α(n)), whereα(n)is the inverse Ackermann function, improving thepreviously knownO(n2)time bound; (ii) a matching lower bound that shows that our algorithm is optimalwrt to worst-case complexity; and (iii) an optimal average-case upper bound ofO(m)time, improving thepreviously knownO(m·logn)bound.Second, we consider the problem of context-sensitive data-dependence analysis, where the task is to obtainanalysis summaries of library code in the presence of callbacks. Our algorithm preprocesses libraries in almostlinear time, after which the contribution of the library in the complexity of the client analysis is only linear,and only wrt the number of call sites.Third, we prove that combinatorial algorithms for Dyck reachability on general graphs with truly sub-cubic bounds cannot be obtained without obtaining sub-cubic combinatorial algorithms for Boolean MatrixMultiplication, which is a long-standing open problem. Thus we establish that the existing combinatorialalgorithms for Dyck reachability are (conditionally) optimal for general graphs. We also show that the samehardness holds for graphs of constant treewidth.Finally, we provide a prototype implementation of our algorithms for both alias analysis and data-dependenceanalysis. Our experimental evaluation demonstrates that the new algorithms significantly outperform allexisting methods on the two problems, over real-world benchmarks.},
author = {Chatterjee, Krishnendu and Choudhary, Bhavya and Pavlogiannis, Andreas},
issn = {2664-1690},
pages = {37},
publisher = {IST Austria},
title = {{Optimal Dyck reachability for data-dependence and alias analysis}},
doi = {10.15479/AT:IST-2017-870-v1-1},
year = {2017},
}
@misc{5456,
abstract = {We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka stateless exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space of traces into equivalence classes (Mazurkiewicz partitioning), with the goal of exploring only few representative traces from each class.
We introduce a new equivalence on traces under sequential consistency semantics, which we call the observation equivalence. Two traces are observationally equivalent if every read event observes the same write event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new definition is data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called data-centric DPOR, based on the observation equivalence.
1. For acyclic architectures, our algorithm is guaranteed to explore exactly one representative trace from each observation class, while spending polynomial time per class. Hence, our algorithm is optimal wrt the observation equivalence, and in several cases explores exponentially fewer traces than any enumerative method based on the Mazurkiewicz equivalence.
2. For cyclic architectures, we consider an equivalence between traces which is finer than the observation equivalence; but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence.
Finally, we perform a basic experimental comparison between the existing Mazurkiewicz-based DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show a significant reduction in both running time and the number of explored equivalence classes.},
author = {Chalupa, Marek and Chatterjee, Krishnendu and Pavlogiannis, Andreas and Sinha, Nishant and Vaidya, Kapil},
issn = {2664-1690},
pages = {36},
publisher = {IST Austria},
title = {{Data-centric dynamic partial order reduction}},
doi = {10.15479/AT:IST-2017-872-v1-1},
year = {2017},
}
@misc{5559,
abstract = {Strong amplifiers of natural selection},
author = {Pavlogiannis, Andreas and Tkadlec, Josef and Chatterjee, Krishnendu and Nowak , Martin},
keywords = {natural selection},
publisher = {IST Austria},
title = {{Strong amplifiers of natural selection}},
doi = {10.15479/AT:ISTA:51},
year = {2017},
}
@inbook{625,
abstract = {In the analysis of reactive systems a quantitative objective assigns a real value to every trace of the system. The value decision problem for a quantitative objective requires a trace whose value is at least a given threshold, and the exact value decision problem requires a trace whose value is exactly the threshold. We compare the computational complexity of the value and exact value decision problems for classical quantitative objectives, such as sum, discounted sum, energy, and mean-payoff for two standard models of reactive systems, namely, graphs and graph games.},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A},
booktitle = {Models, Algorithms, Logics and Tools},
editor = {Aceto, Luca and Bacci, Giorgio and Ingólfsdóttir, Anna and Legay, Axel and Mardare, Radu},
issn = {03029743},
pages = {367 -- 381},
publisher = {Springer},
title = {{The cost of exactness in quantitative reachability}},
doi = {10.1007/978-3-319-63121-9_18},
volume = {10460},
year = {2017},
}
@inproceedings{628,
abstract = {We consider the problem of developing automated techniques for solving recurrence relations to aid the expected-runtime analysis of programs. The motivation is that several classical textbook algorithms have quite efficient expected-runtime complexity, whereas the corresponding worst-case bounds are either inefficient (e.g., Quick-Sort), or completely ineffective (e.g., Coupon-Collector). Since the main focus of expected-runtime analysis is to obtain efficient bounds, we consider bounds that are either logarithmic, linear or almost-linear (O(log n), O(n), O(n · log n), respectively, where n represents the input size). Our main contribution is an efficient (simple linear-time algorithm) sound approach for deriving such expected-runtime bounds for the analysis of recurrence relations induced by randomized algorithms. The experimental results show that our approach can efficiently derive asymptotically optimal expected-runtime bounds for recurrences of classical randomized algorithms, including Randomized-Search, Quick-Sort, Quick-Select, Coupon-Collector, where the worst-case bounds are either inefficient (such as linear as compared to logarithmic expected-runtime complexity, or quadratic as compared to linear or almost-linear expected-runtime complexity), or ineffective.},
author = {Chatterjee, Krishnendu and Fu, Hongfei and Murhekar, Aniket},
editor = {Majumdar, Rupak and Kunčak, Viktor},
isbn = {978-331963386-2},
location = {Heidelberg, Germany},
pages = {118 -- 139},
publisher = {Springer},
title = {{Automated recurrence analysis for almost linear expected runtime bounds}},
doi = {10.1007/978-3-319-63387-9_6},
volume = {10426},
year = {2017},
}
@inproceedings{645,
abstract = {Markov decision processes (MDPs) are standard models for probabilistic systems with non-deterministic behaviours. Long-run average rewards provide a mathematically elegant formalism for expressing long term performance. Value iteration (VI) is one of the simplest and most efficient algorithmic approaches to MDPs with other properties, such as reachability objectives. Unfortunately, a naive extension of VI does not work for MDPs with long-run average rewards, as there is no known stopping criterion. In this work our contributions are threefold. (1) We refute a conjecture related to stopping criteria for MDPs with long-run average rewards. (2) We present two practical algorithms for MDPs with long-run average rewards based on VI. First, we show that a combination of applying VI locally for each maximal end-component (MEC) and VI for reachability objectives can provide approximation guarantees. Second, extending the above approach with a simulation-guided on-demand variant of VI, we present an anytime algorithm that is able to deal with very large models. (3) Finally, we present experimental results showing that our methods significantly outperform the standard approaches on several benchmarks.},
author = {Ashok, Pranav and Chatterjee, Krishnendu and Daca, Przemyslaw and Kretinsky, Jan and Meggendorfer, Tobias},
editor = {Majumdar, Rupak and Kunčak, Viktor},
isbn = {978-331963386-2},
location = {Heidelberg, Germany},
pages = {201 -- 221},
publisher = {Springer},
title = {{Value iteration for long run average reward in markov decision processes}},
doi = {10.1007/978-3-319-63387-9_10},
volume = {10426},
year = {2017},
}
@inproceedings{6519,
abstract = {Graph games with omega-regular winning conditions provide a mathematical framework to analyze a wide range of problems in the analysis of reactive systems and programs (such as the synthesis of reactive systems, program repair, and the verification of branching time properties). Parity conditions are canonical forms to specify omega-regular winning conditions. Graph games with parity conditions are equivalent to mu-calculus model checking, and thus a very important algorithmic problem. Symbolic algorithms are of great significance because they provide scalable algorithms for the analysis of large finite-state systems, as well as algorithms for the analysis of infinite-state systems with finite quotient. A set-based symbolic algorithm uses the basic set operations and the one-step predecessor operators. We consider graph games with n vertices and parity conditions with c priorities (equivalently, a mu-calculus formula with c alternations of least and greatest fixed points). While many explicit algorithms exist for graph games with parity conditions, for set-based symbolic algorithms there are only two algorithms (notice that we use space to refer to the number of sets stored by a symbolic algorithm): (a) the basic algorithm that requires O(n^c) symbolic operations and linear space; and (b) an improved algorithm that requires O(n^{c/2+1}) symbolic operations but also O(n^{c/2+1}) space (i.e., exponential space). In this work we present two set-based symbolic algorithms for parity games: (a) our first algorithm requires O(n^{c/2+1}) symbolic operations and only requires linear space; and (b) developing on our first algorithm, we present an algorithm that requires O(n^{c/3+1}) symbolic operations and only linear space. We also present the first linear space set-based symbolic algorithm for parity games that requires at most a sub-exponential number of symbolic operations. },
author = {Chatterjee, Krishnendu and Dvorák, Wolfgang and Henzinger, Monika and Loitzenbauer, Veronika},
location = {Stockholm, Sweden},
publisher = {Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik},
title = {{Improved set-based symbolic algorithms for parity games}},
doi = {10.4230/LIPICS.CSL.2017.18},
volume = {82},
year = {2017},
}
@article{653,
abstract = {The extent of heterogeneity among driver gene mutations present in naturally occurring metastases - that is, treatment-naive metastatic disease - is largely unknown. To address this issue, we carried out 60× whole-genome sequencing of 26 metastases from four patients with pancreatic cancer. We found that identical mutations in known driver genes were present in every metastatic lesion for each patient studied. Passenger gene mutations, which do not have known or predicted functional consequences, accounted for all intratumoral heterogeneity. Even with respect to these passenger mutations, our analysis suggests that the genetic similarity among the founding cells of metastases was higher than that expected for any two cells randomly taken from a normal tissue. The uniformity of known driver gene mutations among metastases in the same patient has critical and encouraging implications for the success of future targeted therapies in advanced-stage disease.},
author = {Makohon Moore, Alvin and Zhang, Ming and Reiter, Johannes and Božić, Ivana and Allen, Benjamin and Kundu, Deepanjan and Chatterjee, Krishnendu and Wong, Fay and Jiao, Yuchen and Kohutek, Zachary and Hong, Jungeui and Attiyeh, Marc and Javier, Breanna and Wood, Laura and Hruban, Ralph and Nowak, Martin and Papadopoulos, Nickolas and Kinzler, Kenneth and Vogelstein, Bert and Iacobuzio Donahue, Christine},
issn = {10614036},
journal = {Nature Genetics},
number = {3},
pages = {358 -- 366},
publisher = {Nature Publishing Group},
title = {{Limited heterogeneity of known driver gene mutations among the metastases of individual patients with pancreatic cancer}},
doi = {10.1038/ng.3764},
volume = {49},
year = {2017},
}
@article{671,
abstract = {Humans routinely use conditionally cooperative strategies when interacting in repeated social dilemmas. They are more likely to cooperate if others cooperated before, and are ready to retaliate if others defected. To capture the emergence of reciprocity, most previous models consider subjects who can only choose from a restricted set of representative strategies, or who react to the outcome of the very last round only. As players memorize more rounds, the dimension of the strategy space increases exponentially. This increasing computational complexity renders simulations for individuals with higher cognitive abilities infeasible, especially if multiplayer interactions are taken into account. Here, we take an axiomatic approach instead. We propose several properties that a robust cooperative strategy for a repeated multiplayer dilemma should have. These properties naturally lead to a unique class of cooperative strategies, which contains the classical Win-Stay Lose-Shift rule as a special case. A comprehensive numerical analysis for the prisoner's dilemma and for the public goods game suggests that strategies of this class readily evolve across various memory-n spaces. Our results reveal that successful strategies depend not only on how cooperative others were in the past but also on the respective context of cooperation.},
author = {Hilbe, Christian and Martinez, Vaquero and Chatterjee, Krishnendu and Nowak, Martin},
issn = {00278424},
journal = {PNAS},
number = {18},
pages = {4715 -- 4720},
publisher = {National Academy of Sciences},
title = {{Memory-n strategies of direct reciprocity}},
doi = {10.1073/pnas.1621239114},
volume = {114},
year = {2017},
}
@article{681,
abstract = {Two-player games on graphs provide the theoretical framework for many important problems such as reactive synthesis. While the traditional study of two-player zero-sum games has been extended to multi-player games with several notions of equilibria, they are decidable only for perfect-information games, whereas several applications require imperfect-information. In this paper we propose a new notion of equilibria, called doomsday equilibria, which is a strategy profile where all players satisfy their own objective, and if any coalition of players deviates and violates even one of the players' objective, then the objective of every player is violated. We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information games, and for perfect-information games. We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games.},
author = {Chatterjee, Krishnendu and Doyen, Laurent and Filiot, Emmanuel and Raskin, Jean},
issn = {08905401},
journal = {Information and Computation},
pages = {296 -- 315},
publisher = {Elsevier},
title = {{Doomsday equilibria for omega-regular games}},
doi = {10.1016/j.ic.2016.10.012},
volume = {254},
year = {2017},
}
@article{684,
abstract = {We generalize winning conditions in two-player games by adding a structural acceptance condition called obligations. Obligations are orthogonal to the linear winning conditions that define whether a play is winning. Obligations are a declaration that player 0 can achieve a certain value from a configuration. If the obligation is met, the value of that configuration for player 0 is 1. We define the value in such games and show that obligation games are determined. For Markov chains with Borel objectives and obligations, and finite turn-based stochastic parity games with obligations we give an alternative and simpler characterization of the value function. Based on this simpler definition we show that the decision problem of winning finite turn-based stochastic parity games with obligations is in NP∩co-NP. We also show that obligation games provide a game framework for reasoning about p-automata. © 2017 The Association for Symbolic Logic.},
author = {Chatterjee, Krishnendu and Piterman, Nir},
issn = {Obligation blackwell games and p-automata},
journal = {Journal of Symbolic Logic},
number = {2},
pages = {420 -- 452},
publisher = {Cambridge University Press},
title = {{Obligation blackwell games and p-automata}},
doi = {10.1017/jsl.2016.71},
volume = {82},
year = {2017},
}
@article{699,
abstract = {In antagonistic symbioses, such as host–parasite interactions, one population’s success is the other’s loss. In mutualistic symbioses, such as division of labor, both parties can gain, but they might have different preferences over the possible mutualistic arrangements. The rates of evolution of the two populations in a symbiosis are important determinants of which population will be more successful: Faster evolution is thought to be favored in antagonistic symbioses (the “Red Queen effect”), but disfavored in certain mutualistic symbioses (the “Red King effect”). However, it remains unclear which biological parameters drive these effects. Here, we analyze the effects of the various determinants of evolutionary rate: generation time, mutation rate, population size, and the intensity of natural selection. Our main results hold for the case where mutation is infrequent. Slower evolution causes a long-term advantage in an important class of mutualistic interactions. Surprisingly, less intense selection is the strongest driver of this Red King effect, whereas relative mutation rates and generation times have little effect. In antagonistic interactions, faster evolution by any means is beneficial. Our results provide insight into the demographic evolution of symbionts. },
author = {Veller, Carl and Hayward, Laura and Nowak, Martin and Hilbe, Christian},
issn = {00278424},
journal = {PNAS},
number = {27},
pages = {E5396 -- E5405},
publisher = {National Academy of Sciences},
title = {{The red queen and king in finite populations}},
doi = {10.1073/pnas.1702020114},
volume = {114},
year = {2017},
}
@inproceedings{711,
abstract = {Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We therefore introduce and study bidirectional NWA that can process input words in both directions. First, we show that bidirectional NWA can express interesting quantitative properties that are not expressible by forward-only NWA. Second, for the fundamental decision problems of emptiness and universality, we establish decidability and complexity results for the new framework which match the best-known results for the special case of forward-only NWA. Thus, for NWA, the increased expressiveness of bidirectionality is achieved at no additional computational complexity. This is in stark contrast to the unweighted case, where bidirectional finite automata are no more expressive but exponentially more succinct than their forward-only counterparts.},
author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan},
issn = {18688969},
location = {Berlin, Germany},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Bidirectional nested weighted automata}},
doi = {10.4230/LIPIcs.CONCUR.2017.5},
volume = {85},
year = {2017},
}
@article{716,
abstract = {Two-player games on graphs are central in many problems in formal verification and program analysis, such as synthesis and verification of open systems. In this work, we consider solving recursive game graphs (or pushdown game graphs) that model the control flow of sequential programs with recursion.While pushdown games have been studied before with qualitative objectives-such as reachability and ?-regular objectives- in this work, we study for the first time such games with the most well-studied quantitative objective, the mean-payoff objective. In pushdown games, two types of strategies are relevant: (1) global strategies, which depend on the entire global history; and (2) modular strategies, which have only local memory and thus do not depend on the context of invocation but rather only on the history of the current invocation of the module. Our main results are as follows: (1) One-player pushdown games with mean-payoff objectives under global strategies are decidable in polynomial time. (2) Two-player pushdown games with mean-payoff objectives under global strategies are undecidable. (3) One-player pushdown games with mean-payoff objectives under modular strategies are NP-hard. (4) Two-player pushdown games with mean-payoff objectives under modular strategies can be solved in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives under modular strategies are NP-complete). We also establish the optimal strategy complexity by showing that global strategies for mean-payoff objectives require infinite memory even in one-player pushdown games and memoryless modular strategies are sufficient in two-player pushdown games. Finally, we also show that all the problems have the same complexity if the stack boundedness condition is added, where along with the mean-payoff objective the player must also ensure that the stack height is bounded.},
author = {Chatterjee, Krishnendu and Velner, Yaron},
issn = {00045411},
journal = {Journal of the ACM},
number = {5},
pages = {34},
publisher = {ACM},
title = {{The complexity of mean-payoff pushdown games}},
doi = {10.1145/3121408},
volume = {64},
year = {2017},
}
@article{717,
abstract = {We consider finite-state and recursive game graphs with multidimensional mean-payoff objectives. In recursive games two types of strategies are relevant: global strategies and modular strategies. Our contributions are: (1) We show that finite-state multidimensional mean-payoff games can be solved in polynomial time if the number of dimensions and the maximal absolute value of weights are fixed; whereas for arbitrary dimensions the problem is coNP-complete. (2) We show that one-player recursive games with multidimensional mean-payoff objectives can be solved in polynomial time. Both above algorithms are based on hyperplane separation technique. (3) For recursive games we show that under modular strategies the multidimensional problem is undecidable. We show that if the number of modules, exits, and the maximal absolute value of the weights are fixed, then one-dimensional recursive mean-payoff games under modular strategies can be solved in polynomial time, whereas for unbounded number of exits or modules the problem is NP-hard.},
author = {Chatterjee, Krishnendu and Velner, Yaron},
journal = {Journal of Computer and System Sciences},
pages = {236 -- 259},
publisher = {Academic Press},
title = {{Hyperplane separation technique for multidimensional mean-payoff games}},
doi = {10.1016/j.jcss.2017.04.005},
volume = {88},
year = {2017},
}
@article{719,
abstract = {The ubiquity of computation in modern machines and devices imposes a need to assert the correctness of their behavior. Especially in the case of safety-critical systems, their designers need to take measures that enforce their safe operation. Formal methods has emerged as a research field that addresses this challenge: by rigorously proving that all system executions adhere to their specifications, the correctness of an implementation under concern can be assured. To achieve this goal, a plethora of techniques are nowadays available, all of which are optimized for different system types and application domains.},
author = {Chatterjee, Krishnendu and Ehlers, Rüdiger},
issn = {00015903},
journal = {Acta Informatica},
number = {6},
pages = {543 -- 544},
publisher = {Springer},
title = {{Special issue: Synthesis and SYNT 2014}},
doi = {10.1007/s00236-017-0299-0},
volume = {54},
year = {2017},
}