Коммуникационный конечный автомат

В информатике , общающийся конечный автомат - это конечный автомат , помеченный операциями "получить" и "отправить" по некоторому алфавиту каналов. Они были введены Брандом и Зафиропуло, ^[1] и могут использоваться в качестве модели параллельных процессов, таких как сети Петри . Общающиеся конечные автоматы часто используются для моделирования протокола связи, поскольку они позволяют обнаруживать основные ошибки проектирования протокола, включая ограниченность, взаимоблокировки и неопределенные приемы. ^[2]

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

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

Иерархические конечные автоматы — это конечные автоматы, состояния которых сами могут быть другими автоматами. Поскольку общающийся конечный автомат характеризуется параллелизмом, наиболее заметной чертой общающегося иерархического конечного автомата является сосуществование иерархии и параллелизма. Это считается весьма подходящим, поскольку означает более сильное взаимодействие внутри автомата.

Однако было доказано, что сосуществование иерархии и параллелизма по сути своей стоит языковой инклюзивности, языковой эквивалентности и всей универсальности. ^[3]

Для произвольного положительного целого числа протокол ^{[1] : 3} с процессом ( ами) представляет собой четверку с:${\displaystyle N}$ ${\displaystyle N}$${\displaystyle \{(S_{i})_{i=1}^{N},\ (o_{i})_{i=1}^{N},\ (M_{i,j})_{i,j=1}^{N},\ ({\mathtt {succ}})_{i=1}^{N}\}}$

• ${\displaystyle (S_{i})_{i=1}^{N}}$, последовательность непересекающихся конечных множеств. Каждое множество используется для представления процесса, а каждый элемент представляет возможное состояние -го процесса.${\displaystyle N}$${\displaystyle S_{i}}$${\displaystyle я}$
• ${\displaystyle (o_{i})_{i=1}^{N}}$(с ), последовательность, представляющая начальное состояние каждого процесса.${\displaystyle o_{i}\in S_{i}}$
• ${\displaystyle (M_{i,j})_{i,j=1}^{N}}$, конечная последовательность непересекающихся конечных множеств, такая, что каждое множество представляет возможные сообщения, которые могут быть отправлены от процесса к процессу . Если , то пусто.${\displaystyle N^{2}}$${\displaystyle M_{i,j}}$${\displaystyle я}$${\displaystyle j}$${\displaystyle i=j}$${\displaystyle M_{i,j}}$
• ${\displaystyle ({\mathtt {succ}})_{i=1}^{N}:S_{i}\times \bigcup _{j=1}^{N}\left(M_{j,i}^{[+]}\cup M_{i,j}^{[-]}\right)\mapsto S_{i}}$представляет собой последовательность функций перехода. Каждая функция моделирует переход, который может быть выполнен путем передачи или получения любого сообщения. Что касается процесса , символ используется для обозначения сообщения, которое может быть получено, и сообщения, которое может быть отправлено.${\displaystyle я}$${\displaystyle [+]}$${\displaystyle [-]}$

Глобальное состояние — это пара , где ${\displaystyle \langle S,C\rangle}$

• ${\displaystyle S=(s_{1},...,s_{N})}$представляет собой упорядоченный набор состояний, каждый из которых представляет состояние -го процесса.${\displaystyle s_{i}}$${\displaystyle я}$
• ${\displaystyle С}$— это матрица, каждая из которой является подпоследовательностью .${\displaystyle N\times N}$${\displaystyle c_{i,j}\in C}$${\displaystyle M_{i,j}}$

Начальное глобальное состояние — это пара , где${\displaystyle \langle O,\mathrm {E} \rangle}$

• ${\displaystyle O=(o_{1},...,o_{N})}$
• ${\displaystyle \mathrm {E} }$определяется как матрица такая, что для всех , равно пустому слову, .${\displaystyle N\times N}$${\displaystyle i,j\in \{1,...,N\}}$${\displaystyle E_{i,j}}$${\displaystyle \epsilon}$

Существует два типа шагов: шаги, на которых сообщения принимаются, и шаги, на которых сообщения отправляются.

Шаг, на котором процесс получает сообщение, ранее отправленное -ым процессом, представляет собой пару вида когда , с . Аналогично, пара, на которой сообщение отправляется -ым процессом -ому , представляет собой пару вида когда ${\displaystyle j}$${\displaystyle я}$${\displaystyle \left\langle (s_{1},\dots ,s_{j},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &m_{i,j}c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle \vdash \left\langle (s_{1},\dots ,s'_{j},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\точки \\\точки &c_{i,j}&\точки \\\точки &\точки &\точки \\c_{n,1}&\точки &c_{n,n}\end{array}}\right)\right\rangle }$${\displaystyle {\mathtt {succ}}_{i}(s_{j},+m_{i,j})=s'_{j}}$${\displaystyle m'_{i,j}\in M_{i,j}}$${\displaystyle я}$${\displaystyle j}$${\displaystyle \left\langle (s_{1},\dots ,s_{i},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\dots &c_{i,j}&\dots \\\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle \vdash \left\langle (s_{1},\dots ,s'_{i},\dots ,s_{n}),\left({\begin{array}{lll}c_{1,1}&\dots &c_{1,n}\\\dots &\dots &\dots \\\точки &m_{i,j}c_{i,j}&\точки \\\точки &\точки &\точки \\c_{n,1}&\точки &c_{n,n}\end{array}}\right)\right\rangle }$${\displaystyle {\mathtt {succ}}_{i}(s_{i},-m_{i,j})=s'_{i}}$

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

Говорят, что глобальное состояние достижимо , если существует маршрут, проходящий через это состояние.${\displaystyle \langle S,C\rangle}$

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

Далее было доказано, что когда отношение приоритета сообщения пусто, ограниченность, тупики и неопределенное состояние приема могут быть определены даже при условии, что в коммуникации между конечными автоматами присутствуют два или более типов сообщений. ^[4]

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

Некоторые рассматриваемые расширения:

• наличие нотации, указывающей на то, что некоторые штаты могут не получать никаких сообщений,
• Сообщения принимаются в разном порядке, например FILO,
• некоторые сообщения могут потеряться,

Система каналов по сути является версией коммуникационного конечного автомата, в котором автомат не разделен на отдельные процессы. Таким образом, существует единое состояние состояния, и нет ограничений относительно того, какая система может читать/писать на любом канале.

Формально, если задан протокол , то его связанная система каналов имеет вид , где — набор из и из .${\ displaystyle \ langle (S_ {i}) _ {i = 1} ^ {n}, (o_ {i}) _ {i = 1} ^ {n}, (M_ {i, j}) _ {i, j = 1} ^ {n}, ({\ mathtt {succ}}) _ {i} \ rangle }$${\ displaystyle \ langle \ prod (S_ {i}) _ {i = 1} ^ {n}, (o_ {i}) _ {i = 1} ^ {n}, \ bigcup _ {i, j = 1} ^ {n} (M_ {i, j}), \ Delta \ rangle }$${\displaystyle \Дельта}$${\displaystyle ((s_{1},\dots ,s_{j},\dots ,s_{n}),?m_{i,j},(s_{1},\dots ,{\mathtt {succ}}_{j}(s_{j},+m_{i,j}),\dots ,s_{n})}$${\displaystyle ((s_{1},\dots ,s_{i},\dots ,s_{n}),!m_{i,j},(s_{1},\dots ,{\mathtt {succ}}_{i}(s_{i},-m_{i,j}),\dots ,s_{n})}$