Umeå University's logo

Model checking has become a widely used and precise technique for verifying software systems. However, a major challenge in model checking is state space explosion, which occurs due to the exponential memory usage required by the model checker. To address this issue, meta-heuristic and evolutionary algorithms offer a promising solution by searching for a state where a property is either satisfied or violated. Recently, various evolutionary algorithms, such as Genetic Algorithms and Particle Swarm Optimization, have been applied to detect deadlock states. While these approaches have been useful, they primarily focus on deadlock detection. This paper proposes a fuzzy algorithm to analyse reachability properties in systems specified through Graph Transformation Systems with large state spaces. To achieve this, the existing Particle Swarm Optimisation algorithm, which is typically used for deadlock detection, has been extended to analyse reachability properties. To further enhance accuracy, a Fuzzy Adaptive Particle Swarm Optimization algorithm is introduced to determine which states and paths should be explored at each step-in order to find the corresponding reachable state. Additionally, the proposed hybrid algorithm was applied to models generated through rule composition to assess the impact of rule composition on execution time and the number of explored states. These approaches were implemented within an open-source toolset called GROOVE, which is used for designing and model checking Graph Transformation Systems. Experimental results demonstrate that proposed hybrid algorithm reduced verification time by up to 49.86% compared to Particle Swarm Optimization and 65.17% compared to Genetic Algorithms in reachability analysis of complex models. Furthermore, it explored 32.7% fewer states on average than the hybrid method based on Particle Swarm Optimization and Gravitational Search Algorithms, and 57.4% fewer states compared to Genetic Algorithms, indicating improved search efficiency. The application of rule composition further reduced execution time by 35.7% and the number of explored states by 41.2% in large-scale models. These results confirm that proposed hybrid algorithm significantly enhances reachability analysis in the systems modelled via Graph Transformation, improving both computational efficiency and scalability.