English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Journal Article

Robust, Expressive, and Quantitative Linear Temporal Logics

MPS-Authors
/persons/resource/persons215577

Neider,  Daniel
Group R. Majumdar, Max Planck Institute for Software Systems, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

arXiv:1909.08538.pdf
(Preprint), 269KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Neider, D., Weinert, A., & Zimmermann, M. (2019). Robust, Expressive, and Quantitative Linear Temporal Logics. EPTCS 305, 1-16. doi:10.4204/EPTCS.305.1.


Cite as: https://hdl.handle.net/21.11116/0000-0005-DB81-2
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.