We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

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

Abstract: 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.
Comments: arXiv admin note: text overlap with arXiv:1510.08970
Subjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC); Systems and Control (eess.SY)
ACM classes: F.0; F.4.1
Cite as: arXiv:2102.11991 [cs.LO]
  (or arXiv:2102.11991v1 [cs.LO] for this version)

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.