LTL Path Checking Is Efficiently Parallelizable

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. Linear-time temporal logic (LTL) is the standard specification language to describe properties of reactive computation paths. The problem of checking whether a given finite path satisfies an LTL formula plays a key role in monitoring and runtime verification [12,10,6,1,4], where individual paths are checked either online, during the execution of the system, or offline, for example based on an error report. Similarly, path checking occurs in testing [2] and in several static verification techniques, notably in Monte-Carlo-based probabilistic verification, where large numbers of randomly generated sample paths are analyzed [22]. Somewhat surprisingly, given the widespread use of LTL, the complexity of the path ch...

• Type: Conference
• Year: 2009
• Where: ICALP
• Authors: Lars Kuhtz, Bernd Finkbeiner
• Keywords: ICALP 2009, LTL Path Checking, Path Checking Algorithms, Path Checking Problem, Theoretical Computer Science