Robust, expressive, and quantitative linear temporal logics: Pick any two for free

Neider, Daniel, Weinert, Alexander and Zimmermann, Martin ORCID: 0000-0002-8038-2453 (2022) Robust, expressive, and quantitative linear temporal logics: Pick any two for free. INFORMATION AND COMPUTATION, 285. p. 104810.

Text
1808.09028.pdf - Submitted version
Download (439kB) | Preview

Official URL: http://dx.doi.org/10.1016/j.ic.2021.104810

Abstract

Linear Temporal Logic (LTL) is the standard specification language for reactive systems and is successfully applied in industrial settings. However, many shortcomings of LTL have been identified, including limited expressiveness, the lack of quantitative features, and the inability to express robustness. While there is work on overcoming these shortcomings, each of these is typically addressed in isolation, which is insufficient for any application in which all shortcomings manifest themselves simultaneously. Here, we tackle this issue by introducing logics that address more than one shortcoming. To this end, we combine Linear Dynamic Logic, Prompt-LTL, and robust LTL, each addressing one aspect, to new logics. The resulting logics have the same desirable algorithmic properties as plain LTL for all combinations of two aspects. In particular, the highly efficient algorithmic backends developed for LTL are also applicable to these new logics. Finally, we discuss how to address all three aspects simultaneously.

Item Type:	Article
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	16 Nov 2021 08:43
Last Modified:	18 Jan 2023 21:24
DOI:	10.1016/j.ic.2021.104810
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3143206