Accelerating Possibilistic Model Checking: Sparse Engine for Large-Scale Models
摘要
Possibilistic model checking technique is a method that uses mathematical approaches to verify the quantitative performance of fuzzy systems. This paper addresses computational efficiency challenges in possibilistic model checking for large-scale fuzzy systems. We propose three optimizations: Two single-state transitive closure algorithms—TCWSS (Warshall-based) for dense models and TCDM (max-heap-accelerated Dijkstra) for sparse cases, selected adaptively via a sparse engine; A sorting-based vector operation technique replacing fuzzy matrix computations. Experiments demonstrate significant time reduction, achieving a 25× speedup in dense models and a 50× acceleration in sparse models.