Being Correct Is Not Enough: Efficient Verification Using Robust Linear Temporal Logic

While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. In this article, we present and study the logic rLTL, which provides a means to formally reason about both correctness and robustness in system design. Furthermore, we identify a large fragment of rLTL for which the verification problem can be efficiently solved, i.e., verification can be done by using an automaton, recognizing the behaviors described by the rLTL formula phi, of size at most O(3(vertical bar phi vertical bar)), where vertical bar phi vertical bar is the length of phi. This result improves upon the previously known bound of O(5(vertical bar phi vertical bar)) for rLTL verification and is closer to the LTL bound of O(2(vertical bar phi vertical bar)). The usefulness of this fragment is demonstrated by a number of case studies showing its practical significance in terms of expressiveness, the ability to describe robustness, and the fine-grained information that rLTL brings to the process of system verification. Moreover, these advantages come at a low computational overhead with respect to LTL verification.