Semi-distributed LTL model checking for actor based modeling languages

The major difficulty of model checking is state space explosion. Many approaches have been suggested to postpone such explosion to achieve model checking of superior models. Some of these approaches distribute states among grid nodes. Therefore state space size can be enlarged according to the number of grid nodes. Complexity of distributed model checking algorithm and lack of distributed reduction techniques are obstacles of these approaches. In this paper, we introduce semi-distributed model checking algorithm which is developed for actor based modelling languages with asynchronous message passing. Semi-distributed algorithm is a kind of centralized algorithm that stores light weight states in a central node. As a result, the central node can store larger state spaces. Experimental results show substantial improvement for semi-distributed algorithm decreases response time over the past results.