Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Distributed CTL Model-Checking and counterexample search

    Third International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2009)

    Rabat, Morroco, 2 - 3 July 2009


    M.C. Boukala and L. Petrucci


    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 executes a 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.


    PDF filePDF Version of this Paper (138kb)