Robust, Expressive, and Quantitative Linear Temporal Logics
share
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.
READ FULL TEXT