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