Метод верификации свойств реактивной системы на модели

В работе описывается подход к верификации асинхронных дискретных динамических реактивных систем, основанный на использовании темпоральной логики (CTL - Computation Tree Logic), сетей Петри (СП) и систем линейных диофантовых ограничений (СЛДО).