Программа поведенческого анализа вполне структурированных систем переходов

Модель вполне структурированных систем переходов все более широко используется в качестве инструмента исследования параллельных и распределенных систем. С помощью данного класса систем могут быть исследованы следующие проблемы: ограниченности, достижимости, покрытия, неизбежности, поддержки управляющего состояния, останова, – и другие семантические свойства. Несмотря на то, что модель вполне структурированных систем переходов известна и изучается уже несколько десятков лет, было замечено отсутствие практических результатов применения алгоритмов их анализа. Целью данной работы – является разработка программы для анализа поведенческих свойств вполне структурированных систем переходов. В работе рассматриваются два наиболее популярных алгоритма, используемых для изучения поведенческих свойств вполне структурированных систем переходов: Метод насыщения и Покрывающее дерево системы переходов. Для описания исследуемых формализмов и запуска указанных алгоритмов вводится язык программирования WSTSL, являющийся расширением языка SETL, который ориентирован на работу с множествами. Применимость подхода была продемонстрирована на примере эксперимента, в ходе которого была исследована производительность алгоритма построения Покрывающего дерева для сетей Петри, описывающих задачу об обедающих философах разного размера, и на основе которого было выявлено одно из потенциальных направлений для усовершенствования данного алгоритма. Ключевые слова: формальная верификация, системы переходов, правильные квазипорядки, сети Петри.