title: Formal Analysis of Artificial Collectives using Parametric Markov Models
Creators: name: Gainer, Paul
Publisher: name: University of Liverpool Repository
Year: 2020

description: There are many potential applications for the deployment of distributed systems composed of identical autonomous agents such as swarm robotic systems or wireless sensor networks, including remote monitoring, space exploration, or environmental clean up. Such systems need to be robust, and the loss of a small number of agents should not compromise the effectiveness of the system as they will often operate in hostile environments where individual members of that system may suffer failures, or communication may be hindered. To address this, these artificial systems are often designed to imitate the behaviour of self-organising systems found in nature, where simple reactive behaviours for individual members of a system can lead to complex global behaviours, and the collective remains robust to the loss of individuals. Despite much research being conducted into the development and evaluation of these systems, the industrial application of these technologies is still low. This issue could be addressed by further demonstrating that they can reliably, and predictably, achieve given objectives. Designing such systems is challenging, and often detailed simulations are developed for their analysis. Simulations give invaluable insight into the behaviour of such a system, however, there are often corner cases that might be overlooked. By developing a formal model of the system using some appropriate formalism, mathematical techniques can be applied during development to ensure that the system behaves correctly with respect to some given specification. These dynamic and inherently stochastic systems can be modelled as Markov processes; memoryless stochastic processes whose behaviour at any moment in time is determined solely by their current state. Model checking is an algorithmic technique to exhaustively check that a representation of a system as a Markov process exhibits some desirable property; furthermore, such an analysis can be extended to analyse systems whose parameters may not be known in an advance. However, the analysis of formal models of large systems is limited due to the resources that are required for their analysis: the size of the model may grow exponentially with the size of the system, and the subsequent analysis may prove to be impossible due to hardware or time constraints. This thesis investigates the suitability of parametric Markov models for the analysis of swarm robotic systems and wireless sensor networks. The analysis of such models is costly in terms of the size of the formal model representing a system, and the computation time required for its subsequent analysis. Modelling techniques and abstractions are developed for the construction of macroscopic models that abstract away from the identities of individual swarm robots or sensor nodes, and instead focus on the desirable global behaviours of such a system, resulting in smaller formal models. New techniques are then introduced to facilitate the analysis of large families of such models, where similarities between models who share some parameter values are exploited to speed up their analysis. In addition, new representations for such models are developed that allow for larger models to be analysed, and also significantly reduce the time required for that analysis.