Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds
Logic in Computer Science
2019-03-14 v2
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.
Cite
@article{arxiv.1210.0574,
title = {Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds},
author = {Lars Kuhtz and Bernd Finkbeiner},
journal= {arXiv preprint arXiv:1210.0574},
year = {2019}
}