Хорошо структурированная система перехода

В информатике, особенно в области формальной верификации , хорошо структурированные системы переходов (WSTS) представляют собой общий класс систем с бесконечными состояниями, для которых многие проблемы верификации разрешимы из-за существования своего рода порядка между состояниями системы. система, совместимая с переходами системы.Первое определение общей хорошо структурированной переходной системы (WSTS) было введено Аленом Финкелем в его статье ICALP 1987 года под названием «Обобщение процедуры Карпа и Миллера для хорошо структурированных переходных систем».Результаты разрешимости WSTS могут быть применены к сетям Петри , системам каналов с потерями и т. д.

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

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

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

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

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

Требование восходящей совместимости

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

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

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

Использование в информатике

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

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

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

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

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

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

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

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