Хорошо структурированная переходная система - Well-structured transition system

В информатике, особенно в области формальная проверка, хорошо структурированные переходные системы (WSTS) представляют собой общий класс систем с бесконечным числом состояний, для которых многие проблемы проверки являются разрешимый, благодаря существованию своего рода порядок между состояниями системы, которая совместима с переходами системы. Результаты разрешимости WSTS могут быть применены к Сети Петри, системы каналов с потерями и многое другое.

Формальное определение

Напомним, что хорошо квазиупорядоченный на съемочной площадке это квазиупорядочение (т.е. Предварительный заказ или же рефлексивный, переходный бинарное отношение ) такая, что любая бесконечная последовательность элементов , из содержит возрастающую пару с . Набор как говорят квазиупорядоченный, или в ближайшее время wqo.

Для наших целей переходная система это структура , куда любой набор (его элементы называются состояния), и (его элементы называются переходы). В общем, система переходов может иметь дополнительную структуру, такую ​​как начальные состояния, метки переходов, принимающие состояния и т. Д. (Обозначены точками), но они здесь нас не касаются.

А хорошо структурированная переходная система состоит из переходной системы , так что

  • является хорошо квазиупорядоченным на множестве состояний.
  • обратно совместим с : то есть для всех переходов (под этим мы подразумеваем ) и для всех такой, что , Существует такой, что (то есть, можно добраться из последовательностью из нуля или более переходов) и .
Требование обратной совместимости

Хорошо структурированные системы

А хорошо структурированная система[1] это переходная система с набором состояний составленный из конечного состояние контроля набор , а значения данных набор , меблированная разрешимый Предварительный заказ который распространяется на государства , который хорошо структурирован, как определено выше ( является монотонным, т.е. совместимым снизу вверх, относительно ) и, кроме того, имеет вычислимый набор минимумов для набора предшественников любого вверх закрыт подмножество .

Хорошо структурированные системы адаптируют теорию хорошо структурированных переходных систем к моделированию определенных классов систем, встречающихся в Информатика и обеспечивают основу для процедур принятия решений для анализа таких систем, отсюда и дополнительные требования: само определение WSTS ничего не говорит о вычислимости отношений , .

Использование в компьютерных науках

Хорошо структурированные системы

Покрытие может быть определено для любой хорошо структурированной системы, как и достижимость данного состояния управления, посредством обратный алгоритм Абдуллы и др.[1] или для конкретных подклассов хорошо структурированных систем (при условии строгой монотонности,[2] например в случае неограниченного Сети Петри ) путем прогнозного анализа на основе метода Карпа-Миллера. покрываемость график.

Обратный алгоритм

Обратный алгоритм позволяет ответить на следующий вопрос: при наличии хорошо структурированной системы и состояния , есть ли какой-либо путь перехода, ведущий из заданного начального состояния в состояние (такое состояние называется крышка )?

Интуитивно понятное объяснение этого вопроса: если представляет состояние ошибки, затем любое состояние содержащий это также следует рассматривать как состояние ошибки. Если удастся найти хороший квазипорядок, который моделирует это «сдерживание» состояний и который также удовлетворяет требованию монотонности относительно переходного отношения, то на этот вопрос можно будет ответить.

Вместо одного минимального состояния ошибки , обычно рассматривается закрытый вверх набор состояний ошибки.

Алгоритм основан на том, что в хорошо квазипорядке , любое замкнутое вверх множество имеет конечное множество минимумов и любую последовательность замкнутых вверх подмножеств сходится после конечного числа шагов (1).

Алгоритм должен хранить закрытый вверх набор состояний в памяти, что он может делать, потому что замкнутое вверх множество можно представить как конечный набор минимумов. Он начинается с закрытия набора состояний ошибки снизу вверх. и вычисляет на каждой итерации набор (по монотонности, также замкнутый вверх) непосредственных предшественников и добавляя его к набору . Эта итерация завершается после конечного числа шагов из-за свойства (1) квазипорядков скважин. Если находится в окончательно полученном наборе, то вывод - «да» (состояние может быть достигнуто), в противном случае - «нет» (невозможно достичь такого состояния).

Рекомендации

  1. ^ а б Парош Азиз Абдулла, Карлис Черанс, Бенгт Йонссон, Йих-Куен Цай: Алгоритмический анализ программ с хорошо квазиупорядоченными доменами (2000), Информация и вычисления, Vol. 160 выпуски 1-2, с. 109--127
  2. ^ Ален Финкель и Филипп Шнебелен, Хорошо структурированные переходные системы везде!, Теоретическая информатика 256 (1-2), страницы 63–92, 2001.