Finite-State-Maschine kommunizieren - Communicating finite-state machine

In der Informatik ist eine kommunizierende Finite-State-Maschine eine Finite-State-Maschine, die mit "Empfangen" - und "Senden" -Operationen über ein Alphabet von Kanälen gekennzeichnet ist. Sie wurden von Brand und Zafiropulo eingeführt und können als Modell für gleichzeitige Prozesse wie Petri-Netze verwendet werden . Kommunizierende Finite-State-Maschinen werden häufig zur Modellierung eines Kommunikationsprotokolls verwendet, da sie es ermöglichen, größere Fehler beim Protokolldesign zu erkennen, einschließlich Begrenztheit, Deadlocks und nicht spezifizierter Empfänge.

Der Vorteil der Kommunikation von Finite-State-Maschinen besteht darin, dass sie es ermöglichen, viele Eigenschaften in Kommunikationsprotokollen zu bestimmen, die über die bloße Erkennung solcher Eigenschaften hinausgehen. Dieser Vorteil schließt die Notwendigkeit menschlicher Hilfe oder Einschränkung im Allgemeinen aus.

Die Kommunikation von Finite-State-Maschinen kann in Situationen, in denen die Laufzeitverzögerung nicht vernachlässigbar ist (so dass mehrere Nachrichten gleichzeitig übertragen werden können), und in Situationen, in denen es selbstverständlich ist, die Protokollparteien und das Kommunikationsmedium zu beschreiben, leistungsfähiger sein als Finite-State-Maschinen als separate Einheiten.

Hierarchische Zustandsmaschine kommunizieren

Hierarchische Zustandsmaschinen sind endliche Zustandsmaschinen, deren Zustände selbst andere Maschinen sein können. Da eine kommunizierende endliche Zustandsmaschine durch Parallelität gekennzeichnet ist, ist das bemerkenswerteste Merkmal einer kommunizierenden hierarchischen Zustandsmaschine die Koexistenz von Hierarchie und Parallelität. Dies wurde als sehr gut geeignet angesehen, da es eine stärkere Interaktion innerhalb der Maschine bedeutet.

Es wurde jedoch bewiesen, dass die Koexistenz von Hierarchie und Parallelität die Einbeziehung der Sprache, die Sprachäquivalenz und die gesamte Universalität in sich kostet.

Definition

Protokoll

Für eine beliebige positive ganze Zahl ist ein Protokoll mit Prozessen ein Vierfaches mit: ${\ 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}}$, eine Folge von disjunkten endlichen Mengen. Jede Menge wird verwendet, um einen Prozess darzustellen, und jedes Element von repräsentiert einen möglichen Zustand des -ten Prozesses.${\ displaystyle N}$${\ displaystyle S_ {i}}$${\ displaystyle i}$
• ${\ displaystyle (o_ {i}) _ {i = 1} ^ {N}}$(mit ) eine Sequenz, die den Anfangszustand jedes Prozesses darstellt.${\ displaystyle o_ {i} \ in S_ {i}}$
• ${\ displaystyle (M_ {i, j}) _ {i, j = 1} ^ {N}}$eine endliche Folge von disjunkten endlichen Mengen, so dass jede Menge die möglichen Nachrichten darstellt, die von Prozess zu Prozess gesendet werden können . Wenn , dann ist leer.${\ displaystyle N ^ {2}}$${\ displaystyle M_ {i, j}}$${\ displaystyle i}$${\ 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}}$ist eine Folge von Übergangsfunktionen. Jede Funktion modelliert den Übergang, der durch Senden oder Empfangen einer Nachricht ausgeführt werden kann. In Bezug auf den Prozess wird das Symbol verwendet, um eine Nachricht zu notieren, die empfangen werden kann, und eine Nachricht, die gesendet werden kann.${\ displaystyle i}$${\ displaystyle [+]}$${\ displaystyle [-]}$

Globaler Zustand

Ein globaler Staat ist ein Paar, in dem ${\ displaystyle \ langle S, C \ rangle}$

• ${\ displaystyle S = (s_ {1}, ..., s_ {N})}$ist eine geordnete Sammlung von Zuständen, so dass jeder einen Zustand des -ten Prozesses darstellt.${\ displaystyle s_ {i}}$${\ displaystyle i}$
• ${\ displaystyle C}$ist eine Matrix, so dass jede eine Teilfolge von ist .${\ displaystyle N \ times N}$${\ displaystyle c_ {i, j} \ in C}$${\ displaystyle M_ {i, j}}$

Der anfängliche globale Zustand ist ein Paar, bei dem ${\ displaystyle \ langle O, \ mathrm {E} \ rangle}$

• ${\ displaystyle O = (o_ {1}, ..., o_ {N})}$
• ${\ displaystyle \ mathrm {E}}$definiert ist , eine sein , Matrix , so dass für alle , das leere Wort entspricht .${\ displaystyle N \ times N}$${\ displaystyle i, j \ in \ {1, ..., N \}}$${\ displaystyle E_ {i, j}}$${\ displaystyle \ epsilon}$

Schritt

Es gibt zwei Arten von Schritten: Schritte, in denen Nachrichten empfangen werden, und Schritte, in denen Nachrichten gesendet werden.

Ein Schritt, in dem der Prozess eine Nachricht empfängt, die zuvor vom -ten Prozess gesendet wurde , ist ein Paar der Form, wenn , mit . In ähnlicher Weise ist ein Paar, in dem eine Nachricht durch den -ten Prozess an den -ten Prozess gesendet wird, ein Paar der Form, wenn ${\ displaystyle j}$${\ displaystyle i}$${\ displaystyle \ left \ langle (s_ {1}, \ dots, s_ {j}, \ dots, s_ {n}), \ left ({\ begin {array} {lll} c_ {1,1} & \ Punkte & c_ {1, n} \\\ Punkte & \ Punkte & \ Punkte \\\ Punkte & m_ {i, j} c_ {i, j} & \ Punkte \\\ Punkte & \ Punkte & \ Punkte \\ 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 & \ dots \\\ dots & c_ { i, j} & \ dots \\\ dots & \ dots & \ dots \\ c_ {n, 1} & \ dots & 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 i}$${\ displaystyle j}$${\ displaystyle \ left \ langle (s_ {1}, \ dots, s_ {i}, \ dots, s_ {n}), \ left ({\ begin {array} {lll} c_ {1,1} & \ Punkte & c_ {1, n} \\\ Punkte & \ Punkte & \ Punkte \\\ Punkte & c_ {i, j} & \ Punkte \\\ Punkte & \ Punkte & \ Punkte \\ c_ {n, 1} & \ Punkte & 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 \\\ dots & m_ {i, j} c_ { i, j} & \ dots \\\ dots & \ dots & \ dots \\ c_ {n, 1} & \ dots & c_ {n, n} \ end {array}} \ right) \ right \ rangle}$${\ displaystyle {\ mathtt {succ}} _ {i} (s_ {i}, - m_ {i, j}) = s '_ {i}}$

Lauf

Ein Lauf ist eine Folge von globalen Zuständen, so dass ein Schritt einen Zustand mit dem nächsten verknüpft und der erste Zustand initial ist.

Es wird gesagt , dass ein globaler Zustand ist erreichbar , wenn es einen Lauf , das durch diesen Zustand existiert. ${\ displaystyle \ langle S, C \ rangle}$

Probleme

Mit der Einführung des Konzepts selbst wurde bewiesen, dass, wenn zwei Maschinen mit endlichem Zustand mit nur einem Nachrichtentyp kommunizieren, Begrenztheit, Deadlocks und nicht spezifizierter Empfangszustand entschieden und identifiziert werden können, während dies nicht der Fall ist, wenn die Maschinen mit zwei kommunizieren oder mehr Arten von Nachrichten. Später wurde weiter bewiesen, dass wir, wenn nur eine endliche Zustandsmaschine mit einem einzigen Nachrichtentyp kommuniziert, während die Kommunikation ihres Partners nicht eingeschränkt ist, immer noch Beschränkungen, Deadlocks und nicht spezifizierte Empfangszustände entscheiden und identifizieren können.

Es wurde ferner bewiesen, dass, wenn die Nachrichtenprioritätsbeziehung leer ist, Begrenzung, Deadlocks und nicht spezifizierter Empfangszustand selbst unter der Bedingung entschieden werden können, dass es zwei oder mehr Arten von Nachrichten in der Kommunikation zwischen endlichen Zustandsmaschinen gibt.

Begrenztheit, Deadlocks und nicht spezifizierter Empfangszustand sind alle in der Polynomzeit entscheidbar (was bedeutet, dass ein bestimmtes Problem in nachvollziehbarer, nicht unendlicher Zeit gelöst werden kann), da die diesbezüglichen Entscheidungsprobleme nicht deterministisch sind.

Erweiterungen

Einige berücksichtigte Erweiterungen sind:

• mit der Notation, dass einige Staaten möglicherweise keine Nachricht erhalten,
• Nachrichten werden in verschiedenen Reihenfolgen empfangen, wie z. B. FILO,
• Einige Nachrichten können verloren gehen.

Kanalsystem

Ein Kanalsystem ist im Wesentlichen eine Version einer kommunizierenden Finite-State-Maschine, bei der die Maschine nicht in einen bestimmten Prozess unterteilt ist. Somit gibt es einen einzelnen Zustandszustand und es gibt keine Einschränkung, welches System auf irgendeinem Kanal lesen / schreiben kann.

Formal ist bei einem gegebenen Protokoll das zugehörige Kanalsystem , wo sich die Menge von und von befindet . ${\ 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 \ Delta}$${\ 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})}$

Verweise