  While most approaches in formal methods address system correctness, ensuring
robustness has remained a challenge. In this paper we introduce 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.
