It is widely accepted that every system should be robust in that "small" violations of environment assumptions should lead to "small" violations of system guarantees, but it is less clear how to make this intuition mathematically precise. While significant efforts have been devoted to providing notions of robustness for Linear Temporal Logic (LTL), branching-time logics, such as Computation Tree Logic (CTL) and CTL*, have received less attention in this regard. To address this shortcoming, we develop "robust" extensions of CTL and CTL*, which we name robust CTL (rCTL) and robust CTL* (rCTL*). Both extensions are syntactically similar to their parent logics but employ multi-valued semantics to distinguish between "large" and "small" violations of the specification. We show that the multi-valued semantics of rCTL make it more expressive than CTL, while rCTL* is as expressive as CTL*. Moreover, we devise efficient model checking algorithms for rCTL and rCTL*, which have the same asymptotic time complexity as the model checking algorithms for CTL and CTL*, respectively.

翻译：人们广泛认为,每个系统都应该保持稳健,因为“小”违反环境假设应导致“小”违反系统保障,但不太清楚如何使这一直觉数学精确。尽管已经做出大量努力,为线性时空逻辑(LTL)提供稳健性概念,但分支-时间逻辑(如计算树逻辑(CTL)和CTL* )在这方面受到的注意较少。为解决这一缺陷,我们开发了CTL和CTL* 的“紫”延伸,我们称之为强力CTL(rCTL)和强力CTL* (rCTL* ) 。虽然这两个扩展都与其母逻辑相近,但采用了多值的语义学来区分“大”和“小”违反规格的行为。我们表明,RCTL的多值语义使得它比CTL更能表达,而rCTL* 和CTL * 一样明确。此外,我们为rCTL和rCTL* 设计了高效的模型核对算法和复杂程度。