© Springer International Publishing AG, part of Springer Nature 2018. The behaviour of a reactive, line-following robot is analysed using modal logic. This provides an approach that is complementary to numerical simulation, allowing us to explore the qualitative state-space of the robot coupled with its environment. The envisionment of this state-space can be described as a Kripke model, and model-checking tools enable us to analyse this model to search for stable equilibria that contain goal states.
Battle, S., & Thompson, M. (2018). A modal logic analysis of a line-following robot. Communications in Computer and Information Science, 732, 42-55. https://doi.org/10.1007/978-3-319-90418-4_4