TY - JOUR
T1 - Robust computation tree logic
AU - Nayak, Satya Prakash
AU - Neider, Daniel
AU - Roy, Rajarshi
AU - Zimmermann, Martin
N1 - Publisher Copyright:
© The Author(s) 2024.
PY - 2024/3
Y1 - 2024/3
N2 - 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, 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 show that the model checking problem, the satisfiability problem, and the synthesis problem for rCTL and rCTL* have the same asymptotic complexity as their non-robust counterparts, implying that robustness can be added to branching-time logics for free.
AB - 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, 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 show that the model checking problem, the satisfiability problem, and the synthesis problem for rCTL and rCTL* have the same asymptotic complexity as their non-robust counterparts, implying that robustness can be added to branching-time logics for free.
KW - Computation tree logic
KW - Model checking
KW - Robustness
KW - Synthesis
UR - http://www.scopus.com/inward/record.url?scp=85188178714&partnerID=8YFLogxK
U2 - 10.1007/s11334-024-00552-7
DO - 10.1007/s11334-024-00552-7
M3 - Journal article
AN - SCOPUS:85188178714
SN - 1614-5046
JO - Innovations in Systems and Software Engineering
JF - Innovations in Systems and Software Engineering
ER -