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 (2019) Robust, expressive, and quantitative linear temporal logics: Pick any two for free. In: Electronic Proceedings in Theoretical Computer Science, EPTCS, 305, pp. 1-16. Tenth International Symposium on Games, Automata, and Formal Verification, 2. - 3. September 2019, Bordeaux, Frankreich. DOI: 10.4204/EPTCS.305.1

[img] PDF
275kB

Official URL: https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?GandALF2019.1

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 in the literature, among them the limited expressiveness, the lack of quantitative features, and the inability to express robustness. There is work on overcoming these shortcomings, but each of these is typically addressed in isolation. This is insufficient for applications where all shortcomings manifest themselves simultaneously. Here, we tackle this issue by introducing logics that address more than one shortcoming. To this end, we combine the logics Linear Dynamic Logic, Prompt-LTL, and robust LTL, each addressing one aspect, to new logics. For all combinations of two aspects, the resulting logic has the same desirable algorithmic properties as plain LTL. In particular, the highly efficient algorithmic backends that have been 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/131253/
Document Type:Conference or Workshop Item (Speech)
Title:Robust, expressive, and quantitative linear temporal logics: Pick any two for free
Authors:
AuthorsInstitution or Email of AuthorsAuthors 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:2019
Journal or Publication Title:Electronic Proceedings in Theoretical Computer Science, EPTCS
Refereed publication:Yes
Open Access:Yes
Gold Open Access:No
In SCOPUS:Yes
In ISI Web of Science:No
Volume:305
DOI :10.4204/EPTCS.305.1
Page Range:pp. 1-16
Series Name:Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification
Status:Published
Keywords:Mathematische Logik, Verifikation
Event Title:Tenth International Symposium on Games, Automata, and Formal Verification
Event Location:Bordeaux, Frankreich
Event Type:international Conference
Event Dates:2. - 3. September 2019
HGF - Research field:Aeronautics, Space and Transport
HGF - Program:Space
HGF - Program Themes:Space Technology
DLR - Research area:Raumfahrt
DLR - Program:R SY - Technik für Raumfahrtsysteme
DLR - Research theme (Project):R - Vorhaben SISTEC
Location: Köln-Porz
Institutes and Institutions:Institut of Simulation and Software Technology
Institut of Simulation and Software Technology > Distributed Systems and Component Software
Deposited By: Weinert, Alexander
Deposited On:28 Nov 2019 12:08
Last Modified:28 Nov 2019 12:08

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.