Bounded model checking for knowledge and real time - Wona, B; Lomuscio, A; Penczek, W (ACM, 2005)