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