Parallel model checking for \texttt{LTL}, \texttt{CTL}^*, and L^2_

zbMATH Open1271.68142MaRDI QIDQ2845488FDOQ2845488

Authors Martin Leucker, Rafał Somla, Michael Weber 

Publication date 30 August 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066105800933

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Parallel algorithms in computer science (68W10) Temporal logic (03B44)

Recommendations

• scientific article; zbMATH DE number 1705169
• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
• scientific article; zbMATH DE number 2087626
• Parallel nested depth-first searches for LTL model checking
• An experiment on parallel model checking of a CTL fragment
• Efficient model checking algorithms for computation tree logic and their application to the verification of parallel programs

Cited in

(11)

• An experiment on parallel model checking of a CTL fragment
• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
• scientific article; zbMATH DE number 1705169 (Why is no real title available?)
• scientific article; zbMATH DE number 2087626 (Why is no real title available?)
• CUDA accelerated LTL model checking -- revisited
• Efficient parallel path checking for linear-time temporal logic with past and bounds
• LTL Path Checking Is Efficiently Parallelizable
• CTL\(^*\) model checking on a shared-memory architecture
• A Multi-Core Solver for Parity Games
• Parallel Explicit Model Checking for Generalized Büchi Automata
• Parallel and symbolic model checking for fixpoint logic with chop

This page was built for publication: Parallel model checking for \texttt{LTL}, \texttt{CTL}\(^*\), and \(L^2_{\mu}\)

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