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

Download:

Current browse context:

eess.SY

Change to browse by:

References & Citations

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 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.
Comments: arXiv admin note: text overlap with arXiv:1510.08970. v2 notes: Proof on the complexity of translating rLTL formulae to LTL formulae via the rewriting approach. New case study on the scalability of rLTL formulae in the proposed fragment. Accepted to appear in ACM Transactions on Computational Logic
Subjects: Logic in Computer Science (cs.LO); Computational Complexity (cs.CC); Systems and Control (eess.SY)
ACM classes: F.0; F.4.1
Journal reference: ACM Transactions on Computational Logic, Volume 23, Issue 2, April 2022, Article No.: 8, pp 1-39
DOI: 10.1145/3491216
Cite as: arXiv:2102.11991 [cs.LO]
  (or arXiv:2102.11991v2 [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.