Построение сокращенного дерева достижимости для моделей программ в терминах сетей Петри

Рассматривается задача построения пространства состояний для анализа поведения императивных программ. При автоматическом построении моделей программ эффект взрыва числа анализируемых состояний составляет основную проблему для поиска ошибок в исходных текстах программ, причем этот взрыв индуцируется за счет состояния множества переменных программы. Предлагается подход к уменьшению числа состояний дерева достижимости моделей программ через отделение модели потока управления программой от моделей переменных и последующего добавления только переменных, влияющих на поток управления, и сокращения состояний этих переменных. Рассмотренный в статье пример показывает, как на практике может быть применен такой подход.