@phdthesis{7196,
abstract = {In this thesis we study certain mathematical aspects of evolution. The two primary forces that drive an evolutionary process are mutation and selection. Mutation generates new variants in a population. Selection chooses among the variants depending on the reproductive rates of individuals. Evolutionary processes are intrinsically random – a new mutation that is initially present in the population at low frequency can go extinct, even if it confers a reproductive advantage. The overall rate of evolution is largely determined by two quantities: the probability that an invading advantageous mutation spreads through the population (called fixation probability) and the time until it does so (called fixation time). Both those quantities crucially depend not only on the strength of the invading mutation but also on the population structure. In this thesis, we aim to understand how the underlying population structure affects the overall rate of evolution. Specifically, we study population structures that increase the fixation probability of advantageous mutants (called amplifiers of selection). Broadly speaking, our results are of three different types: We present various strong amplifiers, we identify regimes under which only limited amplification is feasible, and we propose population structures that provide different tradeoffs between high fixation probability and short fixation time.},
author = {Tkadlec, Josef},
issn = {2663-337X},
pages = {144},
publisher = {IST Austria},
title = {{A role of graphs in evolutionary processes}},
doi = {10.15479/AT:ISTA:7196},
year = {2020},
}
@article{7343,
abstract = {Coinfections with multiple pathogens can result in complex within‐host dynamics affecting virulence and transmission. While multiple infections are intensively studied in solitary hosts, it is so far unresolved how social host interactions interfere with pathogen competition, and if this depends on coinfection diversity. We studied how the collective disease defences of ants – their social immunity – influence pathogen competition in coinfections of same or different fungal pathogen species. Social immunity reduced virulence for all pathogen combinations, but interfered with spore production only in different‐species coinfections. Here, it decreased overall pathogen sporulation success while increasing co‐sporulation on individual cadavers and maintaining a higher pathogen diversity at the community level. Mathematical modelling revealed that host sanitary care alone can modulate competitive outcomes between pathogens, giving advantage to fast‐germinating, thus less grooming‐sensitive ones. Host social interactions can hence modulate infection dynamics in coinfected group members, thereby altering pathogen communities at the host level and population level.},
author = {Milutinovic, Barbara and Stock, Miriam and Grasse, Anna V and Naderlinger, Elisabeth and Hilbe, Christian and Cremer, Sylvia},
issn = {1461-023X},
journal = {Ecology Letters},
publisher = {Wiley},
title = {{Social immunity modulates competition between coinfecting pathogens}},
doi = {10.1111/ele.13458},
year = {2020},
}
@article{7212,
abstract = {The fixation probability of a single mutant invading a population of residents is among the most widely-studied quantities in evolutionary dynamics. Amplifiers of natural selection are population structures that increase the fixation probability of advantageous mutants, compared to well-mixed populations. Extensive studies have shown that many amplifiers exist for the Birth-death Moran process, some of them substantially increasing the fixation probability or even guaranteeing fixation in the limit of large population size. On the other hand, no amplifiers are known for the death-Birth Moran process, and computer-assisted exhaustive searches have failed to discover amplification. In this work we resolve this disparity, by showing that any amplification under death-Birth updating is necessarily bounded and transient. Our boundedness result states that even if a population structure does amplify selection, the resulting fixation probability is close to that of the well-mixed population. Our transience result states that for any population structure there exists a threshold r⋆ such that the population structure ceases to amplify selection if the mutant fitness advantage r is larger than r⋆. Finally, we also extend the above results to δ-death-Birth updating, which is a combination of Birth-death and death-Birth updating. On the positive side, we identify population structures that maintain amplification for a wide range of values r and δ. These results demonstrate that amplification of natural selection depends on the specific mechanisms of the evolutionary process.},
author = {Tkadlec, Josef and Pavlogiannis, Andreas and Chatterjee, Krishnendu and Nowak, Martin A.},
issn = {15537358},
journal = {PLoS computational biology},
publisher = {PLoS},
title = {{Limits on amplifiers of natural selection under death-Birth updating}},
doi = {10.1371/journal.pcbi.1007494},
volume = {16},
year = {2020},
}
@article{6918,
abstract = {We consider the classic problem of Network Reliability. A network is given together with a source vertex, one or more target vertices, and probabilities assigned to each of the edges. Each edge of the network is operable with its associated probability and the problem is to determine the probability of having at least one source-to-target path that is entirely composed of operable edges. This problem is known to be NP-hard.
We provide a novel scalable algorithm to solve the Network Reliability problem when the treewidth of the underlying network is small. We also show our algorithm’s applicability for real-world transit networks that have small treewidth, including the metro networks of major cities, such as London and Tokyo. Our algorithm leverages tree decompositions to shrink the original graph into much smaller graphs, for which reliability can be efficiently and exactly computed using a brute force method. To the best of our knowledge, this is the first exact algorithm for Network Reliability that can scale to handle real-world instances of the problem.},
author = {Goharshady, Amir Kafshdar and Mohammadi, Fatemeh},
issn = {09518320},
journal = {Reliability Engineering and System Safety},
publisher = {Elsevier},
title = {{An efficient algorithm for computing network reliability in small treewidth}},
doi = {10.1016/j.ress.2019.106665},
volume = {193},
year = {2020},
}
@inproceedings{7346,
abstract = {The Price of Anarchy (PoA) is a well-established game-theoretic concept to shed light on coordination issues arising in open distributed systems. Leaving agents to selfishly optimize comes with the risk of ending up in sub-optimal states (in terms of performance and/or costs), compared to a centralized system design. However, the PoA relies on strong assumptions about agents' rationality (e.g., resources and information) and interactions, whereas in many distributed systems agents interact locally with bounded resources. They do so repeatedly over time (in contrast to "one-shot games"), and their strategies may evolve. Using a more realistic evolutionary game model, this paper introduces a realized evolutionary Price of Anarchy (ePoA). The ePoA allows an exploration of equilibrium selection in dynamic distributed systems with multiple equilibria, based on local interactions of simple memoryless agents. Considering a fundamental game related to virus propagation on networks, we present analytical bounds on the ePoA in basic network topologies and for different strategy update dynamics. In particular, deriving stationary distributions of the stochastic evolutionary process, we find that the Nash equilibria are not always the most abundant states, and that different processes can feature significant off-equilibrium behavior, leading to a significantly higher ePoA compared to the PoA studied traditionally in the literature. },
author = {Schmid, Laura and Chatterjee, Krishnendu and Schmid, Stefan},
booktitle = {Proceedings of the 23rd International Conference on Principles of Distributed Systems},
location = {Neuchâtel, Switzerland},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{The evolutionary price of anarchy: Locally bounded agents in a dynamic virus game}},
doi = {10.4230/LIPIcs.OPODIS.2019.21},
volume = {153},
year = {2020},
}
@inproceedings{6490,
abstract = {Smart contracts are programs that are stored and executed on the Blockchain and can receive, manage and transfer money (cryptocurrency units). Two important problems regarding smart contracts are formal analysis and compiler optimization. Formal analysis is extremely important, because smart contracts hold funds worth billions of dollars and their code is immutable after deployment. Hence, an undetected bug can cause significant financial losses. Compiler optimization is also crucial, because every action of a smart contract has to be executed by every node in the Blockchain network. Therefore, optimizations in compiling smart contracts can lead to significant savings in computation, time and energy.
Two classical approaches in program analysis and compiler optimization are intraprocedural and interprocedural analysis. In intraprocedural analysis, each function is analyzed separately, while interprocedural analysis considers the entire program. In both cases, the analyses are usually reduced to graph problems over the control flow graph (CFG) of the program. These graph problems are often computationally expensive. Hence, there has been ample research on exploiting structural properties of CFGs for efficient algorithms. One such well-studied property is the treewidth, which is a measure of tree-likeness of graphs. It is known that intraprocedural CFGs of structured programs have treewidth at most 6, whereas the interprocedural treewidth cannot be bounded. This result has been used as a basis for many efficient intraprocedural analyses.
In this paper, we explore the idea of exploiting the treewidth of smart contracts for formal analysis and compiler optimization. First, similar to classical programs, we show that the intraprocedural treewidth of structured Solidity and Vyper smart contracts is at most 9. Second, for global analysis, we prove that the interprocedural treewidth of structured smart contracts is bounded by 10 and, in sharp contrast with classical programs, treewidth-based algorithms can be easily applied for interprocedural analysis. Finally, we supplement our theoretical results with experiments using a tool we implemented for computing treewidth of smart contracts and show that the treewidth is much lower in practice. We use 36,764 real-world Ethereum smart contracts as benchmarks and find that they have an average treewidth of at most 3.35 for the intraprocedural case and 3.65 for the interprocedural case.
},
author = {Chatterjee, Krishnendu and Goharshady, Amir Kafshdar and Goharshady, Ehsan Kafshdar},
booktitle = {Proceedings of the 34th ACM Symposium on Applied Computing},
isbn = {9781450359337},
location = {Limassol, Cyprus},
pages = {400--408},
publisher = {ACM},
title = {{The treewidth of smart contracts}},
doi = {10.1145/3297280.3297322},
volume = {Part F147772},
year = {2019},
}
@inproceedings{6887,
abstract = {The fundamental model-checking problem, given as input a model and a specification, asks for the algorithmic verification of whether the model satisfies the specification. Two classical models for reactive systems are graphs and Markov decision processes (MDPs). A basic specification formalism in the verification of reactive systems is the strong fairness (aka Streett) objective, where given different types of requests and corresponding grants, the requirement is that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often. All omega-regular objectives can be expressed as Streett objectives and hence they are canonical in verification. Consider graphs/MDPs with n vertices, m edges, and a Streett objectives with k pairs, and let b denote the size of the description of the Streett objective for the sets of requests and grants. The current best-known algorithm for the problem requires time O(min(n^2, m sqrt{m log n}) + b log n). In this work we present randomized near-linear time algorithms, with expected running time O~(m + b), where the O~ notation hides poly-log factors. Our randomized algorithms are near-linear in the size of the input, and hence optimal up to poly-log factors. },
author = {Chatterjee, Krishnendu and Dvorák, Wolfgang and Henzinger, Monika and Svozil, Alexander},
booktitle = {Leibniz International Proceedings in Informatics},
location = {Amsterdam, Netherlands},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Near-linear time algorithms for Streett objectives in graphs and MDPs}},
doi = {10.4230/LIPICS.CONCUR.2019.7},
volume = {140},
year = {2019},
}
@inproceedings{7183,
abstract = {A probabilistic vector addition system with states (pVASS) is a finite state Markov process augmented with non-negative integer counters that can be incremented or decremented during each state transition, blocking any behaviour that would cause a counter to decrease below zero. The pVASS can be used as abstractions of probabilistic programs with many decidable properties. The use of pVASS as abstractions requires the presence of nondeterminism in the model. In this paper, we develop techniques for checking fast termination of pVASS with nondeterminism. That is, for every initial configuration of size n, we consider the worst expected number of transitions needed to reach a configuration with some counter negative (the expected termination time). We show that the problem whether the asymptotic expected termination time is linear is decidable in polynomial time for a certain natural class of pVASS with nondeterminism. Furthermore, we show the following dichotomy: if the asymptotic expected termination time is not linear, then it is at least quadratic, i.e., in Ω(n2).},
author = {Brázdil, Tomás and Chatterjee, Krishnendu and Kucera, Antonín and Novotný, Petr and Velan, Dominik},
booktitle = {International Symposium on Automated Technology for Verification and Analysis},
isbn = {9783030317836},
issn = {16113349},
location = {Taipei, Taiwan},
pages = {462--478},
publisher = {Springer Nature},
title = {{Deciding fast termination for probabilistic VASS with nondeterminism}},
doi = {10.1007/978-3-030-31784-3_27},
volume = {11781},
year = {2019},
}
@article{7210,
abstract = {The rate of biological evolution depends on the fixation probability and on the fixation time of new mutants. Intensive research has focused on identifying population structures that augment the fixation probability of advantageous mutants. But these amplifiers of natural selection typically increase fixation time. Here we study population structures that achieve a tradeoff between fixation probability and time. First, we show that no amplifiers can have an asymptotically lower absorption time than the well-mixed population. Then we design population structures that substantially augment the fixation probability with just a minor increase in fixation time. Finally, we show that those structures enable higher effective rate of evolution than the well-mixed population provided that the rate of generating advantageous mutants is relatively low. Our work sheds light on how population structure affects the rate of evolution. Moreover, our structures could be useful for lab-based, medical, or industrial applications of evolutionary optimization.},
author = {Tkadlec, Josef and Pavlogiannis, Andreas and Chatterjee, Krishnendu and Nowak, Martin A.},
issn = {2399-3642},
journal = {Communications Biology},
publisher = {Springer Nature},
title = {{Population structure determines the tradeoff between fixation probability and fixation time}},
doi = {10.1038/s42003-019-0373-y},
volume = {2},
year = {2019},
}
@inproceedings{5948,
abstract = {We study the termination problem for nondeterministic probabilistic programs. We consider the bounded termination problem that asks whether the supremum of the expected termination time over all schedulers is bounded. First, we show that ranking supermartingales (RSMs) are both sound and complete for proving bounded termination over nondeterministic probabilistic programs. For nondeterministic probabilistic programs a previous result claimed that RSMs are not complete for bounded termination, whereas our result corrects the previous flaw and establishes completeness with a rigorous proof. Second, we present the first sound approach to establish lower bounds on expected termination time through RSMs.},
author = {Fu, Hongfei and Chatterjee, Krishnendu},
booktitle = {International Conference on Verification, Model Checking, and Abstract Interpretation},
location = {Cascais, Portugal},
pages = {468--490},
publisher = {Springer Nature},
title = {{Termination of nondeterministic probabilistic programs}},
doi = {10.1007/978-3-030-11245-5_22},
volume = {11388},
year = {2019},
}
@article{7158,
abstract = {
Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, and so on. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, and so on. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is fixed as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in an important algorithmic distinction between the resource usage of the one-time preprocessing vs for each individual query. The second aspect we consider is that the control flow graphs for most programs have constant treewidth.
Our main contributions are simple and implementable algorithms that support multiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing but can answer subsequent queries significantly faster as compared to the current algorithmic solutions for interprocedural dataflow analysis. We have also implemented our algorithms and evaluated their performance for performing on-demand interprocedural dataflow analysis on various domains, such as for live variable analysis and reaching definitions, on a standard benchmark set. Our experimental results align with our theoretical statements and show that after a lightweight preprocessing, on-demand queries are answered much faster than the standard existing algorithmic approaches.
},
author = {Chatterjee, Krishnendu and Goharshady, Amir Kafshdar and Goyal, Prateesh and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas},
issn = {0164-0925},
journal = {ACM Transactions on Programming Languages and Systems},
number = {4},
publisher = {ACM},
title = {{Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth}},
doi = {10.1145/3363525},
volume = {41},
year = {2019},
}
@article{7014,
abstract = {We study the problem of developing efficient approaches for proving
worst-case bounds of non-deterministic recursive programs. Ranking functions
are sound and complete for proving termination and worst-case bounds of
nonrecursive programs. First, we apply ranking functions to recursion,
resulting in measure functions. We show that measure functions provide a sound
and complete approach to prove worst-case bounds of non-deterministic recursive
programs. Our second contribution is the synthesis of measure functions in
nonpolynomial forms. We show that non-polynomial measure functions with
logarithm and exponentiation can be synthesized through abstraction of
logarithmic or exponentiation terms, Farkas' Lemma, and Handelman's Theorem
using linear programming. While previous methods obtain worst-case polynomial
bounds, our approach can synthesize bounds of the form $\mathcal{O}(n\log n)$
as well as $\mathcal{O}(n^r)$ where $r$ is not an integer. We present
experimental results to demonstrate that our approach can obtain efficiently
worst-case bounds of classical recursive algorithms such as (i) Merge-Sort, the
divide-and-conquer algorithm for the Closest-Pair problem, where we obtain
$\mathcal{O}(n \log n)$ worst-case bound, and (ii) Karatsuba's algorithm for
polynomial multiplication and Strassen's algorithm for matrix multiplication,
where we obtain $\mathcal{O}(n^r)$ bound such that $r$ is not an integer and
close to the best-known bounds for the respective algorithms.},
author = {Chatterjee, Krishnendu and Fu, Hongfei and Goharshady, Amir Kafshdar},
journal = {ACM Transactions on Programming Languages and Systems},
number = {4},
publisher = {ACM},
title = {{Non-polynomial worst-case analysis of recursive programs}},
doi = {10.1145/3339984},
volume = {41},
year = {2019},
}
@inproceedings{6884,
abstract = {In two-player games on graphs, the players move a token through a graph to produce a finite or infinite path, which determines the qualitative winner or quantitative payoff of the game. We study bidding games in which the players bid for the right to move the token. Several bidding rules were studied previously. In Richman bidding, in each round, the players simultaneously submit bids, and the higher bidder moves the token and pays the other player. Poorman bidding is similar except that the winner of the bidding pays the "bank" rather than the other player. Taxman bidding spans the spectrum between Richman and poorman bidding. They are parameterized by a constant tau in [0,1]: portion tau of the winning bid is paid to the other player, and portion 1-tau to the bank. While finite-duration (reachability) taxman games have been studied before, we present, for the first time, results on infinite-duration taxman games. It was previously shown that both Richman and poorman infinite-duration games with qualitative objectives reduce to reachability games, and we show a similar result here. Our most interesting results concern quantitative taxman games, namely mean-payoff games, where poorman and Richman bidding differ significantly. A central quantity in these games is the ratio between the two players' initial budgets. While in poorman mean-payoff games, the optimal payoff of a player depends on the initial ratio, in Richman bidding, the payoff depends only on the structure of the game. In both games the optimal payoffs can be found using (different) probabilistic connections with random-turn games in which in each turn, instead of bidding, a coin is tossed to determine which player moves. While the value with Richman bidding equals the value of a random-turn game with an un-biased coin, with poorman bidding, the bias in the coin is the initial ratio of the budgets. We give a complete classification of mean-payoff taxman games that is based on a probabilistic connection: the value of a taxman bidding game with parameter tau and initial ratio r, equals the value of a random-turn game that uses a coin with bias F(tau, r) = (r+tau * (1-r))/(1+tau). Thus, we show that Richman bidding is the exception; namely, for every tau <1, the value of the game depends on the initial ratio. Our proof technique simplifies and unifies the previous proof techniques for both Richman and poorman bidding. },
author = {Avni, Guy and Henzinger, Thomas A and Zikelic, Dorde},
location = {Aachen, Germany},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Bidding mechanisms in graph games}},
doi = {10.4230/LIPICS.MFCS.2019.11},
volume = {138},
year = {2019},
}
@inproceedings{6889,
abstract = {We study Markov decision processes and turn-based stochastic games with parity conditions. There are three qualitative winning criteria, namely, sure winning, which requires all paths to satisfy the condition, almost-sure winning, which requires the condition to be satisfied with probability 1, and limit-sure winning, which requires the condition to be satisfied with probability arbitrarily close to 1. We study the combination of two of these criteria for parity conditions, e.g., there are two parity conditions one of which must be won surely, and the other almost-surely. The problem has been studied recently by Berthon et al. for MDPs with combination of sure and almost-sure winning, under infinite-memory strategies, and the problem has been established to be in NP cap co-NP. Even in MDPs there is a difference between finite-memory and infinite-memory strategies. Our main results for combination of sure and almost-sure winning are as follows: (a) we show that for MDPs with finite-memory strategies the problem is in NP cap co-NP; (b) we show that for turn-based stochastic games the problem is co-NP-complete, both for finite-memory and infinite-memory strategies; and (c) we present algorithmic results for the finite-memory case, both for MDPs and turn-based stochastic games, by reduction to non-stochastic parity games. In addition we show that all the above complexity results also carry over to combination of sure and limit-sure winning, and results for all other combinations can be derived from existing results in the literature. Thus we present a complete picture for the study of combinations of two qualitative winning criteria for parity conditions in MDPs and turn-based stochastic games. },
author = {Chatterjee, Krishnendu and Piterman, Nir},
location = {Amsterdam, Netherlands},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Combinations of Qualitative Winning for Stochastic Parity Games}},
doi = {10.4230/LIPICS.CONCUR.2019.6},
volume = {140},
year = {2019},
}
@inproceedings{6942,
abstract = {Graph games and Markov decision processes (MDPs) are standard models in reactive synthesis and verification of probabilistic systems with nondeterminism. The class of 𝜔 -regular winning conditions; e.g., safety, reachability, liveness, parity conditions; provides a robust and expressive specification formalism for properties that arise in analysis of reactive systems. The resolutions of nondeterminism in games and MDPs are represented as strategies, and we consider succinct representation of such strategies. The decision-tree data structure from machine learning retains the flavor of decisions of strategies and allows entropy-based minimization to obtain succinct trees. However, in contrast to traditional machine-learning problems where small errors are allowed, for winning strategies in graph games and MDPs no error is allowed, and the decision tree must represent the entire strategy. In this work we propose decision trees with linear classifiers for representation of strategies in graph games and MDPs. We have implemented strategy representation using this data structure and we present experimental results for problems on graph games and MDPs, which show that this new data structure presents a much more efficient strategy representation as compared to standard decision trees.},
author = {Ashok, Pranav and Brázdil, Tomáš and Chatterjee, Krishnendu and Křetínský, Jan and Lampert, Christoph and Toman, Viktor},
booktitle = {16th International Conference on Quantitative Evaluation of Systems},
isbn = {9783030302801},
issn = {0302-9743},
location = {Glasgow, United Kingdom},
pages = {109--128},
publisher = {Springer Nature},
title = {{Strategy representation by decision trees with linear classifiers}},
doi = {10.1007/978-3-030-30281-8_7},
volume = {11785},
year = {2019},
}
@inproceedings{7402,
abstract = {Graph planning gives rise to fundamental algorithmic questions such as shortest path, traveling salesman problem, etc. A classical problem in discrete planning is to consider a weighted graph and construct a path that maximizes the sum of weights for a given time horizon T. However, in many scenarios, the time horizon is not fixed, but the stopping time is chosen according to some distribution such that the expected stopping time is T. If the stopping time distribution is not known, then to ensure robustness, the distribution is chosen by an adversary, to represent the worst-case scenario. A stationary plan for every vertex always chooses the same outgoing edge. For fixed horizon or fixed stopping-time distribution, stationary plans are not sufficient for optimality. Quite surprisingly we show that when an adversary chooses the stopping-time distribution with expected stopping time T, then stationary plans are sufficient. While computing optimal stationary plans for fixed horizon is NP-complete, we show that computing optimal stationary plans under adversarial stopping-time distribution can be achieved in polynomial time. Consequently, our polynomial-time algorithm for adversarial stopping time also computes an optimal plan among all possible plans.},
author = {Chatterjee, Krishnendu and Doyen, Laurent},
booktitle = {34th Annual ACM/IEEE Symposium on Logic in Computer Science},
isbn = {9781728136080},
location = {Vancouver, BC, Canada},
pages = {1--13},
publisher = {IEEE},
title = {{Graph planning with expected finite horizon}},
doi = {10.1109/lics.2019.8785706},
year = {2019},
}
@inproceedings{6175,
abstract = {We consider the problem of expected cost analysis over nondeterministic probabilistic programs,
which aims at automated methods for analyzing the resource-usage of such programs.
Previous approaches for this problem could only handle nonnegative bounded costs.
However, in many scenarios, such as queuing networks or analysis of cryptocurrency protocols,
both positive and negative costs are necessary and the costs are unbounded as well.
In this work, we present a sound and efficient approach to obtain polynomial bounds on the
expected accumulated cost of nondeterministic probabilistic programs.
Our approach can handle (a) general positive and negative costs with bounded updates in
variables; and (b) nonnegative costs with general updates to variables.
We show that several natural examples which could not be
handled by previous approaches are captured in our framework.
Moreover, our approach leads to an efficient polynomial-time algorithm, while no
previous approach for cost analysis of probabilistic programs could guarantee polynomial runtime.
Finally, we show the effectiveness of our approach using experimental results on a variety of programs for which we efficiently synthesize tight resource-usage bounds.},
author = {Wang, Peixin and Fu, Hongfei and Goharshady, Amir Kafshdar and Chatterjee, Krishnendu and Qin, Xudong and Shi, Wenjun},
booktitle = {PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation},
keyword = {Program Cost Analysis, Program Termination, Probabilistic Programs, Martingales},
location = {Phoenix, AZ, United States},
pages = {204--220},
publisher = {Association for Computing Machinery},
title = {{Cost analysis of nondeterministic probabilistic programs}},
doi = {10.1145/3314221.3314581},
year = {2019},
}
@article{6380,
abstract = {There is a huge gap between the speeds of modern caches and main memories, and therefore cache misses account for a considerable loss of efficiency in programs. The predominant technique to address this issue has been Data Packing: data elements that are frequently accessed within time proximity are packed into the same cache block, thereby minimizing accesses to the main memory. We consider the algorithmic problem of Data Packing on a two-level memory system. Given a reference sequence R of accesses to data elements, the task is to partition the elements into cache blocks such that the number of cache misses on R is minimized. The problem is notoriously difficult: it is NP-hard even when the cache has size 1, and is hard to approximate for any cache size larger than 4. Therefore, all existing techniques for Data Packing are based on heuristics and lack theoretical guarantees. In this work, we present the first positive theoretical results for Data Packing, along with new and stronger negative results. We consider the problem under the lens of the underlying access hypergraphs, which are hypergraphs of affinities between the data elements, where the order of an access hypergraph corresponds to the size of the affinity group. We study the problem parameterized by the treewidth of access hypergraphs, which is a standard notion in graph theory to measure the closeness of a graph to a tree. Our main results are as follows: We show there is a number q* depending on the cache parameters such that (a) if the access hypergraph of order q* has constant treewidth, then there is a linear-time algorithm for Data Packing; (b)the Data Packing problem remains NP-hard even if the access hypergraph of order q*-1 has constant treewidth. Thus, we establish a fine-grained dichotomy depending on a single parameter, namely, the highest order among access hypegraphs that have constant treewidth; and establish the optimal value q* of this parameter. Finally, we present an experimental evaluation of a prototype implementation of our algorithm. Our results demonstrate that, in practice, access hypergraphs of many commonly-used algorithms have small treewidth. We compare our approach with several state-of-the-art heuristic-based algorithms and show that our algorithm leads to significantly fewer cache-misses. },
author = {Chatterjee, Krishnendu and Goharshady, Amir Kafshdar and Okati, Nastaran and Pavlogiannis, Andreas},
issn = {2475-1421},
journal = {Proceedings of the ACM on Programming Languages},
number = {POPL},
publisher = {ACM},
title = {{Efficient parameterized algorithms for data packing}},
doi = {10.1145/3290366},
volume = {3},
year = {2019},
}
@inproceedings{6462,
abstract = {A controller is a device that interacts with a plant. At each time point,it reads the plant’s state and issues commands with the goal that the plant oper-ates optimally. Constructing optimal controllers is a fundamental and challengingproblem. Machine learning techniques have recently been successfully applied totrain controllers, yet they have limitations. Learned controllers are monolithic andhard to reason about. In particular, it is difficult to add features without retraining,to guarantee any level of performance, and to achieve acceptable performancewhen encountering untrained scenarios. These limitations can be addressed bydeploying quantitative run-timeshieldsthat serve as a proxy for the controller.At each time point, the shield reads the command issued by the controller andmay choose to alter it before passing it on to the plant. We show how optimalshields that interfere as little as possible while guaranteeing a desired level ofcontroller performance, can be generated systematically and automatically usingreactive synthesis. First, we abstract the plant by building a stochastic model.Second, we consider the learned controller to be a black box. Third, we mea-surecontroller performanceandshield interferenceby two quantitative run-timemeasures that are formally defined using weighted automata. Then, the problemof constructing a shield that guarantees maximal performance with minimal inter-ference is the problem of finding an optimal strategy in a stochastic2-player game“controller versus shield” played on the abstract state space of the plant with aquantitative objective obtained from combining the performance and interferencemeasures. We illustrate the effectiveness of our approach by automatically con-structing lightweight shields for learned traffic-light controllers in various roadnetworks. The shields we generate avoid liveness bugs, improve controller per-formance in untrained and changing traffic situations, and add features to learnedcontrollers, such as giving priority to emergency vehicles.},
author = {Avni, Guy and Bloem, Roderick and Chatterjee, Krishnendu and Henzinger, Thomas A and Konighofer, Bettina and Pranger, Stefan},
booktitle = {31st International Conference on Computer-Aided Verification},
isbn = {9783030255398},
issn = {0302-9743},
location = {New York, NY, United States},
pages = {630--649},
publisher = {Springer},
title = {{Run-time optimization for learned controllers through quantitative games}},
doi = {10.1007/978-3-030-25540-4_36},
volume = {11561},
year = {2019},
}
@inproceedings{6056,
abstract = {In today's programmable blockchains, smart contracts are limited to being deterministic and non-probabilistic. This lack of randomness is a consequential limitation, given that a wide variety of real-world financial contracts, such as casino games and lotteries, depend entirely on randomness. As a result, several ad-hoc random number generation approaches have been developed to be used in smart contracts. These include ideas such as using an oracle or relying on the block hash. However, these approaches are manipulatable, i.e. their output can be tampered with by parties who might not be neutral, such as the owner of the oracle or the miners.We propose a novel game-theoretic approach for generating provably unmanipulatable pseudorandom numbers on the blockchain. Our approach allows smart contracts to access a trustworthy source of randomness that does not rely on potentially compromised miners or oracles, hence enabling the creation of a new generation of smart contracts that are not limited to being non-probabilistic and can be drawn from the much more general class of probabilistic programs.},
author = {Chatterjee, Krishnendu and Goharshady, Amir Kafshdar and Pourdamghani, Arash},
booktitle = {IEEE International Conference on Blockchain and Cryptocurrency},
location = {Seoul, Korea},
publisher = {IEEE},
title = {{Probabilistic smart contracts: Secure randomness on the blockchain}},
doi = {10.1109/BLOC.2019.8751326},
year = {2019},
}