Verifying Multi-agent Systems via Unbounded Model Checking - Kacprzak, M; Lomuscio, A; asica, T; Penczek, W; Szreter, M (Springer Berlin Heidelberg, 2004)