University of Twente Student Theses
As of Friday, 8 August 2025, the current Student Theses repository is no longer available for thesis uploads. A new Student Theses repository will be available starting Friday, 15 August 2025.
Validating Agent-Based Models with Probabilistic Model Checkers
Balotescu, Alexia (2025) Validating Agent-Based Models with Probabilistic Model Checkers.
PDF
3MB |
Abstract: | This study explores the use of probabilistic model checking (PMC) to verify agent-based models (ABMs) from the social sciences. It focuses on a rumour-spreading model proposed by Mazzoli et al. (2018). The ABM has been encoded as a discrete-time Markov chain in the PRISM model checker. A set of 14 properties has been defined in order to formally verify the model. The results show consistency with the original paper’s simulation results, confirming that formal verification can capture core dynamics, such as spontaneous activation of spreaders or debunking effects. However, challenges like state-space explosion or limited scalability demonstrate the trade-offs of this approach. This study shows that formal tools like PRISM are able to reproduce and even deepen the analysis of ABMs, offering formal guarantees and better insights into system behaviour. However, limitations were also observed, such as large memory usage and scalability issues. This positions PMC as a complementary method to simulation, valuable for medium-scale social networks with rule-driven or well-defined agent behaviours. |
Item Type: | Essay (Bachelor) |
Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
Subject: | 54 computer science |
Programme: | Computer Science BSc (56964) |
Link to this item: | https://purl.utwente.nl/essays/107301 |
Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Repository Staff Only: item control page