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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Flocks of Birds: A Quantitative Evaluation

  • Emilio Incerto,
  • Catia Trubiani

摘要

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.