Model Checking Based on Simultaneous Reachability Analysis

Abstract. Simultaneous reachability analysis SRA is a recently proposed approach to alleviating the state space explosion problem in reachability analysis of concurrent systems. The concept of SRA is to allow a global transition in a reachability graph to contain a set of transitions of di erent processes such that the state reached by the global transition is independent of the execution order of the associated process transitions. In this paper, we describe how to apply the SRA approach to concurrent systems for model checking. We rst describe an SRA-based framework for producing a reduced state graph that provides su cient information for model checking. Following this framework, we present an algorithm that generates a reduced state graph for the extended nite state machine EFSM model with multiple ports. Empirical results indicate that, our SRA reduction algorithm performs as good as or better than the partial order reduction algorithm in SPIN.

• Type: Conference
• Year: 2000
• Where: SPIN
• Authors: Bengi Karaçali, Kuo-Chung Tai
• Keywords: Reachability Analysis Sra, Reduced State Graph, SPIN 2000, SRA Reduction Algorithm, Theoretical Computer Science