Recently, a method for social bot detection was proposed by Pedersen, Slavkovik & Smets (2023). This method involves using a model-based method to detect social bots. The idea of the method is to represent a social network as a logical model M, and to specify the behavior or a social bot as a formula φ. So called model checking algorithms can then be used to find occurrences of bot behavior in the network.
However, previous work only considers the theoretical idea of this approach to detecting social bots. The method itself is discussed in detail, but the implementation and empirical evaluation has not yet been done. This master’s project is about precisely that: to use existing tools or to develop a new one to try to detect bots in practice.
Tasks
The tasks in this project are as follows:
- Get acquainted with basic modal logic to understand the underlying models
- Look into repositories of social network data such as Stanford Large Network Dataset Collection (SNAP)
- Explore how we could translate this data into logical models as described in the paper
- Learn about existing model checkers such as SPIN, NuSMV and MoXI and find out if it is suitable for model checking in this project
- Alternatively, build a model checker from scratch in Python based on the pseudocode in existing work
- Think about other properties we can detect in a network of agents, and if time, try to implement these changes in the model
Prerequisites
Interested students should have taken the course IN3070/IN4070 – Logic.
References
Pedersen, M.Y., Slavkovik, M. & Smets, S. Detecting bots with temporal logic. Synthese 202, 79 (2023). https://doi.org/10.1007/s11229-023-04264-6