@article{48871,
  abstract     = {{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       = {{Bossek, Jakob and Sudholt, Dirk}},
  issn         = {{0304-3975}},
  journal      = {{Theoretical Computer Science}},
  keywords     = {{Evolutionary algorithms, pseudo-Boolean functions, runtime analysis}},
  pages        = {{113757}},
  title        = {{{Do Additional Target Points Speed Up Evolutionary Algorithms?}}},
  doi          = {{10.1016/j.tcs.2023.113757}},
  year         = {{2023}},
}

@inbook{48862,
  abstract     = {{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       = {{Bossek, Jakob and Sudholt, Dirk}},
  booktitle    = {{Proceedings of the 16th ACM/SIGEVO Conference on Foundations of Genetic Algorithms}},
  isbn         = {{978-1-4503-8352-3}},
  keywords     = {{evolutionary algorithms, pseudo-boolean functions, runtime analysis, theory}},
  pages        = {{1–11}},
  publisher    = {{Association for Computing Machinery}},
  title        = {{{Do Additional Optima Speed up Evolutionary Algorithms?}}},
  year         = {{2021}},
}

@inproceedings{39061,
  abstract     = {{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       = {{Krupp, Alexander and Müller, Wolfgang and Oliver, Ian}},
  booktitle    = {{Proceedings of DATE’04 Designers' Forum}},
  isbn         = {{0-7695-2085-5}},
  keywords     = {{Echo cancellers, Logic, Unified modeling language, Automata, Data structures, Boolean functions, Electronic design automation and methodology, Prototypes, Specification languages, Constraint theory}},
  title        = {{{Formal Refinement and Model Checking of An Echo Cancellation Unit}}},
  doi          = {{10.1109/DATE.2004.1269214}},
  year         = {{2004}},
}

@inproceedings{39069,
  abstract     = {{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       = {{Flake, Stephan and Müller, Wolfgang}},
  booktitle    = {{Proceedings of SEFM´04}},
  isbn         = {{0-7695-2222-X}},
  keywords     = {{Unified modeling language, Logic, Clocks, Boolean functions, Application software, Time factors, Real time systems, Formal verification, Buffer storage, Software packages}},
  publisher    = {{IEEE}},
  title        = {{{Past- and Future-Oriented Time-Bound Temporal Properties with OCL}}},
  doi          = {{10.1109/SEFM.2004.1347516}},
  year         = {{2004}},
}