Страница публикации

Метод булевых ограничений в качественном анализе двоичных динамических систем

Авторы: Опарин Г.А., Богданова В.Г., Пашинин А.А.

Журнал: Междунар. журнал прикладных и фундамент. исследований

Том:

Номер: 9

Год: 2018

Отчётный год: 2018

Издательство:

Местоположение издательства:

URL:

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

Индексируется WOS: 0

Индексируется Scopus: 0

Индексируется РИНЦ: 1

Публикация в печати: 0

Добавил в систему: