Constructing of the brief reachability tree for program models in terms of Petri nets

The article deals with the problem of building a state space for analyzing the imperative programs behavior. The state explosion problem of analyzed states number in the automatic program models construction is the main problem for finding errors in the programs source code. This explosion is induced mainly due to the composition of the program variables states. The article proposes an approach to reducing the number of states of the reachability tree of program models by separating the program control flow model from the variable models and then adding only variables that affect the control flow and reducing the states of these variables. The example considered in the article shows how such an approach can be applied in practice.