Formal modelling

Designing complex search methods calls not only for employing sufficient methods for validation of their outcomes, but also verification of their design and analytical features becomes necessary.

There were constructed several formal models aimed at proving different features of evolutionary meta-heuristics. One of the first and important models of meta-heuristic methods was Michael Vose’s SGA model, proving that for the population of a fixed size, Simple Genetic Algorithm can be modelled by a Markov chain, and after further assumption, that the mutation rate is positive, this chain is ergodic. This result formally justifies SGA as a well-defined global optimization algorithm and become an inspiration for preparing a Markov-chain based models for agent-based meta-heuristics and proving their ergodicity feature.

Other approaches to model evolutionary algorithms to be mentioned are different models for single-population and parallel evolutionary algorithms. Using some of such models, the researchers have proven selected practical features, such as e.g., first hitting time for simple settings (e.g., evolution strategy 1 + 1 solving the problem of optimisation of a convex function). Besides such systems, more advanced search and optimisation techniques like memetic or agent-based computational systems lack such models, with some notable exceptions. In general, there is still a lack of a comprehensive stochastic model of the wide class of population-based, agent-based, cultural or memetic computing systems. One of the reason is perhaps that such systems are still weakly defined and formalised which of course have to be done before any attempt to analyse their features analytically. Other reason is for sure that these systems are complex, so proper preparation of detailed formal model leading to significant theoretical results is complicated.

It is easy to see that detailed modelling of such systems will surely lead to better understanding them and is necessary to make sure, that one does not only prepare a complex meta-heuristic, but provides a potential user with a firm background, proofing, that using of such complex computing method makes sense.

Therefore we have proposed a formal model for EMAS dynamics, utilising Markov chains, inspired by the works of Vose. The constructed model allows an exhaustive asymptotic analysis of all memetic search methods fitting the proposed framework. Various types of convergence to the solution of the global optimisation problem can be verified. In particular, the probabilistic guarantee of success results from the ergodicity of the model. A detailed concurrency analysis of the agents’ actions allows to define Markov transition probability function as the commutable composition of stochastic kernels imposed by independent actions.

Ergodicity theorems have also been formulated for EMAS and its immunological variant (iEMAS) and full formal proof (an outline for iEMAS) was constructed.

The obtained theoretical results, in particular the most important feature of ergodicity, proven for EMAS (including its memetic versions) and iEMAS, are helpful for studying important features of stochastic global optimization meta-heuristics conforming EMAS architecture and implemented as a concurrent system in a distributed computing environment.

The proven strong ergodicity of the finite state Markov chain modelling the meta-heuristics causes that it can reach an arbitrary state (arbitrary population) in the finite number of iteration with the probability one which implies the asymptotic stochastic guarantee of success

It is to note, that besides formal models focused on particular aspects of population-based meta-heuristics, in fact genetic algorithm only), there are no similar approaches to model such complex computing system, as agent-based ones. It seems to be one of the biggest advantages of the completed research.