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 Neider | 1 | 153 | 21.97 |
Alexander Weinert | 2 | 0 | 0.68 |
Martin Zimmermann 0002 | 3 | 35 | 10.88 |