Supervisors

Suitable for

Abstract

Agent-based Modelling (ABM) is a unique paradigm for studying complex systems wherein individual agents are explicitly modelled and interact with each other as part of a synthetic population. Within an agent-based model, each agent individually assesses its situation and makes potentially randomised decisions according to a set of internal rules. Note that agents may be heterogeneous, possessing different properties which may cause them to behave differently. By employing an agent-based model, one may hope to understand how global, or macroscopic, properties of a complex system may emerge from the collective behaviour of individuals. In particular, agent-based models allow practitioners to model real-world systems at extremely high fidelity, by taking into account many small details. However, this individual-based view on a global system naturally leads to a great computational overhead. As a result, it becomes challenging to carry out verification, validation, and analysis of agent-based models, and therefore reason about their correctness.

In this project, we will focus on addressing this shortcoming. More specifically, this project will focus on finding computationally succinct representations of agent-based models which can be combined with techniques from formal verification and probabilistic model checking in order verify and reason about the properties of agent-based models.

In short, the main goals of this project include:

A.     To formally describe agent-based models using a mathematical framework (e.g., finite dynamical systems, graph theory and Markov chains). B.      Develop techniques to transform a formal ABM into probabilistic timed automata (PTAs) or discrete-time Markov chains (DTMCs) for formal verification using the PRISM model checker. C.      Explore and implement state-space reduction techniques and demonstrate applications for industrial scale agent-based models.

Familiarity with PRISM, Computer-Aided Formal Verification, Probabilistic Model Checking. Desirable Prerequisites: Machine Learning.

[1] Laubenbacher, R., Jarrah, A.S., Mortveit, H.S., Ravi, S. (2012). Agent Based Modeling, Mathematical Formalism for. In: Meyers, R. (eds) Computational Complexity. Springer, New York, NY. https://doi.org/10.1007/978-1-4614-1800-9_6

[2] Banisch, Sven. "The probabilistic structure of discrete agent-based models." Discontinuity, Nonlinearity, and Complexity 3(3) (2014) 281--292 | DOI:10.5890/DNC.2014.09.005

[3] Banisch, Sven. Markov chain aggregation for agent-based models. Springer, 2015 https://link.springer.com/content/pdf/10.1007/978-3-319-24877-6.pdf

[4] Clarke, Edmund M., et al., eds. Handbook of model checking. Vol. 10. Cham: Springer, 2018.

[5] Computer-Aided Formal Verification: 2022-2023, Department of Computer Science Lecturer David Parker https://www.cs.ox.ac.uk/teaching/courses/2022-2023/computeraidedverification/

[6] Macal, Charles M. "Everything you need to know about agent-based modelling and simulation." Journal of Simulation 10, no. 2 (2016): 144-156

[7] Abar, Sameera, Georgios K. Theodoropoulos, Pierre Lemarinier, and Gregory MP O’Hare. "Agent Based Modelling and Simulation tools: A review of the state-of-art software." Computer Science Review 24 (2017): 13-33.