Showing 151–200 of 362 results for author: Chatterjee, K

Innovative ranking strategy for IPL team formation

Authors: Saptarshi Banerjee, Arnabi Mitra, Debayan Ganguly, Ritajit Majumdar, Kingshuk Chatterjee

Abstract: Indian Premier League (IPL) is a tournament of twenty over cricket matches. Teams of this tournament are selected via an auction from a pool of players. Each team employs a think-tank to build the best possible team. Few studies have been performed to automate the process of team selection. However, those studies mostly concentrate either on the current form of the players, or their long term perf… ▽ More Indian Premier League (IPL) is a tournament of twenty over cricket matches. Teams of this tournament are selected via an auction from a pool of players. Each team employs a think-tank to build the best possible team. Few studies have been performed to automate the process of team selection. However, those studies mostly concentrate either on the current form of the players, or their long term performance. In this paper, we have (i) selected traditional features as well as determined some derived features, which are generated from the traditional features, for batsmen and bowlers, (ii) formulated heuristics for clustering batsmen into openers, middle-order batsmen and finishers, (iii) formulated heuristics for relative ranking of batsmen and bowlers considering the current performance as well as the experience of each player, and (iv) have proposed two greedy algorithms for team selection where the total credit point of the team and the number of players in each cluster is fixed. Our proposed ranking scheme and algorithm not only determines the best possible team but can also determine the best alternate player if one of the target players is unavailable. △ Less

Submitted 5 August, 2019; originally announced August 2019.

Comments: 6 pages, 2 columns

Deciding Fast Termination for Probabilistic VASS with Nondeterminism

Authors: Tomáš Brázdil, Krishnendu Chatterjee, Antonín Kučera, Petr Novotný, Dominik Velan

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 abst… ▽ More 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 $Ω(n^2)$. △ Less

Submitted 25 July, 2019; originally announced July 2019.

Comments: 23 pages, was accepted to ATVA 2019

Strategy Representation by Decision Trees with Linear Classifiers

Authors: Pranav Ashok, Tomáš Brázdil, Krishnendu Chatterjee, Jan Křetínský, Christoph H. Lampert, Viktor Toman

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 nondeterm… ▽ More 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. △ Less

Submitted 27 June, 2019; v1 submitted 19 June, 2019; originally announced June 2019.

Comments: Full version of the paper. To appear in QEST 2019

Energy extraction and particle acceleration around a rotating dyonic black hole in $N=2$, $U(1)^2$ gauged supergravity

Authors: Anik Rudra, Hemwati Nandan, Radouane Gannouji, Soham Chakraborty, Arindam Kumar Chatterjee

Abstract: In the present paper, we explore various gravitational aspects such as energy extraction (via the Penrose process and Superradiance), particle collisions around a $\mathcal{N}=2$, $U(1)^2$ dyonic rotating black hole (BH) in the gauged supergravity model. The impact of the rotation parameter ($a$) and the gauge coupling constant ($g$) on the behaviour of horizon and ergoregion of the BH is studied.… ▽ More In the present paper, we explore various gravitational aspects such as energy extraction (via the Penrose process and Superradiance), particle collisions around a $\mathcal{N}=2$, $U(1)^2$ dyonic rotating black hole (BH) in the gauged supergravity model. The impact of the rotation parameter ($a$) and the gauge coupling constant ($g$) on the behaviour of horizon and ergoregion of the BH is studied. It is of interest to note that, compared with the extremal Kerr BH, the gauge coupling constant, under certain constraints, can enhance the maximum efficiency of energy extraction by the Penrose process almost double. Under the same constraints, we can extract approximately 60.75\% of the initial mass energy from the BH which is noticeably higher in contrast to the extremal Kerr BH. The limit of energy extraction in terms of the local speeds of the fragments is also examined with the help of the Wald inequality. We identify an upper limit on the gauge coupling constant up to which the phenomenon of Superradiance is likely to occur. Finally, we computed the center-of-mass energy ($E_{CM}$) of two particles with the same rest masses moving in the equatorial plane of the BH. Our study also aims to sensitize $E_{CM}$ to the rotation parameter and the gauge coupling constant for extremal and nonextremal spacetime as well. Especially, for the extremal case, an infinitely large amount of $E_{CM}$ can be achieved closer to the horizon which allows the BH to serve as a more powerful Planck-energy-scale collider as compared to Kerr and any other generalized BHs in the Kerr family explored so far in general relativity. However, $E_{CM}$ for the nonextremal spacetime is shown to be finite and has an upper bound. △ Less

Submitted 3 March, 2020; v1 submitted 9 June, 2019; originally announced June 2019.

Comments: 20 pages, 16 figures, 6 tables. Completely new abstract, Conclusion with major changes to BSW effect are made along with the corrections of few typos

Limits on amplifiers of natural selection under death-Birth updating

Authors: Josef Tkadlec, Andreas Pavlogiannis, Krishnendu Chatterjee, Martin A. Nowak

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, so… ▽ More 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 \emph{bounded} and \emph{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^\star$. 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. △ Less

Submitted 6 June, 2019; originally announced June 2019.

The Evolutionary Price of Anarchy: Locally Bounded Agents in a Dynamic Virus Game

Authors: Krishnendu Chatterjee, Laura Schmid, Stefan Schmid

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., re… ▽ More 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. △ Less

Submitted 31 May, 2019; originally announced June 2019.

ACM Class: C.2.4; G.3

Second-Order Multi-Reference Algebraic Diagrammatic Construction Theory for Photoelectron Spectra of Strongly Correlated Systems

Authors: Koushik Chatterjee, Alexander Yu. Sokolov

Abstract: We present a second-order formulation of multi-reference algebraic diagrammatic construction theory [Sokolov, A. Yu. J. Chem. Phys. 2018, 149, 204113] for simulating photoelectron spectra of strongly correlated systems (MR-ADC(2)). The MR-ADC(2) method uses second-order multi-reference perturbation theory (MRPT2) to efficiently obtain ionization energies and intensities for many photoelectron tran… ▽ More We present a second-order formulation of multi-reference algebraic diagrammatic construction theory [Sokolov, A. Yu. J. Chem. Phys. 2018, 149, 204113] for simulating photoelectron spectra of strongly correlated systems (MR-ADC(2)). The MR-ADC(2) method uses second-order multi-reference perturbation theory (MRPT2) to efficiently obtain ionization energies and intensities for many photoelectron transitions in a single computation. In contrast to conventional MRPT2 methods, MR-ADC(2) provides information about ionization of electrons in all orbitals (i.e., core and active) and allows to compute transition intensities in straightforward and efficient way. Although equations of MR-ADC(2) depend on four-particle reduced density matrices, we demonstrate that computation of these large matrices can be completely avoided without introducing any approximations. The resulting MR-ADC(2) implementation has a lower computational scaling compared to conventional MRPT2 methods. We present results of MR-ADC(2) for photoelectron spectra of small molecules, carbon dimer, and equally-spaced hydrogen chains (H10 and H30) and outline directions for future developments. △ Less

Submitted 26 September, 2019; v1 submitted 30 May, 2019; originally announced May 2019.

Journal ref: J. Chem. Theory Comput. 15, 5908 (2019)

Long-Run Average Behavior of Vector Addition Systems with States

Authors: Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop

Abstract: A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite co… ▽ More A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite computations of VASS. The cost of a configuration is for each state, a linear combination of the counter values. In the special case of uniform cost functions, the linear combination is the same for all states. The (regular) long-run emptiness problem is, given a VASS, a cost function, and a threshold value, if there is a (lasso-shaped) computation such that the long-run average value of the cost function does not exceed the threshold. For uniform cost functions, we show that the regular long-run emptiness problem is (a)~decidable in polynomial time for integer-valued VASS, and (b)~decidable but nonelementarily hard for natural-valued VASS (i.e., nonnegative counters). For general cost functions, we show that the problem is (c)~NP-complete for integer-valued VASS, and (d)~undecidable for natural-valued VASS. Our most interesting result is for (c) integer-valued VASS with general cost functions, where we establish a connection between the regular long-run emptiness problem and quadratic Diophantine inequalities. The general (nonregular) long-run emptiness problem is equally hard as the regular problem in all cases except (c), where it remains open. △ Less

Submitted 14 May, 2019; originally announced May 2019.

Finite-Memory Strategies in POMDPs with Long-Run Average Objectives

Authors: Krishnendu Chatterjee, Raimundo Saona, Bruno Ziliotto

Abstract: Partially observable Markov decision processes (POMDPs) are standard models for dynamic systems with probabilistic and nondeterministic behaviour in uncertain environments. We prove that in POMDPs with long-run average objective, the decision maker has approximately optimal strategies with finite memory. This implies notably that approximating the long-run value is recursively enumerable, as well… ▽ More Partially observable Markov decision processes (POMDPs) are standard models for dynamic systems with probabilistic and nondeterministic behaviour in uncertain environments. We prove that in POMDPs with long-run average objective, the decision maker has approximately optimal strategies with finite memory. This implies notably that approximating the long-run value is recursively enumerable, as well as a weak continuity property of the value with respect to the transition function. △ Less

Submitted 28 September, 2022; v1 submitted 30 April, 2019; originally announced April 2019.

MSC Class: 90C39; 90C40; 37A50

The Event Horizon General Relativistic Magnetohydrodynamic Code Comparison Project

Authors: Oliver Porth, Koushik Chatterjee, Ramesh Narayan, Charles F. Gammie, Yosuke Mizuno, Peter Anninos, John G. Baker, Matteo Bugli, Chi-kwan Chan, Jordy Davelaar, Luca Del Zanna, Zachariah B. Etienne, P. Chris Fragile, Bernard J. Kelly, Matthew Liska, Sera Markoff, Jonathan C. McKinney, Bhupendra Mishra, Scott C. Noble, Héctor Olivares, Ben Prather, Luciano Rezzolla, Benjamin R. Ryan, James M. Stone, Niccolò Tomei , et al. (3 additional authors not shown)

Abstract: Recent developments in compact object astrophysics, especially the discovery of merging neutron stars by LIGO, the imaging of the black hole in M87 by the Event Horizon Telescope (EHT) and high precision astrometry of the Galactic Center at close to the event horizon scale by the GRAVITY experiment motivate the development of numerical source models that solve the equations of general relativistic… ▽ More Recent developments in compact object astrophysics, especially the discovery of merging neutron stars by LIGO, the imaging of the black hole in M87 by the Event Horizon Telescope (EHT) and high precision astrometry of the Galactic Center at close to the event horizon scale by the GRAVITY experiment motivate the development of numerical source models that solve the equations of general relativistic magnetohydrodynamics (GRMHD). Here we compare GRMHD solutions for the evolution of a magnetized accretion flow where turbulence is promoted by the magnetorotational instability from a set of nine GRMHD codes: Athena++, BHAC, Cosmos++, ECHO, H-AMR, iharm3D, HARM-Noble, IllinoisGRMHD and KORAL. Agreement between the codes improves as resolution increases, as measured by a consistently applied, specially developed set of code performance metrics. We conclude that the community of GRMHD codes is mature, capable, and consistent on these test problems. △ Less

Submitted 5 August, 2019; v1 submitted 9 April, 2019; originally announced April 2019.

Comments: Accepted version for publication in ApJS (May 28th, 2019)

Accelerating AGN jets to parsec scales using general relativistic MHD simulations

Authors: Koushik Chatterjee, Matthew Liska, Alexander Tchekhovskoy, Sera B. Markoff

Abstract: Accreting black holes produce collimated outflows, or jets, that traverse many orders of magnitude in distance, accelerate to relativistic velocities, and collimate into tight opening angles. Of these, perhaps the least understood is jet collimation due to the interaction with the ambient medium. In order to investigate this interaction, we carried out axisymmetric general relativistic magnetohydr… ▽ More Accreting black holes produce collimated outflows, or jets, that traverse many orders of magnitude in distance, accelerate to relativistic velocities, and collimate into tight opening angles. Of these, perhaps the least understood is jet collimation due to the interaction with the ambient medium. In order to investigate this interaction, we carried out axisymmetric general relativistic magnetohydrodynamic simulations of jets produced by a large accretion disc, spanning over 5 orders of magnitude in time and distance, at an unprecedented resolution. Supported by such a disc, the jet attains a parabolic shape, similar to the M87 galaxy jet, and the product of the Lorentz factor and the jet half-opening angle, $γθ\ll 1$, similar to values found from very long baseline interferometry (VLBI) observations of active galactic nuclei (AGN) jets; this suggests extended discs in AGN. We find that the interaction between the jet and the ambient medium leads to the development of pinch instabilities, which produce significant radial and lateral variability across the jet by converting magnetic and kinetic energy into heat. Thus pinched regions in the jet can be detectable as radiating hotspots and may provide an ideal site for particle acceleration. Pinching also causes gas from the ambient medium to become squeezed between magnetic field lines in the jet, leading to enhanced mass-loading of the jet and potentially contributing to the spine-sheath structure observed in AGN outflows. △ Less

Submitted 9 May, 2019; v1 submitted 5 April, 2019; originally announced April 2019.

Comments: 18 pages, 24 figures, submitted to MNRAS, revised version. See our Youtube channel for accompanying animations: https://www.youtube.com/playlist?list=PLjldVlE2vDFzHMGn75tgc2Lod0kcTWZdQ

Analytic solutions of the geodesic equation for Reissner-Nordström-(anti-)de Sitter black holes surrounded by different kinds of regular and exotic matter fields

Authors: Arindam Kumar Chatterjee, Kai Flathmann, Hemwati Nandan, Anik Rudra

Abstract: The purpose of this study is the derivation of the equation of motion for particles and light in the spacetime of Reissner-Nordström-(anti-)de Sitter black holes in the background of different kinds of regular and exotic matter fields. The complete analytical solutions of the geodesic equations are given in terms of the elliptic Weierstraß $\wp$-function and the hyperelliptic Kleinian $σ$-function… ▽ More The purpose of this study is the derivation of the equation of motion for particles and light in the spacetime of Reissner-Nordström-(anti-)de Sitter black holes in the background of different kinds of regular and exotic matter fields. The complete analytical solutions of the geodesic equations are given in terms of the elliptic Weierstraß $\wp$-function and the hyperelliptic Kleinian $σ$-function. Finally after analyzing the geodesic motion of test particles and light using parametric diagrams and effective potentials, we present a list of all possible orbits. △ Less

Submitted 23 July, 2019; v1 submitted 28 March, 2019; originally announced March 2019.

Comments: Updated to published version

Journal ref: Phys. Rev. D 100, 024044 (2019)

Parallel communicating one-way reversible finite automata system

Authors: Debayan Ganguly, Kingshuk Chatterjee, Kumar Sankar Ray

Abstract: In this paper, we discuss the computational power of parallel communicating finite automata system with 1-way reversible finite automaton as components. We show that unlike the multi-head one way reversible finite automata model (where we are still not sure whether it accepts all the regular languages) parallel communicating one-way reversible finite automata systems can accept all the regular lan… ▽ More In this paper, we discuss the computational power of parallel communicating finite automata system with 1-way reversible finite automaton as components. We show that unlike the multi-head one way reversible finite automata model (where we are still not sure whether it accepts all the regular languages) parallel communicating one-way reversible finite automata systems can accept all the regular languages. Moreover for every multi-head one way reversible finite automaton there exist a parallel communicating one-way reversible finite automata system which accepts the same language. We also make an interesting observation that although the components of the system are reversible the system as a whole is not reversible. On the basis of which we conjecture that parallel communicating one-way reversible finite automata systems may accept languages not accepted by multi-head one way reversible finite automata. △ Less

Submitted 15 March, 2019; originally announced March 2019.

Bengali Handwritten Character Classification using Transfer Learning on Deep Convolutional Neural Network

Authors: Swagato Chatterjee, Rwik Kumar Dutta, Debayan Ganguly, Kingshuk Chatterjee, Sudipta Roy

Abstract: In this paper, we propose a solution which uses state-of-the-art techniques in Deep Learning to tackle the problem of Bengali Handwritten Character Recognition ( HCR ). Our method uses lesser iterations to train than most other comparable methods. We employ Transfer Learning on ResNet 50, a state-of-the-art deep Convolutional Neural Network Model, pretrained on ImageNet dataset. We also use other… ▽ More In this paper, we propose a solution which uses state-of-the-art techniques in Deep Learning to tackle the problem of Bengali Handwritten Character Recognition ( HCR ). Our method uses lesser iterations to train than most other comparable methods. We employ Transfer Learning on ResNet 50, a state-of-the-art deep Convolutional Neural Network Model, pretrained on ImageNet dataset. We also use other techniques like a modified version of One Cycle Policy, varying the input image sizes etc. to ensure that our training occurs fast. We use the BanglaLekha-Isolated Dataset for evaluation of our technique which consists of 84 classes (50 Basic, 10 Numerals and 24 Compound Characters). We are able to achieve 96.12% accuracy in just 47 epochs on BanglaLekha-Isolated dataset. When comparing our method with that of other researchers, considering number of classes and without using Ensemble Learning, the proposed solution achieves state of the art result for Handwritten Bengali Character Recognition. Code and weight files are available at https://github.com/swagato-c/bangla-hwcr-present. △ Less

Submitted 25 February, 2019; originally announced February 2019.

Probabilistic Smart Contracts: Secure Randomness on the Blockchain

Authors: Krishnendu Chatterjee, Amir Kafshdar Goharshady, Arash Pourdamghani

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 co… ▽ More 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. △ Less

Submitted 21 February, 2019; originally announced February 2019.

Comments: Accepted to the 2019 IEEE International Conference on Blockchain and Cryptocurrency (ICBC 2019)

Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time

Authors: Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, Ming Xu

Abstract: The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterati… ▽ More The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterations is fixed and bounded. In this work, we consider probabilistic while loops where the number of iterations is not fixed, but randomized and depends on the initial input values. We present a sound approach for proving expected sensitivity of such programs. Our sound approach is martingale-based and can be automated through existing martingale-synthesis algorithms. Furthermore, our approach is compositional for sequential composition of while loops under a mild side condition. We demonstrate the effectiveness of our approach on several classical examples from Gambler's Ruin, stochastic hybrid systems and stochastic gradient descent. We also present experimental results showing that our automated approach can handle various probabilistic programs in the literature. △ Less

Submitted 28 October, 2019; v1 submitted 13 February, 2019; originally announced February 2019.

Cost Analysis of Nondeterministic Probabilistic Programs

Authors: Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, Wenjun Shi

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 necessar… ▽ More 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 by presenting experimental results on a variety of programs, motivated by real-world applications, for which we efficiently synthesize tight resource-usage bounds. △ Less

Submitted 25 March, 2019; v1 submitted 12 February, 2019; originally announced February 2019.

Comments: A conference version will appear in the 40th ACM Conference on Programming Language Design and Implementation (PLDI 2019)

Polynomial Invariant Generation for Non-deterministic Recursive Programs

Authors: Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady

Abstract: We consider the classical problem of invariant generation for programs with polynomial assignments and focus on synthesizing invariants that are a conjunction of strict polynomial inequalities. We present a sound and semi-complete method based on positivstellensaetze, i.e. theorems in semi-algebraic geometry that characterize positive polynomials over a semi-algebraic set. To the best of our knowl… ▽ More We consider the classical problem of invariant generation for programs with polynomial assignments and focus on synthesizing invariants that are a conjunction of strict polynomial inequalities. We present a sound and semi-complete method based on positivstellensaetze, i.e. theorems in semi-algebraic geometry that characterize positive polynomials over a semi-algebraic set. To the best of our knowledge, this is the first invariant generation method to provide completeness guarantees for invariants consisting of polynomial inequalities. Moreover, on the theoretical side, the worst-case complexity of our approach is subexponential, whereas the worst-case complexity of the previously-known complete method (Colon et al, CAV 2003), which could only handle linear invariants, is exponential. On the practical side, we reduce the invariant generation problem to quadratic programming (QCLP), which is a classical optimization problem with many industrial solvers. Finally, we demonstrate the applicability of our approach by providing experimental results on several academic benchmarks. △ Less

Submitted 6 April, 2020; v1 submitted 12 February, 2019; originally announced February 2019.

Comments: A conference version of this article appears in PLDI 2020

A new integrated likelihood for estimating population size in dependent dual-record system

Authors: Kiranmoy Chatterjee, Diganta Mukherjee

Abstract: Efficient estimation of population size from dependent dual-record system (DRS) remains a statistical challenge in capture-recapture type experiment. Owing to the nonidentifiability of the suitable Time-Behavioral Response Variation model (denoted as $M_{tb}$) under DRS, few methods are developed in Bayesian paradigm based on informative priors. Our contribution in this article is in develo** in… ▽ More Efficient estimation of population size from dependent dual-record system (DRS) remains a statistical challenge in capture-recapture type experiment. Owing to the nonidentifiability of the suitable Time-Behavioral Response Variation model (denoted as $M_{tb}$) under DRS, few methods are developed in Bayesian paradigm based on informative priors. Our contribution in this article is in develo** integrated likelihood function from model $M_{tb}$ based on a novel approach developed by Severini (2007, Biometrika). Suitable weight function on nuisance parameter is derived under the assumption of availability of knowledge on the direction of behavioral dependency. Such pseudo-likelihood function is constructed so that the resulting estimator possess some desirable properties including invariance and negligible prior (or weight) sensitiveness. Extensive simulations explore the better performance of our proposed method in most of the situations than the existing Bayesian methods. Moreover, being a non-Bayesian estimator, it simply avoids heavy computational effort and time. Finally, illustration based on two real life data sets on epidemiology and economic census are presented. △ Less

Submitted 23 January, 2019; originally announced January 2019.

Comments: 19 Pages

Journal ref: Canadian Journal of Statistics. 46, 577-592 (2018)

Modular Verification for Almost-Sure Termination of Probabilistic Programs

Authors: Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee, Amir Kafshdar Goharshady

Abstract: In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a given probabilistic program terminates with probability 1. Scalable approaches for program analysis often rely on modularity as their theoretical basis. In non-probabilistic programs, the classical variant rule (V-rule) of Floyd-Hoare logic provides the foundation for modular analysis. Exte… ▽ More In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a given probabilistic program terminates with probability 1. Scalable approaches for program analysis often rely on modularity as their theoretical basis. In non-probabilistic programs, the classical variant rule (V-rule) of Floyd-Hoare logic provides the foundation for modular analysis. Extension of this rule to almost-sure termination of probabilistic programs is quite tricky, and a probabilistic variant was proposed in [Fioriti and Hermanns 2015]. While the proposed probabilistic variant cautiously addresses the key issue of integrability, we show that the proposed modular rule is still not sound for almost-sure termination of probabilistic programs. Besides establishing unsoundness of the previous rule, our contributions are as follows: First, we present a sound modular rule for almost-sure termination of probabilistic programs. Our approach is based on a novel notion of descent supermartingales. Second, for algorithmic approaches, we consider descent supermartingales that are linear and show that they can be synthesized in polynomial time. Finally, we present experimental results on a variety of benchmarks and several natural examples that model various types of nested while loops in probabilistic programs and demonstrate that our approach is able to efficiently prove their almost-sure termination property. △ Less

Submitted 12 August, 2019; v1 submitted 18 January, 2019; originally announced January 2019.

Comments: Accepted to OOPSLA 2019

On the Estimation of Population Size from a Dependent Triple Record System

Authors: Kiranmoy Chatterjee, Prajamitra Bhuyan

Abstract: Population size estimation based on capture-recapture experiment under triple record system is an interesting problem in various fields including epidemiology, population studies, etc. In many real life scenarios, there exists inherent dependency between capture and recapture attempts. We propose a novel model that successfully incorporates the possible dependency and the associated parameters pos… ▽ More Population size estimation based on capture-recapture experiment under triple record system is an interesting problem in various fields including epidemiology, population studies, etc. In many real life scenarios, there exists inherent dependency between capture and recapture attempts. We propose a novel model that successfully incorporates the possible dependency and the associated parameters possess nice interpretations. We provide estimation methodology for the population size and the associated model parameters based on maximum likelihood method. The proposed model is applied to analyze real data sets from public health and census coverage evaluation study. The performance of the proposed estimate is evaluated through extensive simulation study and the results are compared with the existing competitors. The results exhibit superiority of the proposed model over the existing competitors both in real data analysis and simulation study. △ Less

Submitted 1 April, 2019; v1 submitted 16 January, 2019; originally announced January 2019.

A sincere tribute to E.C.G Sudarshan's phenomenal contribution toward quantum theory of optical coherence

Authors: Arindam Kumar Chatterjee, Anik Rudra, Soham Chakraborty

Abstract: The diagonal representation and optical equivalence theorem are the E. C. G. Sudarshan's mid 20th century adventures in non-classical optics. It basically deals with a quantum mechanical description of photons to explain the quantum properties of light. Inspired by Sudarshan's pioneering work we try to explain the every minute mathematical details of his paper "Equivalence of semi-classical and qu… ▽ More The diagonal representation and optical equivalence theorem are the E. C. G. Sudarshan's mid 20th century adventures in non-classical optics. It basically deals with a quantum mechanical description of photons to explain the quantum properties of light. Inspired by Sudarshan's pioneering work we try to explain the every minute mathematical details of his paper "Equivalence of semi-classical and quantum mechanical descriptions of statistical light beams". In this article we are going to go through some of the basics in develo** quantum optics, then land up in E.C.G's original work and try to present it as rigorous as possible. We show some of its important applications in various classes of physics problems. △ Less

Submitted 27 June, 2019; v1 submitted 21 November, 2018; originally announced December 2018.

Comments: 15 pages, 1 figure

Fixation probability and fixation time in structured populations

Authors: Josef Tkadlec, Andreas Pavlogiannis, Krishnendu Chatterjee, Martin A. Nowak

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 trade-off between high fixatio… ▽ More 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 trade-off between high fixation probability and short fixation time. First, we show that no amplifiers can have 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. △ Less

Submitted 8 March, 2019; v1 submitted 27 September, 2018; originally announced October 2018.

Repeated Coordination with Private Learning

Authors: Pathikrit Basu, Kalyan Chatterjee, Tetsuya Hoshino, Omer Tamuz

Abstract: We study a repeated game with payoff externalities and observable actions where two players receive information over time about an underlying payoff-relevant state, and strategically coordinate their actions. Players learn about the true state from private signals, as well as the actions of others. They commonly learn the true state (Cripps et al., 2008), but do not coordinate in every equilibrium… ▽ More We study a repeated game with payoff externalities and observable actions where two players receive information over time about an underlying payoff-relevant state, and strategically coordinate their actions. Players learn about the true state from private signals, as well as the actions of others. They commonly learn the true state (Cripps et al., 2008), but do not coordinate in every equilibrium. We show that there exist stable equilibria in which players can overcome unfavorable signal realizations and eventually coordinate on the correct action, for any discount factor. For high discount factors, we show that in addition players can also achieve efficient payoffs. △ Less

Submitted 31 August, 2018; originally announced September 2018.

Assisted exchange models in one dimension

Authors: Amit Kumar Chatterjee, P. K. Mohanty

Abstract: We introduce an assisted exchange model (AEM) on a one dimensional periodic lattice with (K+1) different species of hard core particles, where the exchange rate depends on the pair of particles which undergo exchange and their immediate left neighbor. We show that this stochastic process has a pair factorized steady state for a broad class of exchange dynamics. We calculate exactly the particle cu… ▽ More We introduce an assisted exchange model (AEM) on a one dimensional periodic lattice with (K+1) different species of hard core particles, where the exchange rate depends on the pair of particles which undergo exchange and their immediate left neighbor. We show that this stochastic process has a pair factorized steady state for a broad class of exchange dynamics. We calculate exactly the particle current and spatial correlations (K+1)-species AEM using a transfer matrix formalism. Interestingly the current in AEM exhibits density dependent current reversal and negative differential mobility- both of which have been discussed elaborately by using a two species exchange model which resembles the partially asymmetric conserved lattice gas model in one dimension. Moreover, multi-species version of AEM exhibits additional features like multiple points of current reversal, and unusual response of particle current. △ Less

Submitted 27 June, 2018; originally announced June 2018.

Comments: 13 pages, 4 eps figures

Journal ref: Phys. Rev. E 98, 062134 (2018)

New Approaches for Almost-Sure Termination of Probabilistic Programs

Authors: Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee

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 appro… ▽ More 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. △ Less

Submitted 23 August, 2018; v1 submitted 14 June, 2018; originally announced June 2018.

Parameter-Independent Strategies for pMDPs via POMDPs

Authors: Sebastian Arming, Ezio Bartocci, Krishnendu Chatterjee, Joost-Pieter Katoen, Ana Sokolova

Abstract: Markov Decision Processes (MDPs) are a popular class of models suitable for solving control decision problems in probabilistic reactive systems. We consider parametric MDPs (pMDPs) that include parameters in some of the transition probabilities to account for stochastic uncertainties of the environment such as noise or input disturbances. We study pMDPs with reachability objectives where the par… ▽ More Markov Decision Processes (MDPs) are a popular class of models suitable for solving control decision problems in probabilistic reactive systems. We consider parametric MDPs (pMDPs) that include parameters in some of the transition probabilities to account for stochastic uncertainties of the environment such as noise or input disturbances. We study pMDPs with reachability objectives where the parameter values are unknown and impossible to measure directly during execution, but there is a probability distribution known over the parameter values. We study for the first time computing parameter-independent strategies that are expectation optimal, i.e., optimize the expected reachability probability under the probability distribution over the parameters. We present an encoding of our problem to partially observable MDPs (POMDPs), i.e., a reduction of our problem to computing optimal strategies in POMDPs. We evaluate our method experimentally on several benchmarks: a motivating (repeated) learner model; a series of benchmarks of varying configurations of a robot moving on a grid; and a consensus protocol. △ Less

Submitted 13 June, 2018; originally announced June 2018.

Comments: Extended version of a QEST 2018 paper

Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies

Authors: Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Yaron Velner

Abstract: Crypto-currencies are digital assets designed to work as a medium of exchange, e.g., Bitcoin, but they are susceptible to attacks (dishonest behavior of participants). A framework for the analysis of attacks in crypto-currencies requires (a) modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior; (b) concurrent interactions between participants; and (c) analysi… ▽ More Crypto-currencies are digital assets designed to work as a medium of exchange, e.g., Bitcoin, but they are susceptible to attacks (dishonest behavior of participants). A framework for the analysis of attacks in crypto-currencies requires (a) modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior; (b) concurrent interactions between participants; and (c) analysis of long-term monetary gains. Traditional game-theoretic approaches for the analysis of security protocols consider either qualitative temporal properties such as safety and termination, or the very special class of one-shot (stateless) games. However, to analyze general attacks on protocols for crypto-currencies, both stateful analysis and quantitative objectives are necessary. In this work our main contributions are as follows: (a) we show how a class of concurrent mean-payoff games, namely ergodic games, can model various attacks that arise naturally in crypto-currencies; (b) we present the first practical implementation of algorithms for ergodic games that scales to model realistic problems for crypto-currencies; and (c) we present experimental results showing that our framework can handle games with thousands of states and millions of transitions. △ Less

Submitted 8 June, 2018; originally announced June 2018.

Comments: Accepted to CONCUR 2018

Secure Credit Reporting on the Blockchain

Authors: Amir Kafshdar Goharshady, Ali Behrouz, Krishnendu Chatterjee

Abstract: We present a secure approach for maintaining and reporting credit history records on the Blockchain. Our approach removes third-parties such as credit reporting agencies from the lending process and replaces them with smart contracts. This allows customers to interact directly with the lenders or banks while ensuring the integrity, unmalleability and privacy of their credit data. Most importantly,… ▽ More We present a secure approach for maintaining and reporting credit history records on the Blockchain. Our approach removes third-parties such as credit reporting agencies from the lending process and replaces them with smart contracts. This allows customers to interact directly with the lenders or banks while ensuring the integrity, unmalleability and privacy of their credit data. Most importantly, each customer is given full control over complete or selective disclosure of her credit records, eliminating the risk of privacy violations or data breaches such as the one that happened to Equifax in 2017. Moreover, our approach provides strong guarantees for the lenders as well. A lender can check both correctness and completeness of the credit data disclosed to her. This is the first approach that is able to perform all real-world credit reporting tasks without a central authority or changing the financial mechanisms. △ Less

Submitted 24 May, 2018; v1 submitted 23 May, 2018; originally announced May 2018.

Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS

Authors: Tomáš Brázdil, Krishnendu Chatterjee, Antonín Kučera, Petr Novotný, Dominik Velan, Florian Zuleger

Abstract: Vector Addition Systems with States (VASS) provide a well-known and fundamental model for the analysis of concurrent processes, parameterized systems, and are also used as abstract models of programs in resource bound analysis. In this paper we study the problem of obtaining asymptotic bounds on the termination time of a given VASS. In particular, we focus on the practically important case of obta… ▽ More Vector Addition Systems with States (VASS) provide a well-known and fundamental model for the analysis of concurrent processes, parameterized systems, and are also used as abstract models of programs in resource bound analysis. In this paper we study the problem of obtaining asymptotic bounds on the termination time of a given VASS. In particular, we focus on the practically important case of obtaining polynomial bounds on termination time. Our main contributions are as follows: First, we present a polynomial-time algorithm for deciding whether a given VASS has a linear asymptotic complexity. We also show that if the complexity of a VASS is not linear, it is at least quadratic. Second, we classify VASS according to quantitative properties of their cycles. We show that certain singularities in these properties are the key reason for non-polynomial asymptotic complexity of VASS. In absence of singularities, we show that the asymptotic complexity is always polynomial and of the form $Θ(n^k)$, for some integer $k\leq d$, where $d$ is the dimension of the VASS. We present a polynomial-time algorithm computing the optimal $k$. For general VASS, the same algorithm, which is based on a complete technique for the construction of ranking functions in VASS, produces a valid lower bound, i.e., a $k$ such that the termination complexity is $Ω(n^k)$. Our results are based on new insights into the geometry of VASS dynamics, which hold the potential for further applicability to VASS analysis. △ Less

Submitted 29 April, 2018; originally announced April 2018.

Comments: arXiv admin note: text overlap with arXiv:1708.09253

Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-sum Objectives

Authors: Krishnendu Chatterjee, Adrián Elgyütt, Petr Novotný, Owen Rouillé

Abstract: Partially-observable Markov decision processes (POMDPs) with discounted-sum payoff are a standard framework to model a wide range of problems related to decision making under uncertainty. Traditionally, the goal has been to obtain policies that optimize the expectation of the discounted-sum payoff. A key drawback of the expectation measure is that even low probability events with extreme payoff ca… ▽ More Partially-observable Markov decision processes (POMDPs) with discounted-sum payoff are a standard framework to model a wide range of problems related to decision making under uncertainty. Traditionally, the goal has been to obtain policies that optimize the expectation of the discounted-sum payoff. A key drawback of the expectation measure is that even low probability events with extreme payoff can significantly affect the expectation, and thus the obtained policies are not necessarily risk-averse. An alternate approach is to optimize the probability that the payoff is above a certain threshold, which allows obtaining risk-averse policies, but ignores optimization of the expectation. We consider the expectation optimization with probabilistic guarantee (EOPG) problem, where the goal is to optimize the expectation ensuring that the payoff is above a given threshold with at least a specified probability. We present several results on the EOPG problem, including the first algorithm to solve it. △ Less

Submitted 30 April, 2018; v1 submitted 27 April, 2018; originally announced April 2018.

Comments: Full version of a paper published at IJCAI/ECAI 2018

Computational Approaches for Stochastic Shortest Path on Succinct MDPs

Authors: Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, Nastaran Okati

Abstract: We consider the stochastic shortest path (SSP) problem for succinct Markov decision processes (MDPs), where the MDP consists of a set of variables, and a set of nondeterministic rules that update the variables. First, we show that several examples from the AI literature can be modeled as succinct MDPs. Then we present computational approaches for upper and lower bounds for the SSP problem: (a)~for… ▽ More We consider the stochastic shortest path (SSP) problem for succinct Markov decision processes (MDPs), where the MDP consists of a set of variables, and a set of nondeterministic rules that update the variables. First, we show that several examples from the AI literature can be modeled as succinct MDPs. Then we present computational approaches for upper and lower bounds for the SSP problem: (a)~for computing upper bounds, our method is polynomial-time in the implicit description of the MDP; (b)~for lower bounds, we present a polynomial-time (in the size of the implicit description) reduction to quadratic programming. Our approach is applicable even to infinite-state MDPs. Finally, we present experimental results to demonstrate the effectiveness of our approach on several classical examples from the AI literature. △ Less

Submitted 17 July, 2018; v1 submitted 24 April, 2018; originally announced April 2018.

Algorithms and Conditional Lower Bounds for Planning Problems

Authors: Krishnendu Chatterjee, Wolfgang Dvořák, Monika Henzinger, Alexander Svozil

Abstract: We consider planning problems for graphs, Markov decision processes (MDPs), and games on graphs. While graphs represent the most basic planning model, MDPs represent interaction with nature and games on graphs represent interaction with an adversarial environment. We consider two planning problems where there are k different target sets, and the problems are as follows: (a) the coverage problem as… ▽ More We consider planning problems for graphs, Markov decision processes (MDPs), and games on graphs. While graphs represent the most basic planning model, MDPs represent interaction with nature and games on graphs represent interaction with an adversarial environment. We consider two planning problems where there are k different target sets, and the problems are as follows: (a) the coverage problem asks whether there is a plan for each individual target set, and (b) the sequential target reachability problem asks whether the targets can be reached in sequence. For the coverage problem, we present a linear-time algorithm for graphs and quadratic conditional lower bound for MDPs and games on graphs. For the sequential target problem, we present a linear-time algorithm for graphs, a sub-quadratic algorithm for MDPs, and a quadratic conditional lower bound for games on graphs. Our results with conditional lower bounds establish (i) model-separation results showing that for the coverage problem MDPs and games on graphs are harder than graphs and for the sequential reachability problem games on graphs are harder than MDPs and graphs; (ii) objective-separation results showing that for MDPs the coverage problem is harder than the sequential target problem. △ Less

Submitted 19 April, 2018; originally announced April 2018.

Comments: Accepted at ICAPS'18

Coverability: Realizability Lower Bounds

Authors: Krishnendu Chatterjee, Nir Piterman

Abstract: We introduce the problem of temporal coverability for realizability and synthesis. Namely, given a language of words that must be covered by a produced system, how to automatically produce such a system. We consider the case of coverability with no further specifications, where we have to show that the nondeterminism of the produced system is sufficient to produce all the words required in the out… ▽ More We introduce the problem of temporal coverability for realizability and synthesis. Namely, given a language of words that must be covered by a produced system, how to automatically produce such a system. We consider the case of coverability with no further specifications, where we have to show that the nondeterminism of the produced system is sufficient to produce all the words required in the output language. We show a counting argument on a deterministic automaton representing the language to be covered that allows to produce such a system. We then turn to the case of coverability with additional specification and give a precondition for the existence of a system that produces all required words and at the same time produces only computations satisfying the additional correctness criterion. We combine our counting argument on the deterministic automaton for the language to be covered with a ranking on the deterministic Büchi automaton for the correctness criterion. One of the major issues with practical realizability is the interaction between environment assumptions and system guarantees. In many cases, synthesis produces systems that are vacuous and concentrate on forcing the environment to falsify its assumptions instead of fulfilling their guarantees. Coverability offers an alternative approach to tackle this problem. △ Less

Submitted 10 April, 2018; originally announced April 2018.

Combinations of Qualitative Winning for Stochastic Parity Games

Authors: Krishnendu Chatterjee, Nir Piterman

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 must satisfy the condition, almost-sure winning, which requires the condition is satisfied with probability~1, and limit-sure winning, which requires the condition is satisfied with probability arbitrarily close to~1… ▽ More 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 must satisfy the condition, almost-sure winning, which requires the condition is satisfied with probability~1, and limit-sure winning, which requires the condition is satisfied with probability arbitrarily close to~1. We study the combination 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$ coNP. 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 lie in NP $\cap$ coNP; (b)~we show that for turn-based stochastic games the problem is coNP-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 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 qualitative winning criteria for parity conditions in MDPs and turn-based stochastic games. △ Less

Submitted 10 April, 2018; originally announced April 2018.

Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives

Authors: Krishnendu Chatterjee, Monika Henzinger, Veronika Loitzenbauer, Simin Oraee, Viktor Toman

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. Gi… ▽ More 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. △ Less

Submitted 13 April, 2018; v1 submitted 31 March, 2018; originally announced April 2018.

Comments: Full version of the paper. To appear in CAV 2018

Graph Planning with Expected Finite Horizon

Authors: Krishnendu Chatterjee, Laurent Doyen

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 stop** time is chosen according to some distribution s… ▽ More 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 stop** time is chosen according to some distribution such that the expected stop** time is $T$. If the stop** 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 stop**-time distribution, stationary plans are not sufficient for optimality. Quite surprisingly we show that when an adversary chooses the stop**-time distribution with expected stop** 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 stop**-time distribution can be achieved in polynomial time. Consequently, our polynomial-time algorithm for adversarial stop** time also computes an optimal plan among all possible plans. △ Less

Submitted 10 February, 2018; originally announced February 2018.

Strong Amplifiers of Natural Selection: Proofs

Authors: Andreas Pavlogiannis, Josef Tkadlec, Krishnendu Chatterjee, Martin A. Nowak

Abstract: We consider the modified Moran process on graphs to study the spread of genetic and cultural mutations on structured populations. An initial mutant arises either spontaneously (aka \emph{uniform initialization}), or during reproduction (aka \emph{temperature initialization}) in a population of $n$ individuals, and has a fixed fitness advantage $r>1$ over the residents of the population. The fixati… ▽ More We consider the modified Moran process on graphs to study the spread of genetic and cultural mutations on structured populations. An initial mutant arises either spontaneously (aka \emph{uniform initialization}), or during reproduction (aka \emph{temperature initialization}) in a population of $n$ individuals, and has a fixed fitness advantage $r>1$ over the residents of the population. The fixation probability is the probability that the mutant takes over the entire population. Graphs that ensure fixation probability of~1 in the limit of infinite populations are called \emph{strong amplifiers}. Previously, only a few examples of strong amplifiers were known for uniform initialization, whereas no strong amplifiers were known for temperature initialization. In this work, we study necessary and sufficient conditions for strong amplification, and prove negative and positive results. We show that for temperature initialization, graphs that are unweighted and/or self-loop-free have fixation probability upper-bounded by $1-1/f(r)$, where $f(r)$ is a function linear in $r$. Similarly, we show that for uniform initialization, bounded-degree graphs that are unweighted and/or self-loop-free have fixation probability upper-bounded by $1-1/g(r,c)$, where $c$ is the degree bound and $g(r,c)$ a function linear in $r$. Our main positive result complements these negative results, and is as follows: every family of undirected graphs with (i)~self loops and (ii)~diameter bounded by $n^{1-ε}$, for some fixed $ε>0$, can be assigned weights that makes it a strong amplifier, both for uniform and temperature initialization. △ Less

Submitted 14 May, 2018; v1 submitted 7 February, 2018; originally announced February 2018.

Strategy Representation by Decision Trees in Reactive Synthesis

Authors: Tomáš Brázdil, Krishnendu Chatterjee, Jan Křetínský, Viktor Toman

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 gr… ▽ More 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. △ Less

Submitted 19 March, 2018; v1 submitted 2 February, 2018; originally announced February 2018.

Comments: Full version of the paper. To appear in TACAS 2018

Quantitative Analysis of Smart Contracts

Authors: Krishnendu Chatterjee, Amir Kafshdar Goharshady, Yaron Velner

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… ▽ More 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. △ Less

Submitted 17 June, 2018; v1 submitted 10 January, 2018; originally announced January 2018.

Comments: ESOP 2018

Negative Differential Mobility in Interacting Particle Systems

Authors: Amit Kumar Chatterjee, Urna Basu, P. K. Mohanty

Abstract: Driven particles in presence of crowded environment, obstacles or kinetic constraints often exhibit negative differential mobility (NDM) due to their decreased dynamical activity. We propose a new mechanism for complex many-particle systems where slowing down of certain {\it non-driven} degrees of freedom by the external field can give rise to NDM. This phenomenon, resulting from inter-particle in… ▽ More Driven particles in presence of crowded environment, obstacles or kinetic constraints often exhibit negative differential mobility (NDM) due to their decreased dynamical activity. We propose a new mechanism for complex many-particle systems where slowing down of certain {\it non-driven} degrees of freedom by the external field can give rise to NDM. This phenomenon, resulting from inter-particle interactions, is illustrated in a pedagogical example of two interacting random walkers, one of which is biased by an external field while the same field only slows down the other kee** it unbiased. We also introduce and solve exactly the steady state of several driven diffusive systems, including a two species exclusion model, asymmetric misanthrope and zero-range processes, to show explicitly that this mechanism indeed leads to NDM. △ Less

Submitted 4 December, 2017; originally announced December 2017.

Comments: 5 pages, 3 figures

Journal ref: Phys. Rev. E 97, 052137 (2018)

Lower Bounds for Symbolic Computation on Graphs: Strongly Connected Components, Liveness, Safety, and Diameter

Authors: Krishnendu Chatterjee, Wolfgang Dvořák, Monika Henzinger, Veronika Loitzenbauer

Abstract: A model of computation that is widely used in the formal analysis of reactive systems is symbolic algorithms. In this model the access to the input graph is restricted to consist of symbolic operations, which are expensive in comparison to the standard RAM operations. We give lower bounds on the number of symbolic operations for basic graph problems such as the computation of the strongly connecte… ▽ More A model of computation that is widely used in the formal analysis of reactive systems is symbolic algorithms. In this model the access to the input graph is restricted to consist of symbolic operations, which are expensive in comparison to the standard RAM operations. We give lower bounds on the number of symbolic operations for basic graph problems such as the computation of the strongly connected components and of the approximate diameter as well as for fundamental problems in model checking such as safety, liveness, and co-liveness. Our lower bounds are linear in the number of vertices of the graph, even for constant-diameter graphs. For none of these problems lower bounds on the number of symbolic operations were known before. The lower bounds show an interesting separation of these problems from the reachability problem, which can be solved with $O(D)$ symbolic operations, where $D$ is the diameter of the graph. Additionally we present an approximation algorithm for the graph diameter which requires $\tilde{O}(n \sqrt{D})$ symbolic steps to achieve a $(1+ε)$-approximation for any constant $ε> 0$. This compares to $O(n \cdot D)$ symbolic steps for the (naive) exact algorithm and $O(D)$ symbolic steps for a 2-approximation. Finally we also give a refined analysis of the strongly connected components algorithms of Gentilini et al., showing that it uses an optimal number of symbolic steps that is proportional to the sum of the diameters of the strongly connected components. △ Less

Submitted 24 November, 2017; originally announced November 2017.

Sensor Synthesis for POMDPs with Reachability Objectives

Authors: Krishnendu Chatterjee, Martin Chmelik, Ufuk Topcu

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… ▽ More 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. △ Less

Submitted 29 September, 2017; originally announced October 2017.

Comments: arXiv admin note: text overlap with arXiv:1511.08456

Differential voltage amplification from ferroelectric negative capacitance

Authors: Asif I. Khan, Michael Hoffmann, Korok Chatterjee, Zhongyuan Lu, Ruijuan Xu, Claudy Serrao, Samuel Smith, Lane W. Martin, Chenming C. Hu, Ramamoorthy Ramesh, Sayeef Salahuddin

Abstract: It is well known that one needs an external source of energy to provide voltage amplification. Because of this, conventional circuit elements such as resistors, inductors or capacitors cannot provide amplification all by themselves. Here, we demonstrate that a ferroelectric can cause a differential amplification without needing such an external energy source. As the ferroelectric switches from one… ▽ More It is well known that one needs an external source of energy to provide voltage amplification. Because of this, conventional circuit elements such as resistors, inductors or capacitors cannot provide amplification all by themselves. Here, we demonstrate that a ferroelectric can cause a differential amplification without needing such an external energy source. As the ferroelectric switches from one polarization state to the other, a transfer of energy takes place from the ferroelectric to the dielectric, determined by the ratio of their capacitances, which, in turn, leads to the differential amplification. {This amplification is very different in nature from conventional inductor-capacitor based circuits where an oscillatory amplification can be observed. The demonstration of differential voltage amplification from completely passive capacitor elements only, has fundamental ramifications for next generation electronics. △ Less

Submitted 29 September, 2017; originally announced September 2017.

Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs

Authors: Sheshansh Agrawal, Krishnendu Chatterjee, Petr Novotný

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 given a probabilistic program asks whether the program terminates with probability 1. While ranking functions provide a sound and complete method for… ▽ More 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 given a probabilistic program asks whether the 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). While deep theoretical results have been established about RSMs, their application to probabilistic programs with nondeterminism has been limited only to academic examples. 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 abstractions of real-world programs to demonstrate the effectiveness of our approach. △ Less

Submitted 12 September, 2017; originally announced September 2017.

Comments: Preliminary version

Efficient Algorithms for Checking Fast Termination in VASS

Authors: Tomáš Brázdil, Krishnendu Chatterjee, Antonín Kučera, Petr Novotný, Dominik Velan

Abstract: Vector Addition Systems with States (VASS) consists of a finite state space equipped with d counters, where in each transition every counter is incremented, decremented, or left unchanged. VASS provide a fundamental model for analysis of concurrent processes, parametrized systems, and they are also used as abstract models for programs for bounds analysis. While termination is the basic liveness pr… ▽ More Vector Addition Systems with States (VASS) consists of a finite state space equipped with d counters, where in each transition every counter is incremented, decremented, or left unchanged. VASS provide a fundamental model for analysis of concurrent processes, parametrized systems, and they are also used as abstract models for programs for bounds analysis. While termination is the basic liveness property that asks the qualitative question of whether a given model always terminates or not, the more general quantitative question asks for bounds on the number of steps to termination. In the realm of quantitative bounds a fundamental problem is to obtain asymptotic bounds on termination time. Large asymptotic bounds such as exponential or higher already suggest that either there is some error in modeling, or the model is not useful in practice. Hence we focus on polynomial asymptotic bounds for VASS. While some well-known approaches (e.g., lexicographic ranking functions) are neither sound nor complete with respect to polynomial bounds, other approaches only present sound methods for upper bounds. In this work our main contributions are as follows: First, for linear asymptotic bounds we present a sound and complete method for VASS, and moreover, our algorithm runs in polynomial time. Second, we classify VASS according the normals of the vectors of the cycles. We show that singularities in the normal are the key reason for asymptotic bounds such as exponential and non-elementary for VASS. In absence of singularities, we show that the asymptotic complexity bound is always polynomial and of the form $Θ(n^k)$, for some k $\leq$ d. We present an algorithm, with time complexity polynomial in the size of the VASS and exponential in dimension d, to compute the optimal k. △ Less

Submitted 29 August, 2017; originally announced August 2017.

Comparison of Decision Tree Based Classification Strategies to Detect External Chemical Stimuli from Raw and Filtered Plant Electrical Response

Authors: Shre Kumar Chatterjee, Saptarshi Das, Koushik Maharatna, Elisa Masi, Luisa Santopolo, Ilaria Colzi, Stefano Mancuso, Andrea Vitaletti

Abstract: Plants monitor their surrounding environment and control their physiological functions by producing an electrical response. We recorded electrical signals from different plants by exposing them to Sodium Chloride (NaCl), Ozone (O3) and Sulfuric Acid (H2SO4) under laboratory conditions. After applying pre-processing techniques such as filtering and drift removal, we extracted few statistical featur… ▽ More Plants monitor their surrounding environment and control their physiological functions by producing an electrical response. We recorded electrical signals from different plants by exposing them to Sodium Chloride (NaCl), Ozone (O3) and Sulfuric Acid (H2SO4) under laboratory conditions. After applying pre-processing techniques such as filtering and drift removal, we extracted few statistical features from the acquired plant electrical signals. Using these features, combined with different classification algorithms, we used a decision tree based multi-class classification strategy to identify the three different external chemical stimuli. We here present our exploration to obtain the optimum set of ranked feature and classifier combination that can separate a particular chemical stimulus from the incoming stream of plant electrical signals. The paper also reports an exhaustive comparison of similar feature based classification using the filtered and the raw plant signals, containing the high frequency stochastic part and also the low frequency trends present in it, as two different cases for feature extraction. The work, presented in this paper opens up new possibilities for using plant electrical signals to monitor and detect other environmental stimuli apart from NaCl, O3 and H2SO4 in future. △ Less

Submitted 13 May, 2017; originally announced July 2017.

Journal ref: Sensors and Actuators B: Chemical, vol. 249, pp. 278-295, Oct. 2017

Matrix Product States for Interacting Particles without Hardcore Constraints

Authors: Amit Kumar Chatterjee, P. K. Mohanty

Abstract: We construct matrix product steady state for a class of interacting particle systems where particles do not obey hardcore exclusion, meaning each site can occupy any number of particles subjected to the global conservation of total number of particles in the system. To represent the arbitrary occupancy of the sites, the matrix product ansatz here requires an infinite set of matrices which in turn… ▽ More We construct matrix product steady state for a class of interacting particle systems where particles do not obey hardcore exclusion, meaning each site can occupy any number of particles subjected to the global conservation of total number of particles in the system. To represent the arbitrary occupancy of the sites, the matrix product ansatz here requires an infinite set of matrices which in turn leads to an algebra involving infinite number of matrix equations. We show that these matrix equations, in fact, can be reduced to a single functional relation when the matrices are parametric functions of the representative occupation number. We demonstrate this matrix formulation in a class of stochastic particle hop** processes on a one dimensional periodic lattice where hop rates depend on the occupation numbers of the departure site and its neighbors within a finite range; this includes some well known stochastic processes like, totally asymmetric zero range process, misanthrope process, finite range process and partially asymmetric versions of the same processes but with different rate functions depending on the direction of motion. △ Less

Submitted 19 July, 2017; originally announced July 2017.

Comments: 19 pages

MSC Class: 60Gxx

Journal ref: J. Phys. A: Math. Theor. 50 (2017) 495001

Bidirectional Nested Weighted Automata

Authors: Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop

Abstract: Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We the… ▽ More Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We therefore introduce and study bidirectional NWA that can process input words in both directions. First, we show that bidirectional NWA can express interesting quantitative properties that are not expressible by forward-only NWA. Second, for the fundamental decision problems of emptiness and universality, we establish decidability and complexity results for the new framework which match the best-known results for the special case of forward-only NWA. Thus, for NWA, the increased expressiveness of bidirectionality is achieved at no additional computational complexity. This is in stark contrast to the unweighted case, where bidirectional finite automata are no more expressive but exponentially more succinct than their forward-only counterparts. △ Less

Submitted 26 June, 2017; originally announced June 2017.

Comments: The full version of the CONCUR 2017 paper

ACM Class: F.1.1

Faster Monte-Carlo Algorithms for Fixation Probability of the Moran Process on Undirected Graphs

Authors: Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Martin A. Nowak

Abstract: Evolutionary graph theory studies the evolutionary dynamics in a population structure given as a connected graph. Each node of the graph represents an individual of the population, and edges determine how offspring are placed. We consider the classical birth-death Moran process where there are two types of individuals, namely, the residents with fitness 1 and mutants with fitness r. The fitness in… ▽ More Evolutionary graph theory studies the evolutionary dynamics in a population structure given as a connected graph. Each node of the graph represents an individual of the population, and edges determine how offspring are placed. We consider the classical birth-death Moran process where there are two types of individuals, namely, the residents with fitness 1 and mutants with fitness r. The fitness indicates the reproductive strength. The evolutionary dynamics happens as follows: in the initial step, in a population of all resident individuals a mutant is introduced, and then at each step, an individual is chosen proportional to the fitness of its type to reproduce, and the offspring replaces a neighbor uniformly at random. The process stops when all individuals are either residents or mutants. The probability that all individuals in the end are mutants is called the fixation probability. We present faster polynomial-time Monte-Carlo algorithms for finidng the fixation probability on undirected graphs. Our algorithms are always at least a factor O(n^2/log n) faster as compared to the previous algorithms, where n is the number of nodes, and is polynomial even if r is given in binary. We also present lower bounds showing that the upper bound on the expected number of effective steps we present is asymptotically tight for undirected graphs. △ Less

Submitted 21 June, 2017; originally announced June 2017.