Title: Distributed model-checking and counterexample search for CTL logic


Author: Mohand Cherif Boukala; Laure Petrucci


LSI, Computer Science Department, USTHB, BP 32 El-Alia, Algiers, Algeria.
LIPN, CNRS UMR 7030, Université Paris XIII, 99, avenue Jean-Baptiste Clément, F-93430 Villetaneuse, France


Journal: Int. J. of Critical Computer-Based Systems, 2012 Vol.3, No.1/2, pp.44 - 59


Abstract: In this paper, we propose a distributed algorithm for CTL model-checking and a counterexample search whenever the CTL formula is not satisfied. The distributed approach is used in order to cope with the state space explosion problem. A cluster of workstations performs collaborative verification over a partitioned state space. Thus, every process involved in the distributed verification performs the labelling procedure on its own partial state space, and uses the parse tree of the CTL formula to evaluate sub-formulas and delay the synchronisations so as to minimise idle time. A counterexample search consists in a distributed construction of the tree-like corresponding to the failure executions. Some experiments have been carried out to evaluate the efficiency of this approach.


Keywords: system verification; critical systems; temporal logic; CTL model checking; branching time logic; distributed model checking; counterexamples search; state space explosion; collaborative verification; workstation clusters.


DOI: http://dx.doi.org/10.1504/IJCCBS.2012.045076


Available online 24 Jan 2012



Editors Full Text AccessAccess for SubscribersPurchase this articleComment on this article