An experiment on parallel model checking of a CTL fragment

DOI10.1007/978-3-642-33386-6_23MaRDI QIDQ4649304zbMATH OpenOpenAlexFDO

Authors Rodrigo T. Saad, Silvano Dal Zilio, Bernard Berthomieu

Publication date 21 November 2012

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We propose a parallel algorithm for local, on the fly, model checking of a fragment of CTL that is well-suited for modern, multi-core architectures. This model-checking algorithm takes bene t from a parallel state space construction algorithm, which we described in a previous work, and shares the same basic set of principles: there are no assumptions on the models that can be analyzed; no restrictions on the way states are distributed; and no restrictions on the way work is shared among processors. We evaluate the performance of diff erent versions of our algorithm and compare our results with those obtained using other parallel model checking tools. One of the most novel contributions of this work is to study a space-e fficient variant for CTL model-checking that does not require to store the whole transition graph but that operates on a reverse spanning tree.

Recommendations

• CTL model checking on a shared-memory architecture
• CTL^* model checking on a shared-memory architecture
• Model Checking CTL is Almost Always Inherently Sequential
• Parallel model checking for \texttt{LTL}, \texttt{CTL}\(^*\), and \(L^2_{\mu}\)
• Parallel nested depth-first searches for LTL model checking

Cited in

(12)

• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
• CTL model checking on a shared-memory architecture
• Parallel model checking for \texttt{LTL}, \texttt{CTL}\(^*\), and \(L^2_{\mu}\)
• CTL^* model checking on a shared-memory architecture
• A stack-slicing algorithm for multi-core model checking
• Parallel nested depth-first searches for LTL model checking
• scientific article; zbMATH DE number 1746649 (Why is no real title available?)
• Parallelizing a symbolic compositional model-checking algorithm
• Towards Bounded Model Checking for the Universal Fragment of TCTL
• scientific article; zbMATH DE number 2188504 (Why is no real title available?)
• Model Checking Software
• Parallel Graph-Based Stateless Model Checking

This page was built for publication: An experiment on parallel model checking of a CTL fragment

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