Expressiveness and succinctness of a logic of robustness.
Journal of Applied Non-Classical Logics(2015)
摘要
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 th...
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络