Di cult configurations-on the complexity of LTrL

Abstract 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 conguration. 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-hard.