Tech Reports

ULCS-08-002

Resolution for a Temporal Logic of Robustness (Extended Version)

Clare Dixon and John C. McCabe-Dansted

Abstract

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.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.