TY - JOUR AB - We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates "almost surely". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice. Like others, we use variant functions (a.k.a. "super-martingales") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains. AU - Mciver, Annabelle AU - Morgan, Carroll AU - Kaminski, Benjamin Lucien AU - Katoen, Joost P ID - 10418 IS - POPL JF - Proceedings of the ACM on Programming Languages TI - A new proof rule for almost-sure termination VL - 2 ER - TY - CONF AB - There has been renewed interest in modelling the behaviour of evolutionary algorithms by more traditional mathematical objects, such as ordinary differential equations or Markov chains. The advantage is that the analysis becomes greatly facilitated due to the existence of well established methods. However, this typically comes at the cost of disregarding information about the process. Here, we introduce the use of stochastic differential equations (SDEs) for the study of EAs. SDEs can produce simple analytical results for the dynamics of stochastic processes, unlike Markov chains which can produce rigorous but unwieldy expressions about the dynamics. On the other hand, unlike ordinary differential equations (ODEs), they do not discard information about the stochasticity of the process. We show that these are especially suitable for the analysis of fixed budget scenarios and present analogs of the additive and multiplicative drift theorems for SDEs. We exemplify the use of these methods for two model algorithms ((1+1) EA and RLS) on two canonical problems(OneMax and LeadingOnes). AU - Paixao, Tiago AU - Pérez Heredia, Jorge ID - 1112 SN - 978-145034651-1 T2 - Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms TI - An application of stochastic differential equations to evolutionary algorithms ER - TY - CONF AB - We study space complexity and time-space trade-offs with a focus not on peak memory usage but on overall memory consumption throughout the computation. Such a cumulative space measure was introduced for the computational model of parallel black pebbling by [Alwen and Serbinenko ’15] as a tool for obtaining results in cryptography. We consider instead the non- deterministic black-white pebble game and prove optimal cumulative space lower bounds and trade-offs, where in order to minimize pebbling time the space has to remain large during a significant fraction of the pebbling. We also initiate the study of cumulative space in proof complexity, an area where other space complexity measures have been extensively studied during the last 10–15 years. Using and extending the connection between proof complexity and pebble games in [Ben-Sasson and Nordström ’08, ’11] we obtain several strong cumulative space results for (even parallel versions of) the resolution proof system, and outline some possible future directions of study of this, in our opinion, natural and interesting space measure. AU - Alwen, Joel F AU - De Rezende, Susanna AU - Nordstrom, Jakob AU - Vinyals, Marc ED - Papadimitriou, Christos ID - 1175 SN - 18688969 TI - Cumulative space in black-white pebbling and resolution VL - 67 ER - TY - JOUR AB - Variation in genotypes may be responsible for differences in dispersal rates, directional biases, and growth rates of individuals. These traits may favor certain genotypes and enhance their spatiotemporal spreading into areas occupied by the less advantageous genotypes. We study how these factors influence the speed of spreading in the case of two competing genotypes under the assumption that spatial variation of the total population is small compared to the spatial variation of the frequencies of the genotypes in the population. In that case, the dynamics of the frequency of one of the genotypes is approximately described by a generalized Fisher–Kolmogorov–Petrovskii–Piskunov (F–KPP) equation. This generalized F–KPP equation with (nonlinear) frequency-dependent diffusion and advection terms admits traveling wave solutions that characterize the invasion of the dominant genotype. Our existence results generalize the classical theory for traveling waves for the F–KPP with constant coefficients. Moreover, in the particular case of the quadratic (monostable) nonlinear growth–decay rate in the generalized F–KPP we study in detail the influence of the variance in diffusion and mean displacement rates of the two genotypes on the minimal wave propagation speed. AU - Kollár, Richard AU - Novak, Sebastian ID - 1191 IS - 3 JF - Bulletin of Mathematical Biology TI - Existence of traveling waves for the generalized F–KPP equation VL - 79 ER - TY - JOUR AB - Systems such as fluid flows in channels and pipes or the complex Ginzburg–Landau system, defined over periodic domains, exhibit both continuous symmetries, translational and rotational, as well as discrete symmetries under spatial reflections or complex conjugation. The simplest, and very common symmetry of this type is the equivariance of the defining equations under the orthogonal group O(2). We formulate a novel symmetry reduction scheme for such systems by combining the method of slices with invariant polynomial methods, and show how it works by applying it to the Kuramoto–Sivashinsky system in one spatial dimension. As an example, we track a relative periodic orbit through a sequence of bifurcations to the onset of chaos. Within the symmetry-reduced state space we are able to compute and visualize the unstable manifolds of relative periodic orbits, their torus bifurcations, a transition to chaos via torus breakdown, and heteroclinic connections between various relative periodic orbits. It would be very hard to carry through such analysis in the full state space, without a symmetry reduction such as the one we present here. AU - Budanur, Nazmi B AU - Cvitanović, Predrag ID - 1211 IS - 3-4 JF - Journal of Statistical Physics TI - Unstable manifolds of relative periodic orbits in the symmetry reduced state space of the Kuramoto–Sivashinsky system VL - 167 ER -