LTL Path Checking Is Efficiently Parallelizable

DOI10.1007/978-3-642-02930-1_20MaRDI QIDQ3638098zbMATH OpenOpenAlexFDO

Authors Lars Kuhtz, Bernd Finkbeiner

Publication date 14 July 2009

Published in Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02930-1_20

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Efficient parallel path checking for linear-time temporal logic with past and bounds
• Parallel model checking for \texttt{LTL}, \texttt{CTL}\(^*\), and \(L^2_{\mu}\)
• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
• Parallel nested depth-first searches for LTL model checking
• Efficient model checking algorithms for computation tree logic and their application to the verification of parallel programs

Cited in

(7)

• Team semantics for the specification and verification of hyperproperties
• The complexity of counting models of linear-time temporal logic
• Weak Kripke structures and LTL
• scientific article; zbMATH DE number 7056237 (Why is no real title available?)
• A survey of challenges for runtime verification from advanced application domains (beyond software)
• Efficient parallel path checking for linear-time temporal logic with past and bounds
• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties

This page was built for publication: LTL Path Checking Is Efficiently Parallelizable

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