Применение позитивно-образованных формул для исследования частично-наблюдаемых ДСС

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