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

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

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

Напомним, что хорошо квазиупорядоченный ${\displaystyle \leq }$ на съемочной площадке ${\displaystyle X}$ это квазиупорядочение (т.е. Предварительный заказ или же рефлексивный, переходный бинарное отношение ) такая, что любая бесконечная последовательность элементов ${\displaystyle x_{0},x_{1},x_{2},\ldots }$, из ${\displaystyle X}$ содержит возрастающую пару ${\displaystyle x_{i}\leq x_{j}}$ с ${\displaystyle i<j}$. Набор ${\displaystyle X}$ как говорят квазиупорядоченный, или в ближайшее время wqo.

Для наших целей переходная система это структура ${\displaystyle {\mathcal {S}}=\langle S,\rightarrow ,\cdots \rangle }$, куда ${\displaystyle S}$ любой набор (его элементы называются состояния), и ${\displaystyle \rightarrow \subseteq S\times S}$ (его элементы называются переходы). В общем, система переходов может иметь дополнительную структуру, такую ​​как начальные состояния, метки переходов, принимающие состояния и т. Д. (Обозначены точками), но они здесь нас не касаются.

А хорошо структурированная переходная система состоит из переходной системы ${\displaystyle \langle S,\to ,\leq \rangle }$, так что

• ${\displaystyle \leq \subseteq S\times S}$ является хорошо квазиупорядоченным на множестве состояний.
• ${\displaystyle \leq }$ обратно совместим с ${\displaystyle \to }$: то есть для всех переходов ${\displaystyle s_{1}\to s_{2}}$ (под этим мы подразумеваем ${\displaystyle (s_{1},s_{2})\in \to }$) и для всех ${\displaystyle t_{1}}$ такой, что ${\displaystyle s_{1}\leq t_{1}}$, Существует ${\displaystyle t_{2}}$ такой, что ${\displaystyle t_{1}{\xrightarrow {*}}t_{2}}$ (то есть, ${\displaystyle t_{2}}$ можно добраться из ${\displaystyle t_{1}}$ последовательностью из нуля или более переходов) и ${\displaystyle s_{2}\leq t_{2}}$.

Требование обратной совместимости

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

А хорошо структурированная система^[1] это переходная система ${\displaystyle (S,\to )}$ с набором состояний ${\displaystyle S=Q\times D}$ составленный из конечного состояние контроля набор ${\displaystyle Q}$, а значения данных набор ${\displaystyle D}$, меблированная разрешимый Предварительный заказ ${\displaystyle \leq \subseteq D\times D}$ который распространяется на государства ${\displaystyle (q,d)\leq (q',d')\Leftrightarrow q=q'\wedge d\leq d'}$, который хорошо структурирован, как определено выше (${\displaystyle \to }$ является монотонным, т.е. совместимым снизу вверх, относительно ${\displaystyle \leq }$) и, кроме того, имеет вычислимый набор минимумов для набора предшественников любого вверх закрыт подмножество ${\displaystyle S}$.

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

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

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

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

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

Обратный алгоритм позволяет ответить на следующий вопрос: при наличии хорошо структурированной системы и состояния ${\displaystyle s}$, есть ли какой-либо путь перехода, ведущий из заданного начального состояния ${\displaystyle s_{0}}$ в состояние ${\displaystyle s'\geq s}$ (такое состояние называется крышка ${\displaystyle s}$)?

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

Вместо одного минимального состояния ошибки ${\displaystyle s}$, обычно рассматривается закрытый вверх набор ${\displaystyle S_{e}}$ состояний ошибки.

Алгоритм основан на том, что в хорошо квазипорядке ${\displaystyle (A,\leq )}$, любое замкнутое вверх множество имеет конечное множество минимумов и любую последовательность ${\displaystyle S_{1}\subseteq S_{2}\subseteq ...}$ замкнутых вверх подмножеств ${\displaystyle A}$ сходится после конечного числа шагов (1).

Алгоритм должен хранить закрытый вверх набор ${\displaystyle S_{s}}$ состояний в памяти, что он может делать, потому что замкнутое вверх множество можно представить как конечный набор минимумов. Он начинается с закрытия набора состояний ошибки снизу вверх. ${\displaystyle S_{e}}$ и вычисляет на каждой итерации набор (по монотонности, также замкнутый вверх) непосредственных предшественников и добавляя его к набору ${\displaystyle S_{s}}$. Эта итерация завершается после конечного числа шагов из-за свойства (1) квазипорядков скважин. Если ${\displaystyle s_{0}}$ находится в окончательно полученном наборе, то вывод - «да» (состояние ${\displaystyle S_{e}}$ может быть достигнуто), в противном случае - «нет» (невозможно достичь такого состояния).

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

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