Flocks of birds: a quantitative evaluation

This paper elaborates on the concept that utilizing compositional specifications grounded in formal languages enables the modeling and analysis of intricate collective behaviors within natural systems, such as flocks of birds. Current state-of-the-art approaches primarily focus on formalisms that model system behavior for verification purposes, with less emphasis on quantitative aspects. The objective of this paper is to complement formal specifications with a quantitative abstraction, specifically Markov Population Processes (MPP), thus enabling the measurements of key properties, such as the probability of cohesion among birds, for scenarios under evaluation. Starting with a formal specification inherited from the literature, we develop an MPP model that enhances the types of analysis applicable to collective adaptive systems. Our results confirm that MPP models are suitable for replicating the behavior of flocks and pave the way for quantitative assessments, such as the timeliness of interactions between a prey and flocks.