Current browse context:
cs.LO
Change to browse by:
References & Citations
Computer Science > Logic in Computer Science
Title: Being correct is not enough: efficient verification using robust linear temporal logic
(Submitted on 24 Feb 2021 (v1), last revised 19 Oct 2021 (this version, v2))
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.
Submission history
From: Tzanis Anevlavis [view email][v1] Wed, 24 Feb 2021 00:14:00 GMT (69kb)
[v2] Tue, 19 Oct 2021 08:03:45 GMT (909kb,D)
Link back to: arXiv, form interface, contact.