LTL Path Checking Is Efficiently Parallelizable

14 years 7 months ago
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...
Lars Kuhtz, Bernd Finkbeiner
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2009
Authors Lars Kuhtz, Bernd Finkbeiner
Comments (0)