The complexity of LTrL, a global linear time temporal logic over traces is investigated. The logic is global because the truth of a formula is evaluated in a global state, also called configuration. The logic is shown to be non-elementary with the main reason for this complexity being the nesting of until operators in formulas. The fragment of the logic without the until operator is shown to be EXPSPACE-eomplote.
CITATION STYLE
Walukiewiez, I. (1998). Difficult configurations - On the complexity of LTrL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1443 LNCS, pp. 140–151). https://doi.org/10.1007/bfb0055048
Mendeley helps you to discover research relevant for your work.