Efficient parallel path checking for linear-time temporal logic with past and bounds

DOI10.2168/LMCS-8(4:10)2012MaRDI QIDQ4899110zbMATH OpenFDO

Authors Lars Kuhtz, Bernd Finkbeiner

Publication date 7 January 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1210.0574

zbMATH Keywords

bounded temporal operatorslinear-time temporal logic (LTL)linear-time temporal logic with pastmodel checkingparallel complexitypath checking

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• LTL Path Checking Is Efficiently Parallelizable
• On the Complexity of Temporal-Logic Path Checking
• Parallel model checking for \texttt{LTL}, \texttt{CTL}\(^*\), and \(L^2_{\mu}\)
• Model checking a path (preliminary report)
• scientific article; zbMATH DE number 1956570

Cited in

(7)

• Past is for free: On the complexity of verifying linear temporal properties with past
• A survey of challenges for runtime verification from advanced application domains (beyond software)
• A theory of monitors
• LTL Path Checking Is Efficiently Parallelizable
• On the Complexity of Temporal-Logic Path Checking
• Model checking a path (preliminary report)
• The ins and outs of first-order runtime verification

This page was built for publication: Efficient parallel path checking for linear-time temporal logic with past and bounds

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4899110)