Bounded model checking for deontic interpreted systems - Wozna, B; Lomuscio, A; Penczek, W (Electronic Notes of Theoretical Computer Science, 2004)