LTL Path Checking is Efficiently Parallelizable

Best paper award
Lars Kuhtz and Bernd Finkbeiner
PDF 
@InProceedings{KuhtzFinkbeiner09,
    author = {Lars Kuhtz and Bernd Finkbeiner},
    title = {{LTL} Path Checking is Efficiently Parallelizable},
    booktitle = {Proceedings of the 36th International Colloquium on Automata, Languages and Programming (ICALP 2009), Part II},
    editor = {Susanne Albers and Alberto Marchetti-Spaccamela and Yossi Matias and Sotiris Nikoletseas and Wolfgang Thomas},
    series = {LNCS},
    volume = {5556},
    publisher = {Springer},
    year = {2009},
    pages = {235--246}
}

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 July 2009
Contact Data Privacy Policy Imprint
Home People Publications
More