Kommunicerande maskin med ändligt tillstånd

Inom datavetenskap är en kommunicerande maskin med ändligt tillstånd en maskin med ändligt tillstånd märkt med "ta emot" och "sänd" operationer över något alfabet av kanaler. De introducerades av Brand och Zafiropulo och kan användas som en modell av samtidiga processer som Petri-nät . Kommunikerande finita tillståndsmaskiner används ofta för att modellera ett kommunikationsprotokoll eftersom de gör det möjligt att upptäcka större protokolldesignfel, inklusive begränsning, dödläge och ospecificerade mottagningar.

Fördelen med att kommunicera finita tillståndsmaskiner är att de gör det möjligt att bestämma många egenskaper i kommunikationsprotokoll, utöver nivån för att bara detektera sådana egenskaper. Denna fördel utesluter behovet av mänsklig hjälp eller begränsning i allmänhet.

Kommunikation av finita tillståndsmaskiner kan vara mer kraftfull än finita tillståndsmaskiner i situationer där utbredningsfördröjningen inte är försumbar (så att flera meddelanden kan vara på gång samtidigt) och i situationer där det är naturligt att beskriva protokollparterna och kommunikationsmediet som separata enheter.

Kommunicerande hierarkisk statsmaskin

Hierarkiska tillståndsmaskiner är ändliga tillståndsmaskiner vars tillstånd själva kan vara andra maskiner. Eftersom en kommunicerande finita tillståndsmaskin kännetecknas av samtidighet, är den mest anmärkningsvärda egenskapen i en kommunicerande hierarkisk tillståndsmaskin samexistensen av hierarki och samtidighet. Detta har ansetts vara mycket lämpligt eftersom det betyder starkare interaktion inuti maskinen.

Det bevisades dock att samexistensen av hierarki och samtidighet i sig kostar språkinkludering, språkekvivalens och all universalitet.

Definition

Protokoll

För ett godtyckligt positivt heltal $N$$\{(S_{i})_{i=1}^{N},\ (o_{i}) _{i=1}^{N},\ (M_{i,j})_{i,j=1}^{N},\ ({\mathtt {succ}})_{i=1}^ {N}\}$ ett protokoll med $N$ process(er) en fyrdubbel med:

• $(S_{i})_{i=1}^{N}$ , en sekvens av $N$ ändliga mängder. Varje uppsättning används för att representera en process, och varje element i $\displaystyle S_{i}}$ representerar ett möjligt tillstånd för den $i$ -e processen.
• $(o_{i})_{i=1}^{N}$ (med $o_{i}\in S_{i}$ ) , en sekvens som representerar det initiala tillståndet för varje process.
• ${\displaystyle (M_{i,j})_{i,j=1}^{N}} ,$ en ändlig sekvens av $N^{2 }$ disjunta ändliga mängder så att varje uppsättning $M_{i,j}$ representerar de möjliga meddelanden som kan skickas från process $i$ till process $j$ . Om $i=j$ så är $M_{i,j}$ tom.
• $({\mathtt {succ}} )_{i=1}^{N}:S_{i}\times \bigcup _{j=1}^{N}\left(M_{j,i}^{[+]}\cup M_{i ,j}^{[-]}\right)\mapsto S_{i}$ är en sekvens av övergångsfunktioner. Varje funktion modellerar övergången som kan tas genom att sända eller ta emot ett meddelande. Med avseende på process $i$ används symbolen ${\displaystyle [+]} för att notera ett meddelande som kan tas emot och$$[-]$ ett meddelande som kan skickas .

Global stat

Ett globalt tillstånd är ett par $\langle S,C\rangle$ där

• $S=(s_{1},...,s_{N})$ är en ordnad samling av tillstånd så att varje $s_{ i}$ representerar ett tillstånd för den $i$ -e processen.
• $C$ är en $N\x N$ matris så att varje $c_{i,j}\in C$ är en följd av $M_{i,j}$ .

Det initiala globala tillståndet är ett par $\langle O,\mathrm {E} \rangle$ där

• $O=(o_{1},...,o_{N})$
• $\mathrm {E}$ definieras som en $N\ gånger N$ matris så att för alla ${\displaystyle i,j\in \{1,...,N\}} ,$ E $\displaystyle E_{i,j}}$ är lika med det tomma ordet, $\epsilon$ .

Steg

Det finns två typer av steg, steg i vilka meddelanden tas emot och steg i vilka meddelanden skickas.

Ett steg där $j$ -processen tar emot ett meddelande som tidigare skickats av i $\displaystyle i}$ -th processen är ett par av formen $\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({\ börja{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$ när ${\displaystyle {\mathtt {succ}}_{i}(s_{j},+m_{i,j})=s'_{j}} ,$ med $m'_{i,j}\in M_{i,j}$ . På liknande sätt $\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 \\\dots &m_{i,j}c_{i,j}&\dots \ \\dots &\dots &\dots \\c_{n,1}&\dots &c_{n,n}\end{array}}\right)\right\rangle$ ett par där ett meddelande skickas av i $\displaystyle i}$ -th processen till $j$ -th one ett par av formen när ${\mathtt {succ}}_{i}(s_{i},-m_{i,j})=s'_{i}$

Springa

En körning är en sekvens av globala tillstånd så att ett steg relaterar ett tillstånd till nästa, och så att det första tillståndet är initialt.

Det sägs att ett globalt tillstånd $\langle S,C\rangle$ kan nås om det finns en körning som passerar genom detta tillstånd.

Problem

Det har bevisats med introduktionen av själva konceptet att när två finita tillståndsmaskiner kommunicerar med endast en typ av meddelanden, kan begränsning, dödläge och ospecificerat mottagningstillstånd bestämmas och identifieras medan så inte är fallet när maskinerna kommunicerar med två eller fler typer av meddelanden. Senare har det ytterligare bevisats att när endast en ändlig tillståndsmaskin kommunicerar med en enda typ av meddelande medan kommunikationen från dess partner är obegränsad, kan vi fortfarande bestämma och identifiera begränsningar, dödlägen och ospecificerat mottagningstillstånd.

Det har vidare bevisats att när meddelandeprioritetsrelationen är tom, kan begränsning, dödläge och ospecificerat mottagningstillstånd bestämmas även under det tillstånd där det finns två eller flera typer av meddelanden i kommunikationen mellan finita tillståndsmaskiner.

Boundedness, dödlägen och ospecificerat mottagningstillstånd är alla avgörbara i polynomtid (vilket innebär att ett visst problem kan lösas inom lösbar, inte oändlig, tid) eftersom beslutsproblemen angående dem är odeterministiska logspace kompletta.

Tillägg

Några tillägg som övervägs är:

• ha en notering som anger att vissa stater kanske inte tar emot något meddelande,
• meddelanden tas emot i olika ordningsföljder, såsom FILO,
• vissa meddelanden kan försvinna,

Kanalsystem

Huvudartikel: Kanalsystem (datavetenskap)

Ett kanalsystem är i huvudsak en version av en kommunicerande maskin med ändligt tillstånd där maskinen inte är uppdelad i distinkt process. Således finns det ett enda tillstånd och det finns ingen begränsning för vilket system som kan läsa/skriva på vilken kanal som helst.

$\langle (S_{i})_{i=1}^{n},(o_{i})_{i=1}^{n},(M_{i,j})_{i,j=1} ^{n},({\mathtt {succ}})_{i}\rangle$ ett protokoll ${\displaystyle \langle \prod (S_{i})_{i=1}^{n},(o_{i})_{i=1}^ {n},\bigcup _{i,j=1}^{n}(M_{i,j}),\Delta \rangle } , där Δ {\displaystyle \Delta$ dess associerade kanalsystem är } $mängden$ av $((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})$ och av $((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 })$ .