An Incremental Optimization Algorithm for Efficient Verification of Graph Transformation Systems

Abstract

This paper proposes an incremental optimization framework for verifying graph transformation systems to overcome the state space explosion (SSE). SSE refers to the exponential growth of the number of possible states in a system during its verification. The framework maps the verification problem to a search problem and incrementally generates the state space. The generated increments can still be significant in size, thus we use the Raccoon Optimization Algorithm (ROA), to non-exhaustively search through the state space. ROA selects sequences of states with a higher potential of having deadlock in increments, which prevents SSE and ensures that memory capacity is not exceeded. However, there is possibility that the migration method of ROA lead to a loss of diversity in the population, reducing the algorithm’s ability to explore new regions of the search space. To address this issue, we propose a new migration method for ROA, called Improved ROA (IROA), which preserves diversity in the population and reduces execution time and the risk of getting stuck in local optima. Our approach is evaluated using the Groove simulation tool and compared with other relevant meta-heuristic algorithms in terms of computation time and memory consumption. The experimental results show that IROA outperforms both ROA and other relevant meta-heuristic algorithms that we compared in terms of computation time and memory consumption, with total efficiency of 1.043 and 1.02, respectively, demonstrating its effectiveness in verifying massive state spaces without facing state space explosion in a reasonable time.

Keywords

• Artificial intelligence
• raccoon optimization algorithm
• software verification
• model checking
• graph transformation systems
• state space explosion