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

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

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

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

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

Формальное определение [ править ]

Формально система переходов - это пара ( S , →), где S - это набор состояний, а → - отношение переходов состояний (т. Е. Подмножество S × S ). Переход из состояния p в состояние q , т.е. ( p , q ) ∈ →, записывается как p → q .

Меченная система перехода является кортежем ( S , Λ, →) , где S представляет собой набор состояний, Λ представляет собой набор меток и → это отношение меченых переходов (т.е. подмножество S × Л × S ). ( p , α, q ) ∈ → записывается как

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

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

Если для любых данных p и α существует только один набор ( p , α, q ) в →, то говорят, что α является детерминированным (для p ). Если для любых данных p и α существует хотя бы один кортеж ( p , α, q ) в →, то говорят, что α является исполняемым (для 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 Р (\ Лямбда \ раз -)}$

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

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

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

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

Расширения [ править ]

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

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

См. Также [ править ]

Ссылки [ править ]

^ Роберт М. Келлер (июль 1976 г.) " Формальная проверка параллельных программ ", Сообщения ACM , том. 19 , н. 7. С. 371–384.
^ Марк Bezem, JW Klop, Рул де Vrijer ( "Terese"), системы переписывания термов , Cambridge University Press, 2003, ISBN 0-521-39115-6 . С. 7–8.
^ Кристель Байер ; Йост-Питер Катоэн (2008). Принципы проверки моделей . MIT Press. п. 20. ISBN 978-0-262-02649-9.
^ Майкл Гельфонд, Владимир Лифшиц (1998) "Языки действий", Электронные статьи Linköping в области компьютерных и информационных наук , том. 3 , н. 16 .

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

[2] Марк Bezem, JW Klop, Рул де Vrijer ( "Terese"), системы переписывания термов , Cambridge University Press, 2003, ISBN 0-521-39115-6 . С. 7–8.

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

[4] Майкл Гельфонд, Владимир Лифшиц (1998) "Языки действий", Электронные статьи Linköping в области компьютерных и информационных наук , том. 3 , н. 16 .

[1]