A Complete and Compact Propositional Deontic Logic

In this paper we present a propositional deontic logic, with the goal of using it to specify fault-tolerant systems, and an axiomatization of it. We prove several results about this logic: completeness, soundness, compactness and decidability. The main technique used during the completeness proof is based on standard techniques for modal logics, but it has some new characteristics introduced for dealing with this logic. In addition, the logic provides several operators which appear useful for use in practice, in particular to model fault-tolerant systems and to reason about their fault tolerance properties.