Being correct is not enough: efficient verification using robust linear temporal logic

TL;DR

This paper introduces rLTL, a logic for reasoning about correctness and robustness in system design, and presents an efficient verification method for a large fragment of rLTL with improved automaton size bounds.

Contribution

The paper defines rLTL for robustness verification and identifies a large fragment allowing automaton-based verification with improved size bounds, closer to LTL efficiency.

Findings

Verification automaton size bound improved to O(3^{|φ|})

Demonstrated practical case studies of rLTL's expressiveness

Verification overhead remains low compared to LTL

Abstract

While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. In this paper 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 $\varphi$, of size at most $\mathcal{O} \left( 3^{ |\varphi|} \right)$, where $|\varphi|$ is the length of $\varphi$. This result improves upon the previously known bound of $\mathcal{O}\left(5^{|\varphi|} \right)$ for rLTL verification and is closer to the LTL bound of $\mathcal{O}\left( 2^{|\varphi|} \right)$. 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.