elib
DLR-Header
DLR-Logo -> http://www.dlr.de
DLR Portal Home | Imprint | Privacy Policy | Contact | Deutsch
Fontsize: [-] Text [+]

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

Neider, Daniel and Weinert, Alexander and Zimmermann, Martin (2021) Robust, expressive, and quantitative linear temporal logics: Pick any two for free. Information and Computation. Elsevier. doi: 10.1016/j.ic.2021.104810. ISSN 0890-5401. (In Press)

[img] PDF - Preprint version (submitted draft)
576kB

Official URL: https://www.sciencedirect.com/science/article/abs/pii/S0890540121001267

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 URL in elib:https://elib.dlr.de/144975/
Document Type:Article
Title:Robust, expressive, and quantitative linear temporal logics: Pick any two for free
Authors:
AuthorsInstitution or Email of AuthorsAuthor's ORCID iD
Neider, Danielneider (at) mpi-sws.orgUNSPECIFIED
Weinert, Alexanderalexander.weinert (at) dlr.dehttps://orcid.org/0000-0001-8143-246X
Zimmermann, Martinmartin.zimmermann (at) liverpool.ac.ukhttps://orcid.org/0000-0002-8038-2453
Date:20 October 2021
Journal or Publication Title:Information and Computation
Refereed publication:Yes
Open Access:Yes
Gold Open Access:No
In SCOPUS:Yes
In ISI Web of Science:Yes
DOI :10.1016/j.ic.2021.104810
Publisher:Elsevier
ISSN:0890-5401
Status:In Press
Keywords:Temporal Logics, Robustness, Expressiveness, Quantitative Logics
HGF - Research field:Aeronautics, Space and Transport
HGF - Program:Space
HGF - Program Themes:Space System Technology
DLR - Research area:Raumfahrt
DLR - Program:R SY - Space System Technology
DLR - Research theme (Project):R - Tasks SISTEC
Location: Köln-Porz
Institutes and Institutions:Institute for Software Technology > Intelligent and Distributed Systems
Institute for Software Technology
Deposited By: Weinert, Alexander
Deposited On:30 Nov 2021 08:42
Last Modified:30 Nov 2021 08:42

Repository Staff Only: item control page

Browse
Search
Help & Contact
Information
electronic library is running on EPrints 3.3.12
Copyright © 2008-2017 German Aerospace Center (DLR). All rights reserved.