Formal modelling of collective systems

1 Ph.D/Postdoctoral Position

Research objectives: Organisms are not self-propelled particles interacting with social forces, as has been traditionally assumed in the study of collective behaviour. Instead, collectives are composed of heterogeneous, and cognitive, agents with different, possibly conflicting preferences, each mapping a high-dimensional sensory input to a relatively low-dimensional behavioural output. At the same time, collectives show remarkable robustness in behaviour with respect to some perturbations (such as environmental noise) and yet high specificity to others (such as cryptic predators). Current approaches to modelling collectives employ simplistic agent descriptions, in part due to limited quantitative measurements, especially in natural habitats and over the time-scales needed to capture lifetime behaviours exhibited by animals, and also because simpler models allow for tractable analysis of collective dynamics. In the context of visual tracking, our models will provide guidance towards replacing the omniscient prediction models in the trackers. In addition, they might give important guidance for the experiments being conducted in the Centre, and will consequently contribute to all other projects.

The Department of Computer and Information Science has an opening for one Ph.D. or Postdoctoral position to study formal computational modelling of collective behaviour. We aim at building explanatory models, models where the states and parameters of the model reflect our understanding of the underlying mechanisms. The algorithmic challenges include the formal representation of cognitive individuals and reducing the computationally expensive simulation of many mutually dependent individuals. The measured data should be maximally utilised to create and validate models, but data incorporation includes challenges such as the quantitative uncertainties, missing or unavailable measurements. To tackle these challenges, we draw a parallel between our desired explanatory model and a computer program, and we employ methods of formal verification: data will be treated as model specification, and expert knowledge will be used to build initial models and questions of interest. We use methods such as temporal logics, interval metrics, model checking, constraint solvers, model reduction. The PhD/postdoc will explore the parameter synthesis for stochastic population models, where interval-valued properties are automatically inferred from available data. (Advisor: Tatjana Petrov)