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

Конечный автомат, который может иметь бесконечное количество состояний

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

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

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

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

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

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

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

${\displaystyle p\xrightarrow {\alpha } q\,.}$

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

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

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

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

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

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

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

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

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

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

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

Расширения

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

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

Смотрите также

• Бинарное отношение
• Тройное отношение
• Переходный моноид
• Моноид преобразования
• Действие полугруппы
• Предварительный заказ симуляции
• Бисимуляция
• Операционная семантика
• Структура Крипке
• Конечный автомат
• Модальное μ-исчисление

Ссылки

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