Compositional Verification Using Geodesic Distance via Assume-Guarantee Reasoning

Abstract

Assume-guarantee reasoning is indeed an effective compositional verification technique that can help mitigate the state explosion problem in model checking. However, the biggest challenge of applying assume-guarantee reasoning is how to best decompose a system. This paper presents a novel compositional verification frame based on geodesic distance. The proposed algorithm introduces novel techniques to decompose system components into groups. The algorithm’s effectiveness and efficiency are evaluated through a comparative analysis with four state-of-the-art methods commonly used in the field. The results of the comparison consistently demonstrate that the proposed algorithm outperforms the state-of-the-art methods. This implies that the new algorithm exhibits superior performance in terms of decomposition quality and verification efficiency.

Keywords

• Model checking
• compositional verification
• assume-guarantee reasoning
• group technology
• combinatorial testing
• geodesic distance