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 different 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 first describe an SRA-based framework for producing a reduced state graph that provides sufficient information for model checking. Following this framework, we present an algorithm that generates a reduced state graph for the extended finite 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.