A Combined Approach for Reachability Analysis

This paper presents the principle of an approach that allows to analyse most important system properties like reachability, executability, deadlock-freeness etc. The approach is based on two concepts: analysis purpose-directed analysis and specification unfolding. The first concept drives the analysis to the aimed specification part whereas the second allows to present the specification behaviour in a suitable form for the analysis. In contrast to the common analysis methods, the present approach considerably alleviates the state-explosion problem.