dCTL: A Deontic Logic for Fault-Tolerance Reasoning

Nicolas Ricci

24th April 2015 (Friday), 14:00 in ATT 210


With the increasing demand for highly dependable and constantly available systems, being able to reason about faults and their impact on systems is gaining considerable attention. In this talk I will cover a novel logic that we proposed for dealing with reasoning about fault-tolerant systems. This logic, which we refer to as dCTL, employs temporal deontic operators in order to distinguish “good” (normal) from “bad” (faulty) behaviors, using deontic permission and obligation combined in a novel way with temporal operators. These formulas are interpreted over transition systems, in which normal executions are distinguished from faulty ones. Furthermore, we show that this logic is sufficiently expressive to describe various common properties of interest in fault-tolerant systems, and show that it features some desirable characteristics that make it suitable for analysis. I'll also cover results regarding the satisfiability problem for this logic in the aim of its usage in fault-tolerant system synthesis.

Share this page:

Contact Us

Admissions Enquiries:
BSc: +44 (0) 116 252 5280
MSc: +44 (0) 116 252 2265
E: BSc  seadmissions@le.ac.uk
E: MSc  pgadmissions@le.ac.uk

Departmental Enquiries:
T: +44 (0) 116 252 2129/3887
F: +44 (0) 116 252 3604
E: csadmin@mcs.le.ac.uk

Dept of Informatics
University of Leicester
Leicester, LE1 7RH
United Kingdom


AccessAble logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has a detailed accessibility guide for the Informatics Building.