@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{25,
abstract = {Partially observable Markov decision processes (POMDPs) are the standard models for planning under uncertainty with both finite and infinite horizon. Besides the well-known discounted-sum objective, indefinite-horizon objective (aka Goal-POMDPs) is another classical objective for POMDPs. In this case, given a set of target states and a positive cost for each transition, the optimization objective is to minimize the expected total cost until a target state is reached. In the literature, RTDP-Bel or heuristic search value iteration (HSVI) have been used for solving Goal-POMDPs. Neither of these algorithms has theoretical convergence guarantees, and HSVI may even fail to terminate its trials. We give the following contributions: (1) We discuss the challenges introduced in Goal-POMDPs and illustrate how they prevent the original HSVI from converging. (2) We present a novel algorithm inspired by HSVI, termed Goal-HSVI, and show that our algorithm has convergence guarantees. (3) We show that Goal-HSVI outperforms RTDP-Bel on a set of well-known examples.},
author = {Horák, Karel and Bošanský, Branislav and Chatterjee, Krishnendu},
booktitle = {Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence},
location = {Stockholm, Sweden},
pages = {4764 -- 4770},
publisher = {IJCAI},
title = {{Goal-HSVI: Heuristic search value iteration for goal-POMDPs}},
doi = {10.24963/ijcai.2018/662},
volume = {2018-July},
year = {2018},
}
@inproceedings{141,
abstract = {Given a model and a specification, the fundamental model-checking problem asks for algorithmic verification of whether the model satisfies the specification. We consider graphs and Markov decision processes (MDPs), which are fundamental models for reactive systems. One of the very basic specifications that arise in verification of reactive systems is the strong fairness (aka Streett) objective. Given different types of requests and corresponding grants, the objective requires that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often. All ω -regular objectives can be expressed as Streett objectives and hence they are canonical in verification. To handle the state-space explosion, symbolic algorithms are required that operate on a succinct implicit representation of the system rather than explicitly accessing the system. While explicit algorithms for graphs and MDPs with Streett objectives have been widely studied, there has been no improvement of the basic symbolic algorithms. The worst-case numbers of symbolic steps required for the basic symbolic algorithms are as follows: quadratic for graphs and cubic for MDPs. In this work we present the first sub-quadratic symbolic algorithm for graphs with Streett objectives, and our algorithm is sub-quadratic even for MDPs. Based on our algorithmic insights we present an implementation of the new symbolic approach and show that it improves the existing approach on several academic benchmark examples.},
author = {Chatterjee, Krishnendu and Henzinger, Monika and Loitzenbauer, Veronika and Oraee, Simin and Toman, Viktor},
location = {Oxford, United Kingdom},
pages = {178--197},
publisher = {Springer},
title = {{Symbolic algorithms for graphs and Markov decision processes with fairness objectives}},
doi = {10.1007/978-3-319-96142-2_13},
volume = {10982},
year = {2018},
}
@article{2,
abstract = {Indirect reciprocity explores how humans act when their reputation is at stake, and which social norms they use to assess the actions of others. A crucial question in indirect reciprocity is which social norms can maintain stable cooperation in a society. Past research has highlighted eight such norms, called “leading-eight” strategies. This past research, however, is based on the assumption that all relevant information about other population members is publicly available and that everyone agrees on who is good or bad. Instead, here we explore the reputation dynamics when information is private and noisy. We show that under these conditions, most leading-eight strategies fail to evolve. Those leading-eight strategies that do evolve are unable to sustain full cooperation.Indirect reciprocity is a mechanism for cooperation based on shared moral systems and individual reputations. It assumes that members of a community routinely observe and assess each other and that they use this information to decide who is good or bad, and who deserves cooperation. When information is transmitted publicly, such that all community members agree on each other’s reputation, previous research has highlighted eight crucial moral systems. These “leading-eight” strategies can maintain cooperation and resist invasion by defectors. However, in real populations individuals often hold their own private views of others. Once two individuals disagree about their opinion of some third party, they may also see its subsequent actions in a different light. Their opinions may further diverge over time. Herein, we explore indirect reciprocity when information transmission is private and noisy. We find that in the presence of perception errors, most leading-eight strategies cease to be stable. Even if a leading-eight strategy evolves, cooperation rates may drop considerably when errors are common. Our research highlights the role of reliable information and synchronized reputations to maintain stable moral systems.},
author = {Hilbe, Christian and Schmid, Laura and Tkadlec, Josef and Chatterjee, Krishnendu and Nowak, Martin},
journal = {PNAS},
number = {48},
pages = {12241--12246},
publisher = {National Academy of Sciences},
title = {{Indirect reciprocity with private noisy and incomplete information}},
doi = {10.1073/pnas.1810565115 },
volume = {115},
year = {2018},
}
@inproceedings{297,
abstract = {Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with ω -regular winning conditions, specified as parity objectives, which can express properties such as safety, liveness, fairness, are the basic framework for verification and synthesis of reactive systems. The decisions for a player at various states of the graph game are represented as strategies. While the algorithmic problem for solving graph games with parity objectives has been widely studied, the most prominent data-structure for strategy representation in graph games has been binary decision diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain the inherent flavor of the decisions of strategies, and are notoriously hard to minimize to obtain succinct representation. In this work we propose decision trees for strategy representation in graph games. Decision trees retain the flavor of decisions of strategies and allow entropy-based minimization to obtain succinct trees. However, decision trees work in settings (e.g., probabilistic models) where errors are allowed, and overfitting of data is typically avoided. In contrast, for strategies in graph games no error is allowed, and the decision tree must represent the entire strategy. We develop new techniques to extend decision trees to overcome the above obstacles, while retaining the entropy-based techniques to obtain succinct trees. We have implemented our techniques to extend the existing decision tree solvers. We present experimental results for problems in reactive synthesis to show that decision trees provide a much more efficient data-structure for strategy representation as compared to BDDs.},
author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Kretinsky, Jan and Toman, Viktor},
location = {Thessaloniki, Greece},
pages = {385 -- 407},
publisher = {Springer},
title = {{Strategy representation by decision trees in reactive synthesis}},
doi = {10.1007/978-3-319-89960-2_21},
volume = {10805},
year = {2018},
}
@article{293,
abstract = {People sometimes make their admirable deeds and accomplishments hard to spot, such as by giving anonymously or avoiding bragging. Such ‘buried’ signals are hard to reconcile with standard models of signalling or indirect reciprocity, which motivate costly pro-social behaviour by reputational gains. To explain these phenomena, we design a simple game theory model, which we call the signal-burying game. This game has the feature that senders can bury their signal by deliberately reducing the probability of the signal being observed. If the signal is observed, however, it is identified as having been buried. We show under which conditions buried signals can be maintained, using static equilibrium concepts and calculations of the evolutionary dynamics. We apply our analysis to shed light on a number of otherwise puzzling social phenomena, including modesty, anonymous donations, subtlety in art and fashion, and overeagerness.},
author = {Hoffman, Moshe and Hilbe, Christian and Nowak, Martin},
journal = {Nature Human Behaviour},
pages = {397 -- 404},
publisher = {Nature Publishing Group},
title = {{The signal-burying game can explain why we obscure positive traits and good deeds}},
doi = {10.1038/s41562-018-0354-z},
volume = {2},
year = {2018},
}
@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},
}
@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},
}
@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{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},
}
@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},
}
@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},
}
@article{744,
abstract = {In evolutionary game theory interactions between individuals are often assumed obligatory. However, in many real-life situations, individuals can decide to opt out of an interaction depending on the information they have about the opponent. We consider a simple evolutionary game theoretic model to study such a scenario, where at each encounter between two individuals the type of the opponent (cooperator/defector) is known with some probability, and where each individual either accepts or opts out of the interaction. If the type of the opponent is unknown, a trustful individual accepts the interaction, whereas a suspicious individual opts out of the interaction. If either of the two individuals opt out both individuals remain without an interaction. We show that in the prisoners dilemma optional interactions along with suspicious behaviour facilitates the emergence of trustful cooperation.},
author = {Priklopil, Tadeas and Chatterjee, Krishnendu and Nowak, Martin},
issn = {00225193},
journal = { Journal of Theoretical Biology},
pages = {64 -- 72},
publisher = {Elsevier},
title = {{Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma}},
doi = {10.1016/j.jtbi.2017.08.025},
volume = {433},
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{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{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{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},
}
@phdthesis{821,
abstract = {This dissertation focuses on algorithmic aspects of program verification, and presents modeling and complexity advances on several problems related to the
static analysis of programs, the stateless model checking of concurrent programs, and the competitive analysis of real-time scheduling algorithms.
Our contributions can be broadly grouped into five categories.
Our first contribution is a set of new algorithms and data structures for the quantitative and data-flow analysis of programs, based on the graph-theoretic notion of treewidth.
It has been observed that the control-flow graphs of typical programs have special structure, and are characterized as graphs of small treewidth.
We utilize this structural property to provide faster algorithms for the quantitative and data-flow analysis of recursive and concurrent programs.
In most cases we make an algebraic treatment of the considered problem,
where several interesting analyses, such as the reachability, shortest path, and certain kind of data-flow analysis problems follow as special cases.
We exploit the constant-treewidth property to obtain algorithmic improvements for on-demand versions of the problems,
and provide data structures with various tradeoffs between the resources spent in the preprocessing and querying phase.
We also improve on the algorithmic complexity of quantitative problems outside the algebraic path framework,
namely of the minimum mean-payoff, minimum ratio, and minimum initial credit for energy problems.
Our second contribution is a set of algorithms for Dyck reachability with applications to data-dependence analysis and alias analysis.
In particular, we develop an optimal algorithm for Dyck reachability on bidirected graphs, which are ubiquitous in context-insensitive, field-sensitive points-to analysis.
Additionally, we develop an efficient algorithm for context-sensitive data-dependence analysis via Dyck reachability,
where the task is to obtain analysis summaries of library code in the presence of callbacks.
Our algorithm preprocesses libraries in almost linear time, after which the contribution of the library in the complexity of the client analysis is (i)~linear in the number of call sites and (ii)~only logarithmic in the size of the whole library, as opposed to linear in the size of the whole library.
Finally, we prove that Dyck reachability is Boolean Matrix Multiplication-hard in general, and the hardness also holds for graphs of constant treewidth.
This hardness result strongly indicates that there exist no combinatorial algorithms for Dyck reachability with truly subcubic complexity.
Our third contribution is the formalization and algorithmic treatment of the Quantitative Interprocedural Analysis framework.
In this framework, the transitions of a recursive program are annotated as good, bad or neutral, and receive a weight which measures
the magnitude of their respective effect.
The Quantitative Interprocedural Analysis problem asks to determine whether there exists an infinite run of the program where the long-run ratio of the bad weights over the good weights is above a given threshold.
We illustrate how several quantitative problems related to static analysis of recursive programs can be instantiated in this framework,
and present some case studies to this direction.
Our fourth contribution is a new dynamic partial-order reduction for the stateless model checking of concurrent programs. Traditional approaches rely on the standard Mazurkiewicz equivalence between traces, by means of partitioning the trace space into equivalence classes, and attempting to explore a few representatives from each class.
We present a new dynamic partial-order reduction method called the Data-centric Partial Order Reduction (DC-DPOR).
Our algorithm is based on a new equivalence between traces, called the observation equivalence.
DC-DPOR explores a coarser partitioning of the trace space than any exploration method based on the standard Mazurkiewicz equivalence.
Depending on the program, the new partitioning can be even exponentially coarser.
Additionally, DC-DPOR spends only polynomial time in each explored class.
Our fifth contribution is the use of automata and game-theoretic verification techniques in the competitive analysis and synthesis of real-time scheduling algorithms for firm-deadline tasks.
On the analysis side, we leverage automata on infinite words to compute the competitive ratio of real-time schedulers subject to various environmental constraints.
On the synthesis side, we introduce a new instance of two-player mean-payoff partial-information games, and show
how the synthesis of an optimal real-time scheduler can be reduced to computing winning strategies in this new type of games.},
author = {Pavlogiannis, Andreas},
pages = {418},
publisher = {IST Austria},
title = {{Algorithmic advances in program analysis and their applications}},
doi = {10.15479/AT:ISTA:th_854},
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},
}
@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},
}