Hillston, Jane

Cole, Murray

Piho, Paul

Engineering and Physical Sciences Research Council (EPSRC)

2020-09-30T09:21:08Z

2020-09-30T09:21:08Z

2020-07-25

This thesis explores aspects of model specification and analysis for population dynamics which arise when modelling complex interactions and communication structures in agent or component collectives. The motivating examples come from the design of man-made systems where the optimal parametrisations for the behaviours of agents or components are not known a priori. In particular, we introduce a formal modelling framework to support the specification of control problems for collective dynamics in a high-level process algebraic language. A natural choice for the underlying semantics is to consider continuous time Markov decision processes due to their close relation to continuous time Markov chains that have traditionally been used as the mathematical model in numerous high-level modelling languages for stochastic dynamics. Although the theory of the resulting decision processes has a long history, the practical considerations, like computation time, present challenges due to the problem of state space explosion when considering large systems with complex behaviours. State space explosion problems are especially apparent in formal modelling paradigms where the specification of models usually happens at a component or an agent level in terms of a discrete set of states with defined rules for composing the specified behaviours into the dynamics of a system. Such specifications often give rise to very large models which are costly to analyse in full detail. However, when analysing models of collectives we are usually interested in the resulting macro-scale dynamics in terms of some aggregate measures. With that in mind, the second aspect of analysing collective dynamics that is considered in this thesis relates to fluid, linear noise and moment closure-based approximation methods which aim to give a good representation of the macro-scale dynamics of the models while being computationally less costly to analyse. We address a class of models where the population structure results from the assumption that components or agents can only be distinguished from each other based on the state they are in and focus on the particular cases where the population dynamics can be separated into a discrete set of modes. Our study of these models is motivated by considering information propagation via broadcast communication where the behaviour of components can change drastically when new information is received from the rest of the population. We consider existing approximation methods for resulting stochastic processes and propose a novel approach for applying these methods to models incorporating broadcast communication where each level of information available to the collective corresponds to a discrete dynamic mode. The resulting approximations combine continuous dynamics with discrete stochastic jumps and are not immediately simple to treat numerically. To that end we propose further approximations that allow for a computationally efficient analysis. Finally, we demonstrate how the formal modelling framework in conjunction with the developed approximation methods can be used for an example in policy synthesis.

https://hdl.handle.net/1842/37267

http://dx.doi.org/10.7488/era/554

en

The University of Edinburgh

H. Lv, J. Hillston, P. Piho, and H. Wang. An attribute-based availability model for large scale IaaS clouds with CARMA. IEEE Transactions on Parallel and Distributed Systems, 31(3):733–748, 2020.

P. Piho and J. Hillston. Policy synthesis for collective dynamics. In 15th International Conference on Quantitative Evaluation of SysTems (QEST 2018). Springer, 2018.

constructed models

continuous time Markov decision processes

collective dynamics

approximation

approximation analytical methods

Formal modelling and approximation-based analysis for mode-switching population dynamics

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy