Lars Kuhtz ; Bernd Finkbeiner - Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds

lmcs:1219 - Logical Methods in Computer Science, October 23, 2012, Volume 8, Issue 4 - https://doi.org/10.2168/LMCS-8(4:10)2012
Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds

Authors: Lars Kuhtz ; Bernd Finkbeiner

    Path checking, the special case of the model checking problem where the model under consideration is a single path, plays an important role in monitoring, testing, and verification. We prove that for linear-time temporal logic (LTL), path checking can be efficiently parallelized. In addition to the core logic, we consider the extensions of LTL with bounded-future (BLTL) and past-time (LTL+Past) operators. Even though both extensions improve the succinctness of the logic exponentially, path checking remains efficiently parallelizable: Our algorithm for LTL, LTL+Past, and BLTL+Past is in AC^1(logDCFL) \subseteq NC.


    Volume: Volume 8, Issue 4
    Published on: October 23, 2012
    Accepted on: June 25, 2015
    Submitted on: January 4, 2010
    Keywords: Computer Science - Logic in Computer Science,F.4.1, F.2.2

    7 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 340 times.
    This article's PDF has been downloaded 196 times.