Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds

TL;DR

This paper demonstrates that path checking for linear-time temporal logic (LTL) and its extensions with past and bounds can be efficiently parallelized, enabling faster verification processes.

Contribution

It introduces an efficient parallel algorithm for path checking in LTL, BLTL, and LTL+Past, extending the applicability to more expressive logics.

Findings

Path checking for LTL and extensions is in AC^1(logDCFL)

The algorithm is efficiently parallelizable for extended LTL logics

Extensions with past and bounds do not hinder parallelization efficiency

Abstract

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.