منطق عملي بولي، جبرهاي بول اتميك و تحمل پذيري خطا، يا، منطق عملي تكليف، جبرهاي بول اتميك و تحمل پذيري خطا

چكيده انگليسي :

Deontic Action Logic Atomic Boolean Algebras and Fault Tolerance Fatemeh Ahmadi f ahmadi79 @yahoo com January 10 2012 Master of Science Thesis Department of Mathematical Scienoes Isfahan University of Technology Isfahan 84156 83111 IranSupervisors Dr Mojtaba Aghaei aghaei@cc iut ac ir 2000 MSC 03B45 Key word Deontic logic Fault tolerance Temporal logic Contrary to duty reasoning Abstract Deontic logics have proved to be useful for reasoning about legal and moral systems where thesituation is more or less similar to fault tolerance there exists a set of rules that states what the normalbehaviors 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 allowus to describe the basic behavior of the system while we use deontic predicates on action to expressprescriptions about the systems behavior In this master of science thesis a systems for deontic logic is express and reason about properties offault tolerance computing systems We study the properties of this logic commenting on those thatare relevant to the use of the logic in practice Here a deontic action logic and its axiomatization isintroduced 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 asmodel checking we want this logic to have appropriate meta properties So the logic is not just soundand complete but also decidable and compact strongly complete For expressing properties inherentto fault tolerance we need to be able to express temporal assertation recovery actions permission andobligation predicates on actions Though the propositional version of the logic is quite expressive it isaugmented with temporal operators and an axiomatic system for this more expressive framework isoutlined An important characteristic of this deontic action logic is that Boolean combinators is usedon actions and because of finiteness restrictions the generated Boolean algebra is atomic which is acrucial 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 performsome actions to recover from this violation This is an instance of what is called by deontic logicianscontrary to duty or CTD for short reasoning CTD reasoning is an important object of study indeontic logic this kind of reasoning arises naturally in legal scenarios In the last Chapter a newversion 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 contraryto duty reasoning We study how to apply this formalism to characterize fault tolerance mechanismsand to then reason about the properties of the mechanisms Some example are provided throughout this thesis to illustrate how the ideas described can be appliedin practice The first example is the classical example of dinning philosophers of Dijkstra but somefeatures is added to it so that every process has the possibility of crashing for an indefinite amount oftime This modification allows us to show how the constructs presented in Chapter 4 can be used inpractice to reason about fault tolerance The second example it is a simple train system fault toleranceis important in these kinds of systems since failures may cause tragic accidents In this example isshowed how contrary to duty statements might arise in practice

احمدي، فاطمه

منطق عملي بولي، جبرهاي بول اتميك و تحمل پذيري خطا، يا، منطق عملي تكليف، جبرهاي بول اتميك و تحمل پذيري خطا

منطق تكليف , منطق زماني , استدلال تناقص در ماموريت