Distributed Maximality based CTL Model Checking
In this paper we investigate an approach to perform a distributed CTL Model checker algorithm on a network of workstations using Kleen three value logic, the state spaces is partitioned among the network nodes, We represent the incomplete state spaces as a Maximality labeled Transition System MLTS which are able to express true concurrency. we execute in parallel the same algorithm in each node, for a certain property <symbol> on an incomplete MLTS , this last compute the set of states which satisfy <symbol> or which if they fail <symbol> are assigned the value <symbol> .The third value <symbol> mean unknown whether true or false because the partial state space lacks sufficient information needed for a precise answer concerning the complete state space .To solve this problem each node exchange the information needed to conclude the result about the complete state space. The experimental version of the algorithm is currently being implemented using the functional programming language Erlang.
Keywords: True concurrency semantics, State space explosion problem, Distributed model checking, three value logic
Download Full-Text
