LTL Path Checking is Efficiently Parallelizable

Lars Kuhtz and Bernd Finkbeiner

We present an AC¹ (logDCFL) algorithm for checking LTL formulas over finite paths, thus establishing that the problem can be efficiently parallelized. Our construction provides a foundation for the parallelization of various applications in monitoring, testing, and verification.

36th International Colloquium on Automata, Languages and Programming (ICALP 2009).

Best paper award.

(pdf) (bib)