## On the complexity of temporal-logic path checking

*Daniel Bundala* and
*Joël
Ouaknine*
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 finite
word. For LTL, the complexity of this task was recently shown to be in
NC [9]. In this paper, we 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. At the time of writing,
MTL is the most expressive logic with an NC path-checking algorithm,
and UTL is the most expressive fragment of LTL with a more efficient
path-checking algorithm than for full LTL (subject to standard
complexity-theoretic assumptions). We then establish a connection
between LTL path checking and planar circuits, which we exploit to
show that any further progress in determining the precise complexity
of LTL path checking would immediately entail more efficient
evaluation algorithms than are known for a certain class of planar
circuits. The connection further implies that the complexity of LTL
path checking depends on the Boolean connectives allowed: adding
Boolean exclusive or yields a temporal logic with P-complete
path-checking problem.

*Proceedings of ICALP 14*, LNCS 8573, 2014. 16 pages.

PDF
© 2014
Springer-Verlag.

Imprint / Data Protection