Tech Reports


Resolution for a Temporal Logic of Robustness (Extended Version)

Clare Dixon and John C. McCabe-Dansted


The logic RoCTL* is an extension of the branching time temporal logic CTL* to represent robustness and reliability in systems. New operators are introduced dealing with obligation (where no failures occur) and robustness (where at most one additional failure occurs). The only known decision procedure for the temporal logic of robustness RoCTL* involves a reduction to the non-elementary QCTL* logic. Here we propose a CTL like restriction of RoCTL*, termed RoCTL, and investigate its application and complexity. We show that the fragment of RoCTL without the robust and prone operators, RoCTL-, can be translated into CTL. We provide a satisfiability preserving translation for RoCTL$- into CTL. By applying a known resolution calculus to the resulting formulae we obtain a resolution calculus for RoCTL- and show that the complexity of satisfiability of RoCTL- is EXPTIME.

[Full Paper]