--- _id: '10418' abstract: - lang: eng text: 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. acknowledgement: "McIver and Morgan are grateful to David Basin and the Information Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during part of which this work began. And thanks particularly to Andreas Lochbihler, who shared with us the probabilistic termination problem that led to it. They acknowledge the support of ARC grant DP140101119. Part of this work was carried out during the Workshop on Probabilistic Programming Semantics\r\nat McGill University’s Bellairs Research Institute on Barbados organised by Alexandra Silva and\r\nPrakash Panangaden. Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4." article_number: '33' article_processing_charge: No article_type: original author: - first_name: Annabelle full_name: Mciver, Annabelle last_name: Mciver - first_name: Carroll full_name: Morgan, Carroll last_name: Morgan - first_name: Benjamin Lucien full_name: Kaminski, Benjamin Lucien last_name: Kaminski - first_name: Joost P full_name: Katoen, Joost P id: 4524F760-F248-11E8-B48F-1D18A9856A87 last_name: Katoen citation: ama: Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2017;2(POPL). doi:10.1145/3158121 apa: 'Mciver, A., Morgan, C., Kaminski, B. L., & Katoen, J. P. (2017). A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. Los Angeles, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3158121' chicago: Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost P Katoen. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the ACM on Programming Languages. Association for Computing Machinery, 2017. https://doi.org/10.1145/3158121. ieee: A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule for almost-sure termination,” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL. Association for Computing Machinery, 2017. ista: Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33. mla: Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, 33, Association for Computing Machinery, 2017, doi:10.1145/3158121. short: A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM on Programming Languages 2 (2017). conference: end_date: 2018-01-13 location: Los Angeles, CA, United States name: 'POPL: Programming Languages' start_date: 2018-01-07 date_created: 2021-12-05T23:01:49Z date_published: 2017-12-07T00:00:00Z date_updated: 2021-12-07T08:04:14Z day: '07' department: - _id: KrCh - _id: ToHe doi: 10.1145/3158121 external_id: arxiv: - '1711.03588' intvolume: ' 2' issue: POPL language: - iso: eng main_file_link: - open_access: '1' url: https://dl.acm.org/doi/10.1145/3158121 month: '12' oa: 1 oa_version: Published Version publication: Proceedings of the ACM on Programming Languages publication_identifier: eissn: - 2475-1421 publication_status: published publisher: Association for Computing Machinery quality_controlled: '1' scopus_import: '1' status: public title: A new proof rule for almost-sure termination type: journal_article user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9 volume: 2 year: '2017' ... --- _id: '1112' abstract: - lang: eng text: 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). author: - first_name: Tiago full_name: Paixao, Tiago id: 2C5658E6-F248-11E8-B48F-1D18A9856A87 last_name: Paixao orcid: 0000-0003-2361-3953 - first_name: Jorge full_name: Pérez Heredia, Jorge last_name: Pérez Heredia citation: ama: 'Paixao T, Pérez Heredia J. An application of stochastic differential equations to evolutionary algorithms. In: Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms. ACM; 2017:3-11. doi:10.1145/3040718.3040729' apa: 'Paixao, T., & Pérez Heredia, J. (2017). An application of stochastic differential equations to evolutionary algorithms. In Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms (pp. 3–11). Copenhagen, Denmark: ACM. https://doi.org/10.1145/3040718.3040729' chicago: Paixao, Tiago, and Jorge Pérez Heredia. “An Application of Stochastic Differential Equations to Evolutionary Algorithms.” In Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms, 3–11. ACM, 2017. https://doi.org/10.1145/3040718.3040729. ieee: T. Paixao and J. Pérez Heredia, “An application of stochastic differential equations to evolutionary algorithms,” in Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms, Copenhagen, Denmark, 2017, pp. 3–11. ista: 'Paixao T, Pérez Heredia J. 2017. An application of stochastic differential equations to evolutionary algorithms. Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms. FOGA: Foundations of Genetic Algorithms, 3–11.' mla: Paixao, Tiago, and Jorge Pérez Heredia. “An Application of Stochastic Differential Equations to Evolutionary Algorithms.” Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms, ACM, 2017, pp. 3–11, doi:10.1145/3040718.3040729. short: T. Paixao, J. Pérez Heredia, in:, Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms, ACM, 2017, pp. 3–11. conference: end_date: 2017-01-15 location: Copenhagen, Denmark name: 'FOGA: Foundations of Genetic Algorithms' start_date: 2017-01-12 date_created: 2018-12-11T11:50:12Z date_published: 2017-01-12T00:00:00Z date_updated: 2021-01-12T06:48:22Z day: '12' department: - _id: NiBa doi: 10.1145/3040718.3040729 language: - iso: eng month: '01' oa_version: None page: 3 - 11 publication: Proceedings of the 14th ACM/SIGEVO Conference on Foundations of Genetic Algorithms publication_identifier: isbn: - 978-145034651-1 publication_status: published publisher: ACM publist_id: '6255' quality_controlled: '1' scopus_import: 1 status: public title: An application of stochastic differential equations to evolutionary algorithms type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2017' ... --- _id: '1175' abstract: - lang: eng text: 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. alternative_title: - LIPIcs author: - first_name: Joel F full_name: Alwen, Joel F id: 2A8DFA8C-F248-11E8-B48F-1D18A9856A87 last_name: Alwen - first_name: Susanna full_name: De Rezende, Susanna last_name: De Rezende - first_name: Jakob full_name: Nordstrom, Jakob last_name: Nordstrom - first_name: Marc full_name: Vinyals, Marc last_name: Vinyals citation: ama: 'Alwen JF, De Rezende S, Nordstrom J, Vinyals M. Cumulative space in black-white pebbling and resolution. In: Papadimitriou C, ed. Vol 67. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017:38:1-38-21. doi:10.4230/LIPIcs.ITCS.2017.38' apa: 'Alwen, J. F., De Rezende, S., Nordstrom, J., & Vinyals, M. (2017). Cumulative space in black-white pebbling and resolution. In C. Papadimitriou (Ed.) (Vol. 67, p. 38:1-38-21). Presented at the ITCS: Innovations in Theoretical Computer Science, Berkeley, CA, United States: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.ITCS.2017.38' chicago: Alwen, Joel F, Susanna De Rezende, Jakob Nordstrom, and Marc Vinyals. “Cumulative Space in Black-White Pebbling and Resolution.” edited by Christos Papadimitriou, 67:38:1-38-21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. https://doi.org/10.4230/LIPIcs.ITCS.2017.38. ieee: 'J. F. Alwen, S. De Rezende, J. Nordstrom, and M. Vinyals, “Cumulative space in black-white pebbling and resolution,” presented at the ITCS: Innovations in Theoretical Computer Science, Berkeley, CA, United States, 2017, vol. 67, p. 38:1-38-21.' ista: 'Alwen JF, De Rezende S, Nordstrom J, Vinyals M. 2017. Cumulative space in black-white pebbling and resolution. ITCS: Innovations in Theoretical Computer Science, LIPIcs, vol. 67, 38:1-38-21.' mla: Alwen, Joel F., et al. Cumulative Space in Black-White Pebbling and Resolution. Edited by Christos Papadimitriou, vol. 67, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, p. 38:1-38-21, doi:10.4230/LIPIcs.ITCS.2017.38. short: J.F. Alwen, S. De Rezende, J. Nordstrom, M. Vinyals, in:, C. Papadimitriou (Ed.), Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017, p. 38:1-38-21. conference: end_date: 2017-01-11 location: Berkeley, CA, United States name: 'ITCS: Innovations in Theoretical Computer Science' start_date: 2017-01-09 date_created: 2018-12-11T11:50:33Z date_published: 2017-01-01T00:00:00Z date_updated: 2021-01-12T06:48:51Z day: '01' ddc: - '005' - '600' department: - _id: KrPi doi: 10.4230/LIPIcs.ITCS.2017.38 editor: - first_name: Christos full_name: Papadimitriou, Christos last_name: Papadimitriou file: - access_level: open_access checksum: dbc94810be07c2fb1945d5c2a6130e6c content_type: application/pdf creator: system date_created: 2018-12-12T10:17:11Z date_updated: 2020-07-14T12:44:37Z file_id: '5263' file_name: IST-2018-927-v1+1_LIPIcs-ITCS-2017-38.pdf file_size: 557769 relation: main_file file_date_updated: 2020-07-14T12:44:37Z has_accepted_license: '1' intvolume: ' 67' language: - iso: eng license: https://creativecommons.org/licenses/by/4.0/ month: '01' oa: 1 oa_version: Published Version page: 38:1-38-21 publication_identifier: issn: - '18688969' publication_status: published publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik publist_id: '6179' pubrep_id: '927' quality_controlled: '1' scopus_import: 1 status: public title: Cumulative space in black-white pebbling and resolution tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 67 year: '2017' ... --- _id: '1191' abstract: - lang: eng text: 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. acknowledgement: "We thank Nick Barton, Katarína Bod’ová, and Sr\r\n-\r\ndan Sarikas for constructive feed-\r\nback and support. Furthermore, we would like to express our deep gratitude to the anonymous referees (one\r\nof whom, Jimmy Garnier, agreed to reveal his identity) and the editor Max Souza, for very helpful and\r\ndetailed comments and suggestions that significantly helped us to improve the manuscript. This project has\r\nreceived funding from the European Union’s Seventh Framework Programme for research, technological\r\ndevelopment and demonstration under Grant Agreement 618091 Speed of Adaptation in Population Genet-\r\nics and Evolutionary Computation (SAGE) and the European Research Council (ERC) Grant No. 250152\r\n(SN), from the Scientific Grant Agency of the Slovak Republic under the Grant 1/0459/13 and by the Slovak\r\nResearch and Development Agency under the Contract No. APVV-14-0378 (RK). RK would also like to\r\nthank IST Austria for its hospitality during the work on this project." author: - first_name: Richard full_name: Kollár, Richard last_name: Kollár - first_name: Sebastian full_name: Novak, Sebastian id: 461468AE-F248-11E8-B48F-1D18A9856A87 last_name: Novak citation: ama: Kollár R, Novak S. Existence of traveling waves for the generalized F–KPP equation. Bulletin of Mathematical Biology. 2017;79(3):525-559. doi:10.1007/s11538-016-0244-3 apa: Kollár, R., & Novak, S. (2017). Existence of traveling waves for the generalized F–KPP equation. Bulletin of Mathematical Biology. Springer. https://doi.org/10.1007/s11538-016-0244-3 chicago: Kollár, Richard, and Sebastian Novak. “Existence of Traveling Waves for the Generalized F–KPP Equation.” Bulletin of Mathematical Biology. Springer, 2017. https://doi.org/10.1007/s11538-016-0244-3. ieee: R. Kollár and S. Novak, “Existence of traveling waves for the generalized F–KPP equation,” Bulletin of Mathematical Biology, vol. 79, no. 3. Springer, pp. 525–559, 2017. ista: Kollár R, Novak S. 2017. Existence of traveling waves for the generalized F–KPP equation. Bulletin of Mathematical Biology. 79(3), 525–559. mla: Kollár, Richard, and Sebastian Novak. “Existence of Traveling Waves for the Generalized F–KPP Equation.” Bulletin of Mathematical Biology, vol. 79, no. 3, Springer, 2017, pp. 525–59, doi:10.1007/s11538-016-0244-3. short: R. Kollár, S. Novak, Bulletin of Mathematical Biology 79 (2017) 525–559. date_created: 2018-12-11T11:50:38Z date_published: 2017-03-01T00:00:00Z date_updated: 2021-01-12T06:48:58Z day: '01' department: - _id: NiBa doi: 10.1007/s11538-016-0244-3 ec_funded: 1 intvolume: ' 79' issue: '3' language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/1607.00944 month: '03' oa: 1 oa_version: Preprint page: 525-559 project: - _id: 25B1EC9E-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '618091' name: Speed of Adaptation in Population Genetics and Evolutionary Computation - _id: 25B07788-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '250152' name: Limits to selection in biology and in evolutionary computation publication: Bulletin of Mathematical Biology publication_status: published publisher: Springer publist_id: '6160' quality_controlled: '1' scopus_import: 1 status: public title: Existence of traveling waves for the generalized F–KPP equation type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 79 year: '2017' ... --- _id: '1211' abstract: - lang: eng text: 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. acknowledgement: 'This work was supported by the family of late G. Robinson, Jr. and NSF Grant DMS-1211827. ' author: - first_name: Nazmi B full_name: Budanur, Nazmi B id: 3EA1010E-F248-11E8-B48F-1D18A9856A87 last_name: Budanur orcid: 0000-0003-0423-5010 - first_name: Predrag full_name: Cvitanović, Predrag last_name: Cvitanović citation: ama: Budanur NB, Cvitanović P. Unstable manifolds of relative periodic orbits in the symmetry reduced state space of the Kuramoto–Sivashinsky system. Journal of Statistical Physics. 2017;167(3-4):636-655. doi:10.1007/s10955-016-1672-z apa: Budanur, N. B., & Cvitanović, P. (2017). Unstable manifolds of relative periodic orbits in the symmetry reduced state space of the Kuramoto–Sivashinsky system. Journal of Statistical Physics. Springer. https://doi.org/10.1007/s10955-016-1672-z chicago: Budanur, Nazmi B, and Predrag Cvitanović. “Unstable Manifolds of Relative Periodic Orbits in the Symmetry Reduced State Space of the Kuramoto–Sivashinsky System.” Journal of Statistical Physics. Springer, 2017. https://doi.org/10.1007/s10955-016-1672-z. ieee: N. B. Budanur and P. Cvitanović, “Unstable manifolds of relative periodic orbits in the symmetry reduced state space of the Kuramoto–Sivashinsky system,” Journal of Statistical Physics, vol. 167, no. 3–4. Springer, pp. 636–655, 2017. ista: Budanur NB, Cvitanović P. 2017. Unstable manifolds of relative periodic orbits in the symmetry reduced state space of the Kuramoto–Sivashinsky system. Journal of Statistical Physics. 167(3–4), 636–655. mla: Budanur, Nazmi B., and Predrag Cvitanović. “Unstable Manifolds of Relative Periodic Orbits in the Symmetry Reduced State Space of the Kuramoto–Sivashinsky System.” Journal of Statistical Physics, vol. 167, no. 3–4, Springer, 2017, pp. 636–55, doi:10.1007/s10955-016-1672-z. short: N.B. Budanur, P. Cvitanović, Journal of Statistical Physics 167 (2017) 636–655. date_created: 2018-12-11T11:50:44Z date_published: 2017-05-01T00:00:00Z date_updated: 2021-01-12T06:49:07Z day: '01' ddc: - '530' department: - _id: BjHo doi: 10.1007/s10955-016-1672-z file: - access_level: open_access checksum: 3e971d09eb167761aa0888ed415b0056 content_type: application/pdf creator: system date_created: 2018-12-12T10:18:01Z date_updated: 2020-07-14T12:44:39Z file_id: '5319' file_name: IST-2017-782-v1+1_BudCvi15.pdf file_size: 2820207 relation: main_file file_date_updated: 2020-07-14T12:44:39Z has_accepted_license: '1' intvolume: ' 167' issue: 3-4 language: - iso: eng month: '05' oa: 1 oa_version: Submitted Version page: 636-655 publication: Journal of Statistical Physics publication_status: published publisher: Springer publist_id: '6136' pubrep_id: '782' quality_controlled: '1' scopus_import: 1 status: public title: Unstable manifolds of relative periodic orbits in the symmetry reduced state space of the Kuramoto–Sivashinsky system type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 167 year: '2017' ...