An Incremental Optimization Algorithm for Efficient Verification of Graph Transformation Systems

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...

Full description

Saved in:
Bibliographic Details
Published in:IEEE access 2023-01, Vol.11, p.1-1
Main Authors: Nejati, Faranak, Hamid, Nor Asilah Wati Abdul, Koohi, Sina Zangbari, Zadeh, Zahra Rahmani
Format: Article
Language:English
Subjects:
Algorithms
Artificial intelligence
Computing time
Consumption
Formal verification
Graph theory
Graph Transformation Systems
Grooves
Heuristic methods
Metaheuristics
Model checking
Optimization
Optimization algorithms
Optimized production technology
Raccoon Optimization Algorithm
Searching
Sociology
Software Verification
State Space Explosion
State-space methods
Statistics
System recovery
Verification
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2169-3536
2169-3536
DOI:10.1109/ACCESS.2023.3291412