Deontic STIT logic, from logical paradox to security policy

Abstract

A deontic STIT logic is studied in this paper with the possible application of specifying security policies for intrude detection in the pervasive computing environment. Compared to the existing deontic STIT logics, an advantage of our logic is that it is capable of solving the miners paradox, a logical paradox which recently grabs attentions of logicians, philosophers, linguistists and computer scientists. A complete and sound axiomatization of our logic is developed.