Переходная система

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

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

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

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

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

Формально переходная система представляет собой пару $(S,T)$ где $S$ представляет собой совокупность состояний и $T$ , отношение перехода , является подмножеством $S\times S$ . Мы говорим, что происходит переход из состояния $p$ заявить $q$ если только $(p,q)\in T$ , и обозначим его $p\rightarrow q$ .

Помеченная система переходов представляет собой кортеж $(S,\Lambda ,T)$ где $S$ представляет собой совокупность состояний, $\Lambda$ представляет собой набор меток, и $T$ , помеченное отношение перехода , является подмножеством $S\times \Lambda \times S$ . Мы говорим, что происходит переход из состояния $p$ заявить $q$ с этикеткой $\alpha$ если только $(p,\alpha ,q)\in T$ и обозначим это

p\xrightarrow {\alpha } q\,.

Метки могут обозначать разные вещи в зависимости от интересующего языка. Типичное использование меток включает представление ожидаемых входных данных, условий, которые должны быть истинными для запуска перехода, или действий, выполняемых во время перехода. Системы помеченных переходов изначально были представлены как системы поименованных переходов. ^[1]

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

Если для любого данного $p$ и $\alpha$ , существует только один кортеж $(p,\alpha ,q)$ в $T$ , тогда говорят, что $\alpha$ является детерминированным (для $p$ ).
Если для любого данного $p$ и $\alpha$ , существует хотя бы один кортеж $(p,\alpha ,q)$ в $T$ , тогда говорят, что $\alpha$ является исполняемым (для $p$ ).

Формулировка коалгебры

Формальное определение можно перефразировать следующим образом. Маркированные системы перехода состояний на $S$ с этикетками от $\Lambda$ соответствуют взаимно однозначно функциям $S\to {\mathcal {P}}(\Lambda \times S)$ , где ${\mathcal {P}}$ — (ковариантный) функтор степенного набора . При этой биекции $(S,\Lambda ,T)$ отправляется в $\xi _{T}:S\to {\mathcal {P}}(\Lambda \times S)$ , определяемый

p\mapsto \{\,(\alpha ,q)\in \Lambda \times S\mid p\xrightarrow {\alpha } q\,\}

.

Другими словами, помеченная система переходов состояний представляет собой коалгебру функтора $P(\Lambda \times {-})$ .

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

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

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

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

Расширения

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

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

См. также

Ссылки

^ Роберт М. Келлер (июль 1976 г.) « Формальная проверка параллельных программ », Сообщения ACM , том. 19 , номер. 7 , стр. 371–384.
^ Марк Безем, Дж. В. Клоп, Роэль де Вриер («Тереза»), Системы переписывания терминов , Cambridge University Press, 2003, ISBN 0-521-39115-6 . стр. 7–8.
^ Кристель Байер ; Йост-Питер Катоен (2008). Принципы проверки моделей . Массачусетский технологический институт Пресс. п. 20. ISBN 978-0-262-02649-9 .
^ Майкл Гельфонд, Владимир Лифшиц (1998) «Языки действий», Linköping Electronic Articles in Computer and Information Science , vol. 3 , номер. 16 .

[1] Роберт М. Келлер (июль 1976 г.) « Формальная проверка параллельных программ », Сообщения ACM , том. 19 , номер. 7 , стр. 371–384.

[2] Марк Безем, Дж. В. Клоп, Роэль де Вриер («Тереза»), Системы переписывания терминов , Cambridge University Press, 2003, ISBN 0-521-39115-6 . стр. 7–8.

[BaierKatoen2008-3] Кристель Байер ; Йост-Питер Катоен (2008). Принципы проверки моделей . Массачусетский технологический институт Пресс. п. 20. ISBN 978-0-262-02649-9 .

[4] Майкл Гельфонд, Владимир Лифшиц (1998) «Языки действий», Linköping Electronic Articles in Computer and Information Science , vol. 3 , номер. 16 .

[1]

[2]

[3]

[4]