هدف از اين پاياننامه، معرفي يك چهارچوب رياضي جهت استدلال در مورد خواص سيستمهاي تحملپذير خطا ميباشد. در همين راستا يك منطق عملي تكليف (DPL ) و يك اصلگذاري براي آن معرفي ميگردد. اين منطق خواص مفيدي مثل سلامت، تماميت، فشردگي و تصميمپذيري دارد. اگر چه منطق معرفي شده، ارزشمند و مهم است ولي از آنجا كه منطقهاي زماني در مشخص كردن سيستمهاي محاسبه نقش مهمي دارند، اين منطق توسط عملگرهاي زماني (CTL) توسيع داده ميشود. در سيستمهاي تحملپذير خطا، بعد از يك نقض بايد اعمالي اجرا شود تا آن نقض را جبران كند كه در منطق تكليف استدلال CTD ناميده ميشود. رويكرد ما در اين پاياننامه براي مواجهه با چنين جملاتي، استفاده از چندين نسخهي مجوز ميباشد كه به اين ترتيب توسيع سودمند ديگري از DPL حاصل ميشود. در اين پاياننامه همچنين با طرح سناريوهايي از ساختارهاي ارائه شده مانند شام فيلسوفان و سيستم قطار، چگونگي كاربرد آنها را براي مشخص كردن سيستمهاي محاسبه در عمل نيز نشان ميدهيم.
-