Title
Robust, Expressive, and Quantitative Linear Temporal Logics.
Abstract
Linear Temporal Logic (LTL) is the standard specification language for reactive systems and 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. Typically, each one of these deficiencies is 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 at a time. To this end, we combine the logics robust LTL, Prompt-LTL, and Linear Dynamic Logic, each addressesing 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 introduce a logic addressing all three aspects.
Year
Venue
Field
2018
arXiv: Logic in Computer Science
Specification language,Algorithm,Robustness (computer science),Linear temporal logic,Theoretical computer science,Dynamic logic (digital electronics),Reactive system,Mathematics,Expressivity
DocType
Volume
Citations 
Journal
abs/1808.09028
0
PageRank 
References 
Authors
0.34
0
3
Name
Order
Citations
PageRank
Daniel Neider115321.97
Alexander Weinert200.68
Martin Zimmermann 000233510.88