Опарин Геннадий Анатольевич, Богданова Вера Геннадьевна, Горский Сергей Алексеевич

Институт динамики систем и теории управления имени В.М. Матросова Сибирского отделения Российской академии наук

Высокая вычислительная сложность ряда задач анализа динамики и структурно-параметрического синтеза для разных классов динамических управляемых систем обусловливает разработку методов и средств их параллельного решения. На основе метода булевых ограничений задачи качественного анализа поведения траекторий двоичных динамических систем, функционирование которых рассматривается на конечном интервале времени, сводятся к решению задач булевой выполнимости и проверки истинности квантифицированных булевых формул. Строится математическая модель исследуемого динамического свойства в виде системы булевых уравнений, учитывающая как спецификацию свойства, так и уравнения динамики конкретного объекта. Такой подход, в отличие от существующих, является декларативным и обеспечивает возможность параллелизма по данным. Для проверки истинности 2-квантифицированных булевых формул разработан параллельный решатель Hpc2qall. В отличие от аналогичных решателей, Hpc2qall выдает не только результат проверки истинности формулы (SAT или UNSAT), но и осуществляет конструктивное нахождение всех наборов значений переменных под квантором всеобщности, приводящих к результату UNSAT. Приводится пример применения конструктивного подхода для решения задачи синтеза стабилизирующей обратной связи.

двоичная динамическая система, булева модель, параллельный 2QBF решатель, качественный анализ