On the Complexity of Path Checking in Temporal Logics

Daniel Bundala ( University of Oxford )

Given a formula in a temporal logic such as LTL or MTL, a fundamental problem is the complexity of evaluating the formula on a given trace. For LTL, the complexity of this task was recently shown to be in NC. In this paper, we establish a connection between LTL path checking and planar circuits, which we then exploit to show that any further progress in determining the precise complexity of LTL+Past path checking would immediately entail a more efficient evaluation algorithm for a certain class of planar circuits. Moreover, we show that the path-checking problem for LTL extended with exclusive or is P-hard. We then present an NC algorithm for MTL, a quantitative (or metric) extension of LTL. Finally, we give an AC^1 algorithm for UTL, the unary fragment of LTL. At the time of writing, this appears to be the most expressive fragment of LTL with a more efficient path-checking algorithm than for full LTL (subject to standard complexity-theoretic assumptions).