ABS Fatemeh Ahmadi (Latin)

ABSTRACT:

   Deontic logics have proved to be useful for reasoning about legal and moral systems, where the situation is more or less similar to fault tolerance: there exists a set of rules that states what the normal behaviors or scenarios are. Violations arise when these rules are not followed and, as a consequence, some actions must be performed to a normal or desirable state. The standard logical operators allow us to describe the basic behavior of the system, while we use deontic predicates on action to express prescriptions about the systems behavior.

   In this master of science thesis, a systems for deontic logic is express and reason about propertie   of fault tolerance computing systems. We study the properties of this logic, commenting on those that are relevant to the use of the logic in practice. Here a deontic action logic and its axiomatization is introduced. The logic has some innovative features, as compared to extant versions of deontic logic. For example, because we want to do various forms of automated analysis of specification, such as model checking, we want this logic to have appropriate meta properties. So, the logic is not just sound and complete, but also decidable and compact (strongly complete). For expressing properties inherent to fault tolerance, we need to be able to express temporal assertation, recovery actions, permission and obligation predicates on actions. Though the propositional version of the logic is quite expressive, it is augmented with temporal operators, and an axiomatic system for this more expressive framework is outlined. An important characteristic of this deontic action logic is that Boolean combinators is used on actions, and, because of finiteness restrictions, the generated Boolean algebra is atomic, which is a crucial point in proving the completeness of the axiomatic system.

   In fault tolerant systems, it is usual to have situations where, after a violation, we must perform some actions to recover from this violation. This is an instance of what is called by deontic logicians contrary to duty (or CTD for short) reasoning. CTD reasoning is an important object of study in deontic logic; this kind of reasoning arises naturally in legal scenarios. In the last Chapter a new version of this kind of this kind of deontic logic is proposed 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. We study how to apply this formalism to characterize fault tolerance mechanisms and to then reason about the properties of the mechanisms.

Some example are provided throughout this thesis to illustrate how the ideas described can be applied in practice. The first example is the ltr">