Expressiveness and succinctness of a logic of robustness

摘要

This paper compares the recently proposed Robust Full Computational Tree Logic (RoCTL~*) to model robustness in concurrent systems with other computational tree logic (CTL~*)-based logics. RoCTL~* extends CTL~* with the addition of the operators Obligatory and Robustly, which quantify over failure-free paths and paths with one more failure respectively. This paper focuses on examining the succinctness and expressiveness of RoCTL~* by presenting translations to and from RoCTL~*. The core result of this paper is to show that RoCTL~* is expressively equivalent to CTL~* but is non-elementarily more succinct. That is, RoCTL~* does not add any expressive power over CTL~*, but can represent some properties using vastly reduced formulae. We present a translation from RoCTL~* into CTL~* that preserves truth but may result in non-elementary growth in the length of the translated formula, as each nested Robustly operator may result in an extra exponential blowup. However, we show that this translation is optimal in the sense that any equivalence-preserving translation will require an extra exponential growth per nested Robustly. Note that this result has to do with the length of the translated formula. It has not been proved that there is no elementary decision procedure for RoCTL~*; it is only known that RoCTL~* must be at least as hard as CTL~* (i.e., double exponential). We also compare RoCTL~* to Quantified CTL~* (QCTL~*) and hybrid logics.