@inproceedings{12767, abstract = {Several problems in planning and reactive synthesis can be reduced to the analysis of two-player quantitative graph games. Optimization is one form of analysis. We argue that in many cases it may be better to replace the optimization problem with the satisficing problem, where instead of searching for optimal solutions, the goal is to search for solutions that adhere to a given threshold bound. This work defines and investigates the satisficing problem on a two-player graph game with the discounted-sum cost model. We show that while the satisficing problem can be solved using numerical methods just like the optimization problem, this approach does not render compelling benefits over optimization. When the discount factor is, however, an integer, we present another approach to satisficing, which is purely based on automata methods. We show that this approach is algorithmically more performant – both theoretically and empirically – and demonstrates the broader applicability of satisficing over optimization.}, author = {Bansal, Suguman and Chatterjee, Krishnendu and Vardi, Moshe Y.}, booktitle = {27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783030720155}, issn = {1611-3349}, location = {Luxembourg City, Luxembourg}, pages = {20--37}, publisher = {Springer Nature}, title = {{On satisficing in quantitative games}}, doi = {10.1007/978-3-030-72016-2}, volume = {12651}, year = {2021}, } @inproceedings{10667, abstract = {Bayesian neural networks (BNNs) place distributions over the weights of a neural network to model uncertainty in the data and the network's prediction. We consider the problem of verifying safety when running a Bayesian neural network policy in a feedback loop with infinite time horizon systems. Compared to the existing sampling-based approaches, which are inapplicable to the infinite time horizon setting, we train a separate deterministic neural network that serves as an infinite time horizon safety certificate. In particular, we show that the certificate network guarantees the safety of the system over a subset of the BNN weight posterior's support. Our method first computes a safe weight set and then alters the BNN's weight posterior to reject samples outside this set. Moreover, we show how to extend our approach to a safe-exploration reinforcement learning setting, in order to avoid unsafe trajectories during the training of the policy. We evaluate our approach on a series of reinforcement learning benchmarks, including non-Lyapunovian safety specifications.}, author = {Lechner, Mathias and Žikelić, Ðorđe and Chatterjee, Krishnendu and Henzinger, Thomas A}, booktitle = {35th Conference on Neural Information Processing Systems}, location = {Virtual}, title = {{Infinite time horizon safety of Bayesian neural networks}}, doi = {10.48550/arXiv.2111.03165}, year = {2021}, } @article{8793, abstract = {We study optimal election sequences for repeatedly selecting a (very) small group of leaders among a set of participants (players) with publicly known unique ids. In every time slot, every player has to select exactly one player that it considers to be the current leader, oblivious to the selection of the other players, but with the overarching goal of maximizing a given parameterized global (“social”) payoff function in the limit. We consider a quite generic model, where the local payoff achieved by a given player depends, weighted by some arbitrary but fixed real parameter, on the number of different leaders chosen in a round, the number of players that choose the given player as the leader, and whether the chosen leader has changed w.r.t. the previous round or not. The social payoff can be the maximum, average or minimum local payoff of the players. Possible applications include quite diverse examples such as rotating coordinator-based distributed algorithms and long-haul formation flying of social birds. Depending on the weights and the particular social payoff, optimal sequences can be very different, from simple round-robin where all players chose the same leader alternatingly every time slot to very exotic patterns, where a small group of leaders (at most 2) is elected in every time slot. Moreover, we study the question if and when a single player would not benefit w.r.t. its local payoff when deviating from the given optimal sequence, i.e., when our optimal sequences are Nash equilibria in the restricted strategy space of oblivious strategies. As this is the case for many parameterizations of our model, our results reveal that no punishment is needed to make it rational for the players to optimize the social payoff.}, author = {Zeiner, Martin and Schmid, Ulrich and Chatterjee, Krishnendu}, issn = {0166218X}, journal = {Discrete Applied Mathematics}, number = {1}, pages = {392--415}, publisher = {Elsevier}, title = {{Optimal strategies for selecting coordinators}}, doi = {10.1016/j.dam.2020.10.022}, volume = {289}, year = {2021}, } @article{9381, abstract = {A game of rock-paper-scissors is an interesting example of an interaction where none of the pure strategies strictly dominates all others, leading to a cyclic pattern. In this work, we consider an unstable version of rock-paper-scissors dynamics and allow individuals to make behavioural mistakes during the strategy execution. We show that such an assumption can break a cyclic relationship leading to a stable equilibrium emerging with only one strategy surviving. We consider two cases: completely random mistakes when individuals have no bias towards any strategy and a general form of mistakes. Then, we determine conditions for a strategy to dominate all other strategies. However, given that individuals who adopt a dominating strategy are still prone to behavioural mistakes in the observed behaviour, we may still observe extinct strategies. That is, behavioural mistakes in strategy execution stabilise evolutionary dynamics leading to an evolutionary stable and, potentially, mixed co-existence equilibrium.}, author = {Kleshnina, Maria and Streipert, Sabrina S. and Filar, Jerzy A. and Chatterjee, Krishnendu}, issn = {15537358}, journal = {PLoS Computational Biology}, number = {4}, publisher = {Public Library of Science}, title = {{Mistakes can stabilise the dynamics of rock-paper-scissors games}}, doi = {10.1371/journal.pcbi.1008523}, volume = {17}, year = {2021}, } @article{9640, abstract = {Selection and random drift determine the probability that novel mutations fixate in a population. Population structure is known to affect the dynamics of the evolutionary process. Amplifiers of selection are population structures that increase the fixation probability of beneficial mutants compared to well-mixed populations. Over the past 15 years, extensive research has produced remarkable structures called strong amplifiers which guarantee that every beneficial mutation fixates with high probability. But strong amplification has come at the cost of considerably delaying the fixation event, which can slow down the overall rate of evolution. However, the precise relationship between fixation probability and time has remained elusive. Here we characterize the slowdown effect of strong amplification. First, we prove that all strong amplifiers must delay the fixation event at least to some extent. Second, we construct strong amplifiers that delay the fixation event only marginally as compared to the well-mixed populations. Our results thus establish a tight relationship between fixation probability and time: Strong amplification always comes at a cost of a slowdown, but more than a marginal slowdown is not needed.}, author = {Tkadlec, Josef and Pavlogiannis, Andreas and Chatterjee, Krishnendu and Nowak, Martin A.}, issn = {20411723}, journal = {Nature Communications}, number = {1}, publisher = {Springer Nature}, title = {{Fast and strong amplifiers of natural selection}}, doi = {10.1038/s41467-021-24271-w}, volume = {12}, year = {2021}, } @inproceedings{9646, abstract = {We consider the fundamental problem of deriving quantitative bounds on the probability that a given assertion is violated in a probabilistic program. We provide automated algorithms that obtain both lower and upper bounds on the assertion violation probability. The main novelty of our approach is that we prove new and dedicated fixed-point theorems which serve as the theoretical basis of our algorithms and enable us to reason about assertion violation bounds in terms of pre and post fixed-point functions. To synthesize such fixed-points, we devise algorithms that utilize a wide range of mathematical tools, including repulsing ranking supermartingales, Hoeffding's lemma, Minkowski decompositions, Jensen's inequality, and convex optimization. On the theoretical side, we provide (i) the first automated algorithm for lower-bounds on assertion violation probabilities, (ii) the first complete algorithm for upper-bounds of exponential form in affine programs, and (iii) provably and significantly tighter upper-bounds than the previous approaches. On the practical side, we show our algorithms can handle a wide variety of programs from the literature and synthesize bounds that are remarkably tighter than previous results, in some cases by thousands of orders of magnitude.}, author = {Wang, Jinyi and Sun, Yican and Fu, Hongfei and Chatterjee, Krishnendu and Goharshady, Amir Kafshdar}, booktitle = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation}, isbn = {9781450383912}, location = {Online}, pages = {1171--1186}, publisher = {Association for Computing Machinery}, title = {{Quantitative analysis of assertion violations in probabilistic programs}}, doi = {10.1145/3453483.3454102}, year = {2021}, } @inproceedings{9645, abstract = {We consider the fundamental problem of reachability analysis over imperative programs with real variables. Previous works that tackle reachability are either unable to handle programs consisting of general loops (e.g. symbolic execution), or lack completeness guarantees (e.g. abstract interpretation), or are not automated (e.g. incorrectness logic). In contrast, we propose a novel approach for reachability analysis that can handle general and complex loops, is complete, and can be entirely automated for a wide family of programs. Through the notion of Inductive Reachability Witnesses (IRWs), our approach extends ideas from both invariant generation and termination to reachability analysis. We first show that our IRW-based approach is sound and complete for reachability analysis of imperative programs. Then, we focus on linear and polynomial programs and develop automated methods for synthesizing linear and polynomial IRWs. In the linear case, we follow the well-known approaches using Farkas' Lemma. Our main contribution is in the polynomial case, where we present a push-button semi-complete algorithm. We achieve this using a novel combination of classical theorems in real algebraic geometry, such as Putinar's Positivstellensatz and Hilbert's Strong Nullstellensatz. Finally, our experimental results show we can prove complex reachability objectives over various benchmarks that were beyond the reach of previous methods.}, author = {Asadi, Ali and Chatterjee, Krishnendu and Fu, Hongfei and Goharshady, Amir Kafshdar and Mahdavi, Mohammad}, booktitle = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation}, isbn = {9781450383912}, location = {Online}, pages = {772--787}, publisher = {Association for Computing Machinery}, title = {{Polynomial reachability witnesses via Stellensätze}}, doi = {10.1145/3453483.3454076}, year = {2021}, } @inproceedings{10002, abstract = {We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with n vertices and m edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires O(n2) symbolic operations and O(1) symbolic space. The only other symbolic algorithm for the MEC decomposition requires O(nm−−√) symbolic operations and O(m−−√) symbolic space. A main open question is whether the worst-case O(n2) bound for symbolic operations can be beaten. We present a symbolic algorithm that requires O˜(n1.5) symbolic operations and O˜(n−−√) symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all 0<ϵ≤1/2 the symbolic algorithm requires O˜(n2−ϵ) symbolic operations and O˜(nϵ) symbolic space ( O˜ hides poly-logarithmic factors). Using our techniques we present faster algorithms for computing the almost-sure winning regions of ω -regular objectives for MDPs. We consider the canonical parity objectives for ω -regular objectives, and for parity objectives with d -priorities we present an algorithm that computes the almost-sure winning region with O˜(n2−ϵ) symbolic operations and O˜(nϵ) symbolic space, for all 0<ϵ≤1/2 .}, author = {Chatterjee, Krishnendu and Dvorak, Wolfgang and Henzinger, Monika H and Svozil, Alexander}, booktitle = {Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science}, isbn = {978-1-6654-4896-3}, issn = {1043-6871}, keywords = {Computer science, Computational modeling, Markov processes, Probabilistic logic, Formal verification, Game Theory}, location = {Rome, Italy}, pages = {1--13}, publisher = {Institute of Electrical and Electronics Engineers}, title = {{Symbolic time and space tradeoffs for probabilistic verification}}, doi = {10.1109/LICS52264.2021.9470739}, year = {2021}, } @inproceedings{10004, abstract = {Markov chains are the de facto finite-state model for stochastic dynamical systems, and Markov decision processes (MDPs) extend Markov chains by incorporating non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization criterion is the maximal expected total reward where the MDP stops after T steps, which can be computed by a simple dynamic programming algorithm. We consider a natural generalization of the problem where the stopping times can be chosen according to a probability distribution, such that the expected stopping time is T, to optimize the expected total reward. Quite surprisingly we establish inter-reducibility of the expected stopping-time problem for Markov chains with the Positivity problem (which is related to the well-known Skolem problem), for which establishing either decidability or undecidability would be a major breakthrough. Given the hardness of the exact problem, we consider the approximate version of the problem: we show that it can be solved in exponential time for Markov chains and in exponential space for MDPs.}, author = {Chatterjee, Krishnendu and Doyen, Laurent}, booktitle = {Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science}, isbn = {978-1-6654-4896-3}, issn = {1043-6871}, keywords = {Computer science, Heuristic algorithms, Memory management, Automata, Markov processes, Probability distribution, Complexity theory}, location = {Rome, Italy}, pages = {1--13}, publisher = {Institute of Electrical and Electronics Engineers}, title = {{Stochastic processes with expected stopping time}}, doi = {10.1109/LICS52264.2021.9470595}, year = {2021}, } @inproceedings{10055, abstract = {Repeated idempotent elements are commonly used to characterise iterable behaviours in abstract models of computation. Therefore, given a monoid M, it is natural to ask how long a sequence of elements of M needs to be to ensure the presence of consecutive idempotent factors. This question is formalised through the notion of the Ramsey function R_M associated to M, obtained by mapping every k ∈ ℕ to the minimal integer R_M(k) such that every word u ∈ M^* of length R_M(k) contains k consecutive non-empty factors that correspond to the same idempotent element of M. In this work, we study the behaviour of the Ramsey function R_M by investigating the regular 𝒟-length of M, defined as the largest size L(M) of a submonoid of M isomorphic to the set of natural numbers {1,2, …, L(M)} equipped with the max operation. We show that the regular 𝒟-length of M determines the degree of R_M, by proving that k^L(M) ≤ R_M(k) ≤ (k|M|⁴)^L(M). To allow applications of this result, we provide the value of the regular 𝒟-length of diverse monoids. In particular, we prove that the full monoid of n × n Boolean matrices, which is used to express transition monoids of non-deterministic automata, has a regular 𝒟-length of (n²+n+2)/2.}, author = {Jecker, Ismael R}, booktitle = {38th International Symposium on Theoretical Aspects of Computer Science}, isbn = {978-3-9597-7180-1}, issn = {1868-8969}, location = {Saarbrücken, Germany}, publisher = {Schloss Dagstuhl - Leibniz Zentrum für Informatik}, title = {{A Ramsey theorem for finite monoids}}, doi = {10.4230/LIPIcs.STACS.2021.44}, volume = {187}, year = {2021}, }