---
_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'
...