LTL Path Checking is Efficiently Parallelizable

Lars Kuhtz and Bernd Finkbeiner

We present an AC1 (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)