On the complexity of path checking in temporal logics

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 word. For LTL, the complexity of this task was recently shown to be in NC hierarchy. In this paper, we establish a connection between LTL path checking and planar circuits. We use the connection to show that the path-checking problem for LTL extended with exclusive or is already P-hard. We then present an NC algorithm for MTL, a quantitative (or metric) extension of LTL and give an AC-1 algorithm for UTL, the unary fragment of LTL.

Authors

• Daniel Bundala
• Joël Ouaknine Max Planck Institute for Software Systems, Saarland Informatics Campus

Keywords

No keywords are indexed for this paper.