An Approach to Cope with the State Space Explosion Problem in Graph Transformation Systems Using PSO and GSA Algorithms

One of the best solutions to verify software systems (especially critical systems) is model checking in which all reachable states are generated from an initial state and the generated state space is searched to find errors or some desirable patterns. However, the problem for many real and complex systems is the state space explosion in which model checking cannot generate all the states. In this paper, a solution is presented to cope with this problem in systems modeled by graph transformation. Since meta-heuristic algorithms are proper solutions to search in very large problem spaces, they employed in this research to find errors (e.g. deadlocks) in systems which cannot be verified through existing model checking approaches because of state space explosion problem. To do so, a Particle Swarm optimization (PSO) algorithm is empployed to consider only a subset of states (called population) in each step of the algorithm. To avoid local optima problem, PSO is combined with Gravitational Search Algorithm (GSA). Our proposed approach is implemented in GROOVE –a toolset for designing and model checking graph transformation system-. The experiments show better results in terms of accuracy, speed and memory usage in comparison with the existing approaches.