---
_id: '48871'
abstract:
- lang: eng
  text: 'Most runtime analyses of randomised search heuristics focus on the expected
    number of function evaluations to find a unique global optimum. We ask a fundamental
    question: if additional search points are declared optimal, or declared as desirable
    target points, do these additional optima speed up evolutionary algorithms? More
    formally, we analyse the expected hitting time of a target set OPT{$\cup$}S where
    S is a set of non-optimal search points and OPT is the set of optima and compare
    it to the expected hitting time of OPT. We show that the answer to our question
    depends on the number and placement of search points in S. For all black-box algorithms
    and all fitness functions with polynomial expected optimisation times we show
    that, if additional optima are placed randomly, even an exponential number of
    optima has a negligible effect on the expected optimisation time. Considering
    Hamming balls around all global optima gives an easier target for some algorithms
    and functions and can shift the phase transition with respect to offspring population
    sizes in the (1,{$\lambda$}) EA on OneMax. However, for the one-dimensional Ising
    model the time to reach Hamming balls of radius (1/2-{$ϵ$})n around optima does
    not reduce the asymptotic expected optimisation time in the worst case. Finally,
    on functions where search trajectories typically join in a single search point,
    turning one search point into an optimum drastically reduces the expected optimisation
    time.'
author:
- first_name: Jakob
  full_name: Bossek, Jakob
  id: '102979'
  last_name: Bossek
  orcid: 0000-0002-4121-4668
- first_name: Dirk
  full_name: Sudholt, Dirk
  last_name: Sudholt
citation:
  ama: Bossek J, Sudholt D. Do Additional Target Points Speed Up Evolutionary Algorithms?
    <i>Theoretical Computer Science</i>. Published online 2023:113757. doi:<a href="https://doi.org/10.1016/j.tcs.2023.113757">10.1016/j.tcs.2023.113757</a>
  apa: Bossek, J., &#38; Sudholt, D. (2023). Do Additional Target Points Speed Up
    Evolutionary Algorithms? <i>Theoretical Computer Science</i>, 113757. <a href="https://doi.org/10.1016/j.tcs.2023.113757">https://doi.org/10.1016/j.tcs.2023.113757</a>
  bibtex: '@article{Bossek_Sudholt_2023, title={Do Additional Target Points Speed
    Up Evolutionary Algorithms?}, DOI={<a href="https://doi.org/10.1016/j.tcs.2023.113757">10.1016/j.tcs.2023.113757</a>},
    journal={Theoretical Computer Science}, author={Bossek, Jakob and Sudholt, Dirk},
    year={2023}, pages={113757} }'
  chicago: Bossek, Jakob, and Dirk Sudholt. “Do Additional Target Points Speed Up
    Evolutionary Algorithms?” <i>Theoretical Computer Science</i>, 2023, 113757. <a
    href="https://doi.org/10.1016/j.tcs.2023.113757">https://doi.org/10.1016/j.tcs.2023.113757</a>.
  ieee: 'J. Bossek and D. Sudholt, “Do Additional Target Points Speed Up Evolutionary
    Algorithms?,” <i>Theoretical Computer Science</i>, p. 113757, 2023, doi: <a href="https://doi.org/10.1016/j.tcs.2023.113757">10.1016/j.tcs.2023.113757</a>.'
  mla: Bossek, Jakob, and Dirk Sudholt. “Do Additional Target Points Speed Up Evolutionary
    Algorithms?” <i>Theoretical Computer Science</i>, 2023, p. 113757, doi:<a href="https://doi.org/10.1016/j.tcs.2023.113757">10.1016/j.tcs.2023.113757</a>.
  short: J. Bossek, D. Sudholt, Theoretical Computer Science (2023) 113757.
date_created: 2023-11-14T15:58:56Z
date_updated: 2023-12-13T10:51:07Z
department:
- _id: '819'
doi: 10.1016/j.tcs.2023.113757
keyword:
- Evolutionary algorithms
- pseudo-Boolean functions
- runtime analysis
language:
- iso: eng
page: '113757'
publication: Theoretical Computer Science
publication_identifier:
  issn:
  - 0304-3975
status: public
title: Do Additional Target Points Speed Up Evolutionary Algorithms?
type: journal_article
user_id: '102979'
year: '2023'
...
---
_id: '48862'
abstract:
- lang: eng
  text: 'Most runtime analyses of randomised search heuristics focus on the expected
    number of function evaluations to find a unique global optimum. We ask a fundamental
    question: if additional search points are declared optimal, or declared as desirable
    target points, do these additional optima speed up evolutionary algorithms? More
    formally, we analyse the expected hitting time of a target set OPT {$\cup$} S
    where S is a set of non-optimal search points and OPT is the set of optima and
    compare it to the expected hitting time of OPT. We show that the answer to our
    question depends on the number and placement of search points in S. For all black-box
    algorithms and all fitness functions we show that, if additional optima are placed
    randomly, even an exponential number of optima has a negligible effect on the
    expected optimisation time. Considering Hamming balls around all global optima
    gives an easier target for some algorithms and functions and can shift the phase
    transition with respect to offspring population sizes in the (1,{$\lambda$}) EA
    on One-Max. Finally, on functions where search trajectories typically join in
    a single search point, turning one search point into an optimum drastically reduces
    the expected optimisation time.'
author:
- first_name: Jakob
  full_name: Bossek, Jakob
  id: '102979'
  last_name: Bossek
  orcid: 0000-0002-4121-4668
- first_name: Dirk
  full_name: Sudholt, Dirk
  last_name: Sudholt
citation:
  ama: 'Bossek J, Sudholt D. Do Additional Optima Speed up Evolutionary Algorithms?
    In: <i>Proceedings of the 16th ACM/SIGEVO Conference on Foundations of Genetic
    Algorithms</i>. Association for Computing Machinery; 2021:1–11.'
  apa: Bossek, J., &#38; Sudholt, D. (2021). Do Additional Optima Speed up Evolutionary
    Algorithms? In <i>Proceedings of the 16th ACM/SIGEVO Conference on Foundations
    of Genetic Algorithms</i> (pp. 1–11). Association for Computing Machinery.
  bibtex: '@inbook{Bossek_Sudholt_2021, place={New York, NY, USA}, title={Do Additional
    Optima Speed up Evolutionary Algorithms?}, booktitle={Proceedings of the 16th
    ACM/SIGEVO Conference on Foundations of Genetic Algorithms}, publisher={Association
    for Computing Machinery}, author={Bossek, Jakob and Sudholt, Dirk}, year={2021},
    pages={1–11} }'
  chicago: 'Bossek, Jakob, and Dirk Sudholt. “Do Additional Optima Speed up Evolutionary
    Algorithms?” In <i>Proceedings of the 16th ACM/SIGEVO Conference on Foundations
    of Genetic Algorithms</i>, 1–11. New York, NY, USA: Association for Computing
    Machinery, 2021.'
  ieee: 'J. Bossek and D. Sudholt, “Do Additional Optima Speed up Evolutionary Algorithms?,”
    in <i>Proceedings of the 16th ACM/SIGEVO Conference on Foundations of Genetic
    Algorithms</i>, New York, NY, USA: Association for Computing Machinery, 2021,
    pp. 1–11.'
  mla: Bossek, Jakob, and Dirk Sudholt. “Do Additional Optima Speed up Evolutionary
    Algorithms?” <i>Proceedings of the 16th ACM/SIGEVO Conference on Foundations of
    Genetic Algorithms</i>, Association for Computing Machinery, 2021, pp. 1–11.
  short: 'J. Bossek, D. Sudholt, in: Proceedings of the 16th ACM/SIGEVO Conference
    on Foundations of Genetic Algorithms, Association for Computing Machinery, New
    York, NY, USA, 2021, pp. 1–11.'
date_created: 2023-11-14T15:58:55Z
date_updated: 2023-12-13T10:45:31Z
department:
- _id: '819'
extern: '1'
keyword:
- evolutionary algorithms
- pseudo-boolean functions
- runtime analysis
- theory
language:
- iso: eng
page: 1–11
place: New York, NY, USA
publication: Proceedings of the 16th ACM/SIGEVO Conference on Foundations of Genetic
  Algorithms
publication_identifier:
  isbn:
  - 978-1-4503-8352-3
publication_status: published
publisher: Association for Computing Machinery
status: public
title: Do Additional Optima Speed up Evolutionary Algorithms?
type: book_chapter
user_id: '102979'
year: '2021'
...
---
_id: '39061'
abstract:
- lang: eng
  text: This article presents an approach, which combines theorem proving-based refinement
    with model checking for state based real-time systems. Our verification flow starts
    from UML state diagrams, which are translated to the formal B language and are
    model checked for real-time properties. By means of the B language and a B theorem
    prover, refined state diagrams are verified against their abstract representation.
    The approach is presented by means of the refinement of a digital echo cancellation
    unit.
author:
- first_name: Alexander
  full_name: Krupp, Alexander
  last_name: Krupp
- first_name: Wolfgang
  full_name: Müller, Wolfgang
  id: '16243'
  last_name: Müller
- first_name: Ian
  full_name: Oliver, Ian
  last_name: Oliver
citation:
  ama: 'Krupp A, Müller W, Oliver I. Formal Refinement and Model Checking of An Echo
    Cancellation Unit. In: <i>Proceedings of DATE’04 Designers’ Forum</i>. ; 2004.
    doi:<a href="https://doi.org/10.1109/DATE.2004.1269214">10.1109/DATE.2004.1269214</a>'
  apa: Krupp, A., Müller, W., &#38; Oliver, I. (2004). Formal Refinement and Model
    Checking of An Echo Cancellation Unit. <i>Proceedings of DATE’04 Designers’ Forum</i>.
    Proceedings Design, Automation and Test in Europe Conference and Exhibition. <a
    href="https://doi.org/10.1109/DATE.2004.1269214">https://doi.org/10.1109/DATE.2004.1269214</a>
  bibtex: '@inproceedings{Krupp_Müller_Oliver_2004, place={Paris}, title={Formal Refinement
    and Model Checking of An Echo Cancellation Unit}, DOI={<a href="https://doi.org/10.1109/DATE.2004.1269214">10.1109/DATE.2004.1269214</a>},
    booktitle={Proceedings of DATE’04 Designers’ Forum}, author={Krupp, Alexander
    and Müller, Wolfgang and Oliver, Ian}, year={2004} }'
  chicago: Krupp, Alexander, Wolfgang Müller, and Ian Oliver. “Formal Refinement and
    Model Checking of An Echo Cancellation Unit.” In <i>Proceedings of DATE’04 Designers’
    Forum</i>. Paris, 2004. <a href="https://doi.org/10.1109/DATE.2004.1269214">https://doi.org/10.1109/DATE.2004.1269214</a>.
  ieee: 'A. Krupp, W. Müller, and I. Oliver, “Formal Refinement and Model Checking
    of An Echo Cancellation Unit,” presented at the Proceedings Design, Automation
    and Test in Europe Conference and Exhibition, 2004, doi: <a href="https://doi.org/10.1109/DATE.2004.1269214">10.1109/DATE.2004.1269214</a>.'
  mla: Krupp, Alexander, et al. “Formal Refinement and Model Checking of An Echo Cancellation
    Unit.” <i>Proceedings of DATE’04 Designers’ Forum</i>, 2004, doi:<a href="https://doi.org/10.1109/DATE.2004.1269214">10.1109/DATE.2004.1269214</a>.
  short: 'A. Krupp, W. Müller, I. Oliver, in: Proceedings of DATE’04 Designers’ Forum,
    Paris, 2004.'
conference:
  name: Proceedings Design, Automation and Test in Europe Conference and Exhibition
date_created: 2023-01-24T08:53:26Z
date_updated: 2023-01-24T08:53:31Z
department:
- _id: '672'
doi: 10.1109/DATE.2004.1269214
keyword:
- Echo cancellers
- Logic
- Unified modeling language
- Automata
- Data structures
- Boolean functions
- Electronic design automation and methodology
- Prototypes
- Specification languages
- Constraint theory
language:
- iso: eng
place: Paris
publication: Proceedings of DATE’04 Designers' Forum
publication_identifier:
  isbn:
  - 0-7695-2085-5
status: public
title: Formal Refinement and Model Checking of An Echo Cancellation Unit
type: conference
user_id: '5786'
year: '2004'
...
---
_id: '39069'
abstract:
- lang: eng
  text: We present the syntax and semantics of a past- and future-oriented temporal
    extension of the Object Constraint Language (OCL). Our extension supports designers
    to express time-bounded properties over a state-oriented UML model of a system
    under development. The semantics is formally defined over the system states of
    a mathematical object model. Additionally, we present a mapping to Clocked Linear
    Temporal Logic (Clocked LTL) formulae, which is the basis for further application
    in verification with model checking. We demonstrate the applicability of the approach
    by the example of a buffer specification in the context of a production system.
author:
- first_name: Stephan
  full_name: Flake, Stephan
  last_name: Flake
- first_name: Wolfgang
  full_name: Müller, Wolfgang
  id: '16243'
  last_name: Müller
citation:
  ama: 'Flake S, Müller W. Past- and Future-Oriented Time-Bound Temporal Properties
    with OCL. In: <i>Proceedings of SEFM´04</i>. IEEE; 2004. doi:<a href="https://doi.org/10.1109/SEFM.2004.1347516">10.1109/SEFM.2004.1347516</a>'
  apa: Flake, S., &#38; Müller, W. (2004). Past- and Future-Oriented Time-Bound Temporal
    Properties with OCL. <i>Proceedings of SEFM´04</i>.  Proceedings of the Second
    International Conference on Software Engineering and Formal Methods. <a href="https://doi.org/10.1109/SEFM.2004.1347516">https://doi.org/10.1109/SEFM.2004.1347516</a>
  bibtex: '@inproceedings{Flake_Müller_2004, place={Beijing, China}, title={Past-
    and Future-Oriented Time-Bound Temporal Properties with OCL}, DOI={<a href="https://doi.org/10.1109/SEFM.2004.1347516">10.1109/SEFM.2004.1347516</a>},
    booktitle={Proceedings of SEFM´04}, publisher={IEEE}, author={Flake, Stephan and
    Müller, Wolfgang}, year={2004} }'
  chicago: 'Flake, Stephan, and Wolfgang Müller. “Past- and Future-Oriented Time-Bound
    Temporal Properties with OCL.” In <i>Proceedings of SEFM´04</i>. Beijing, China:
    IEEE, 2004. <a href="https://doi.org/10.1109/SEFM.2004.1347516">https://doi.org/10.1109/SEFM.2004.1347516</a>.'
  ieee: 'S. Flake and W. Müller, “Past- and Future-Oriented Time-Bound Temporal Properties
    with OCL,” presented at the  Proceedings of the Second International Conference
    on Software Engineering and Formal Methods, 2004, doi: <a href="https://doi.org/10.1109/SEFM.2004.1347516">10.1109/SEFM.2004.1347516</a>.'
  mla: Flake, Stephan, and Wolfgang Müller. “Past- and Future-Oriented Time-Bound
    Temporal Properties with OCL.” <i>Proceedings of SEFM´04</i>, IEEE, 2004, doi:<a
    href="https://doi.org/10.1109/SEFM.2004.1347516">10.1109/SEFM.2004.1347516</a>.
  short: 'S. Flake, W. Müller, in: Proceedings of SEFM´04, IEEE, Beijing, China, 2004.'
conference:
  name: ' Proceedings of the Second International Conference on Software Engineering
    and Formal Methods'
date_created: 2023-01-24T09:03:36Z
date_updated: 2023-01-24T09:03:41Z
department:
- _id: '672'
doi: 10.1109/SEFM.2004.1347516
keyword:
- Unified modeling language
- Logic
- Clocks
- Boolean functions
- Application software
- Time factors
- Real time systems
- Formal verification
- Buffer storage
- Software packages
language:
- iso: eng
place: Beijing, China
publication: Proceedings of SEFM´04
publication_identifier:
  isbn:
  - 0-7695-2222-X
publisher: IEEE
status: public
title: Past- and Future-Oriented Time-Bound Temporal Properties with OCL
type: conference
user_id: '5786'
year: '2004'
...