Deontic Logic, Contrary to Duty Reasoning and Fault Tolerance

Deontic Logic was introduced in the first half of the last century to formalize aspects of legal reasoning. Since then a lot of effort has gone into improving the formalism(s) and widening their applicability, including in Computer Science and Software Engineering. One strand of work has focused on the use of an action based approach to deontic operators, rather than the traditional property focused operators. We propose a new version of this kind of deontic logic that has very nice meta-logical properties, avoids many of the traditional problems of deontic logics and has an appealing treatment of contrary to duty reasoning. This kind of reasoning provides a kind of conditional reasoning about having violated normative constraints and describing the resulting consequences. We show how to apply this formalism to characterize fault tolerance mechanisms and to then reason about the properties of the mechanisms.