Система перехода - Transition system

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

Системы переходов математически совпадают с абстрактными системами перезаписи (как описано далее в этой статье) и ориентированными графами . Они отличаются от конечных автоматов по нескольким параметрам:

Набор состояний не обязательно конечный или даже счетный.
Набор переходов не обязательно конечный или даже счетный.
Никакого "начального" или "конечного" состояния не дается.

Системы переходов можно представить в виде ориентированных графов.

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

Формально система переходов - это пара, где - набор состояний и отношение переходов состояний (т. Е. Подмножество ). Переход из состояния в состояние (т.е. ) записывается как . ${\ displaystyle (S, \ rightarrow)}$ ${\ displaystyle S}$ ${\ displaystyle \ rightarrow}$ ${\ displaystyle S \ times S}$ ${\ displaystyle p}$ ${\ displaystyle q}$ ${\ displaystyle (p, q) \ in \ rightarrow}$ ${\ displaystyle p \ rightarrow q}$

Меченная система перехода является кортежем , где находится множество состояний, представляет собой набор меток, и это отношение меченых переходов (то есть, подмножество ). записывается как ${\ displaystyle (S, \ Lambda, \ rightarrow)}$ ${\ displaystyle S}$ ${\ displaystyle \ Lambda}$ ${\ displaystyle \ rightarrow}$ ${\ Displaystyle S \ times \ Lambda \ times S}$ ${\ Displaystyle (п, \ альфа, д) \ в \ rightarrow}$

{\ displaystyle p {\ overset {\ alpha} {\ rightarrow}} q \,}

и представляет переход из состояния в состояние с меткой . Ярлыки могут представлять разные вещи в зависимости от интересующего языка. Типичное использование меток включает представление ожидаемого ввода, условий, которые должны быть истинными для запуска перехода, или действий, выполняемых во время перехода. Системы маркированных переходов были первоначально представлены как системы именованных переходов. ${\ displaystyle p}$ ${\ displaystyle q}$ ${\ displaystyle \ alpha}$

Особые случаи

Если для любого заданного и существует только один кортеж в , то говорят, что это детерминированный (для ). ${\ displaystyle p}$ ${\ displaystyle \ alpha}$ ${\ Displaystyle (п, \ альфа, q)}$ ${\ displaystyle \ rightarrow}$ ${\ displaystyle \ alpha}$ ${\ displaystyle p}$
Если для любого заданного и существует хотя бы один кортеж в , то говорят, что он является исполняемым (для ). ${\ displaystyle p}$ ${\ displaystyle \ alpha}$ ${\ Displaystyle (п, \ альфа, q)}$ ${\ displaystyle \ rightarrow}$ ${\ displaystyle \ alpha}$ ${\ displaystyle p}$

Теоретико-категориальная формализация

Формальное определение можно перефразировать в терминах теории категорий. Каждая система меченного перехода состояния является взаимно однозначно зависит от к Powerset из индексируются записывается в виде , определенном ${\ displaystyle (S, \ Lambda, \ rightarrow)}$ ${\ displaystyle \ xi _ {\ rightarrow}}$ ${\ displaystyle S}$ ${\ displaystyle S}$ ${\ displaystyle \ Lambda}$ ${\ Displaystyle {\ mathcal {P}} (\ Lambda \ times S)}$

{\ displaystyle p \ mapsto \ {(\ alpha, q) \ in \ Lambda \ times S: p {\ overset {\ alpha} {\ rightarrow}} q \}.}

.

Следовательно, помеченная система переходов состояний является F-коалгеброй для функтора . ${\ Displaystyle Р (\ Лямбда \ раз -)}$

Связь между маркированной и немаркированной переходной системой

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

Сравнение с абстрактными системами перезаписи

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

Расширения

При проверке модели иногда определяется система переходов, включающая также дополнительную функцию маркировки для состояний, в результате чего возникает понятие, охватывающее структуру Крипке .

Языки действий являются расширениями переходных систем, добавив множество флюента F , множество значений V , а функция , которая отображает F × S в V .

Languages

In other projects