Difficult Configurations - On the Complexity of LTrL

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

• Type: Conference
• Year: 1998
• Where: ICALP
• Authors: Igor Walukiewicz
• Keywords: Global, Global State, ICALP 1998, Programming Languages, Time Temporal Logic