@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}, } @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}, } @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}, } @misc{5559, abstract = {Strong amplifiers of natural selection}, author = {Pavlogiannis, Andreas and Tkadlec, Josef and Chatterjee, Krishnendu and Nowak , Martin}, keywords = {natural selection}, publisher = {Institute of Science and Technology Austria}, title = {{Strong amplifiers of natural selection}}, doi = {10.15479/AT:ISTA:51}, year = {2017}, } @inproceedings{639, 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 non-recursive programs. First, we apply ranking functions to recursion, resulting in measure functions, and show that they 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 non-polynomial 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 O(n log n) as well as O(nr) where r is not an integer. We present experimental results to demonstrate that our approach can efficiently obtain worst-case bounds of classical recursive algorithms such as Merge-Sort, Closest-Pair, Karatsuba’s algorithm and Strassen’s algorithm.}, author = {Chatterjee, Krishnendu and Fu, Hongfei and Goharshady, Amir}, editor = {Majumdar, Rupak and Kunčak, Viktor}, isbn = {978-331963389-3}, location = {Heidelberg, Germany}, pages = {41 -- 63}, publisher = {Springer}, title = {{Non-polynomial worst case analysis of recursive programs}}, doi = {10.1007/978-3-319-63390-9_3}, volume = {10427}, year = {2017}, } @inproceedings{949, abstract = {The notion of treewidth of graphs has been exploited for faster algorithms for several problems arising in verification and program analysis. Moreover, various notions of balanced tree decompositions have been used for improved algorithms supporting dynamic updates and analysis of concurrent programs. In this work, we present a tool for constructing tree-decompositions of CFGs obtained from Java methods, which is implemented as an extension to the widely used Soot framework. The experimental results show that our implementation on real-world Java benchmarks is very efficient. Our tool also provides the first implementation for balancing tree-decompositions. In summary, we present the first tool support for exploiting treewidth in the static analysis problems on Java programs.}, author = {Chatterjee, Krishnendu and Goharshady, Amir and Pavlogiannis, Andreas}, editor = {D'Souza, Deepak}, issn = {03029743}, location = {Pune, India}, pages = {59 -- 66}, publisher = {Springer}, title = {{JTDec: A tool for tree decompositions in soot}}, doi = {10.1007/978-3-319-68167-2_4}, volume = {10482}, year = {2017}, } @inproceedings{1068, abstract = {Games on graphs provide the appropriate framework to study several central problems in computer science, such as verification and synthesis of reactive systems. One of the most basic objectives for games on graphs is the liveness (or Büchi) objective that given a target set of vertices requires that some vertex in the target set is visited infinitely often. We study generalized Büchi objectives (i.e., conjunction of liveness objectives), and implications between two generalized Büchi objectives (known as GR(1) objectives), that arise in numerous applications in computer-aided verification. We present improved algorithms and conditional super-linear lower bounds based on widely believed assumptions about the complexity of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider graph games with n vertices, m edges, and generalized Büchi objectives with k conjunctions. First, we present an algorithm with running time O(k*n^2), improving the previously known O(k*n*m) and O(k^2*n^2) worst-case bounds. Our algorithm is optimal for dense graphs under (A1). Second, we show that the basic algorithm for the problem is optimal for sparse graphs when the target sets have constant size under (A2). Finally, we consider GR(1) objectives, with k_1 conjunctions in the antecedent and k_2 conjunctions in the consequent, and present an O(k_1 k_2 n^{2.5})-time algorithm, improving the previously known O(k_1*k_2*n*m)-time algorithm for m > n^{1.5}. }, author = {Chatterjee, Krishnendu and Dvorák, Wolfgang and Henzinger, Monika H and Loitzenbauer, Veronika}, location = {Krakow, Poland}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Conditionally optimal algorithms for generalized Büchi Games}}, doi = {10.4230/LIPIcs.MFCS.2016.25}, volume = {58}, year = {2016}, } @inproceedings{1069, abstract = {The Continuous Skolem Problem asks whether a real-valued function satisfying a linear differen- tial equation has a zero in a given interval of real numbers. This is a fundamental reachability problem for continuous linear dynamical systems, such as linear hybrid automata and continuous- time Markov chains. Decidability of the problem is currently open – indeed decidability is open even for the sub-problem in which a zero is sought in a bounded interval. In this paper we show decidability of the bounded problem subject to Schanuel’s Conjecture, a unifying conjecture in transcendental number theory. We furthermore analyse the unbounded problem in terms of the frequencies of the differential equation, that is, the imaginary parts of the characteristic roots. We show that the unbounded problem can be reduced to the bounded problem if there is at most one rationally linearly independent frequency, or if there are two rationally linearly independent frequencies and all characteristic roots are simple. We complete the picture by showing that de- cidability of the unbounded problem in the case of two (or more) rationally linearly independent frequencies would entail a major new effectiveness result in Diophantine approximation, namely computability of the Diophantine-approximation types of all real algebraic numbers.}, author = {Chonev, Ventsislav K and Ouaknine, Joël and Worrell, James}, location = {Rome, Italy}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik}, title = {{On the skolem problem for continuous linear dynamical systems}}, doi = {10.4230/LIPIcs.ICALP.2016.100}, volume = {55}, year = {2016}, } @inproceedings{1070, abstract = {We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. We show that our variant of CTL is decidable and that the model-checking problem is in Delta_3^P = P^{NP^NP}, and is DP-hard. We analogously consider quantifier exchange in extensions of CTL, and we present operators defined using basic operators of CTL* that express the occurrence of infinitely many synchronization points. We show that the model-checking problem remains in Delta_3^P. The distinguishing power of CTL and of our new logic coincide if the Next operator is allowed in the logics, thus the classical bisimulation quotient can be used for state-space reduction before model checking. }, author = {Chatterjee, Krishnendu and Doyen, Laurent}, location = {Rome, Italy}, publisher = {Schloss Dagstuhl- Leibniz-Zentrum fur Informatik}, title = {{Computation tree logic for synchronization properties}}, doi = {10.4230/LIPIcs.ICALP.2016.98}, volume = {55}, year = {2016}, } @inproceedings{1090, abstract = { While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan}, location = {Krakow; Poland}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Nested weighted limit-average automata of bounded width}}, doi = {10.4230/LIPIcs.MFCS.2016.24}, volume = {58}, year = {2016}, }