Kanalsystem (datavetenskap)

Inom datavetenskap är ett kanalsystem en finita-tillståndsmaskin som liknar kommunicerande finite-state-maskin där det finns ett enda system som kommunicerar med sig själv istället för att många system kommunicerar med varandra. Ett kanalsystem liknar en pushdown-automat där en kö används istället för en stack. Dessa köer kallas kanaler . Intuitivt representerar varje kanal en sekvens ett meddelande som ska skickas och läsas i den ordning som de skickas.

Definition

Kanalsystem

definieras ett kanalsystem (eller perfekt kanalsystem ) ${\displaystyle S} som en tupel$ $\langle Q,C,\Sigma ,\Delta \rangle$ med:

$Q=\{q_{1},\dots ,q_{m}\}$ en ändlig uppsättning kontrolltillstånd ,
$q_{0}\in Q$ ett initialt tillstånd ,
$A$ ett ändligt alfabet (för enkelhetens skull, låt $\epsilon \in A$ ),
$C=\{c_{1},\dots ,c_{n}\}$ en ändlig uppsättning kanaler ,
$\Sigma =\{a_{1},\dots ,a_{p}\}$ ett ändligt alfabet av meddelanden ,
${\displaystyle \Delta \subseteq Q\times C\times \{?,!\}\times \Sigma ^{*}\times A\times Q} en ändlig uppsättning övergångsregler$ med $\Sigma ^{*}$ är uppsättningen av ändliga (potentiellt tomma) ord över alfabetet $\Sigma$ .

Beroende på författaren kan ett kanalsystem inte ha något initialtillstånd och kan ha ett tomt alfabet.

Konfiguration

En konfiguration eller globalt tillstånd för kanalsystemet är en $n+1$ tuppel som tillhör $Q\times \prod _{i=1}^ {n}(\Sigma ^{*})$ . Intuitivt representerar en konfiguration $\gamma =(q,w_{1},\dots ,w_{m})$ att en körning är i tillståndet ${\ displaystyle q}$ och att dess $i$ -e kanal innehåller ordet $w_{i}$ .

Den initiala konfigurationen är $(q_{0},\epsilon ,\dots ,\epsilon )$ , med $\epsilon$ det tomma ordet.

Steg

Intuitivt betyder en övergång $(q,c_{i},!,u,a,q')$ att systemet kan gå till kontrolltillstånd $q$ till $q'$ genom att skriva ett $u$ i slutet av kanalen $c_{i}$ . På liknande sätt $(q,c_{i},?,u,a,q')$ att systemet kan gå till kontrolltillstånd $q$ till $q'$ genom att ta bort a $u$ som börjar med ordet $c_{i}$ .

Formellt, givet en konfiguration $(q,w_{1},\dots ,w_{m})$ och en övergång ${\displaystyle (q,c_{i},!,u,q')} ,$ det finns ett perfekt steg ${\displaystyle (q,w_{1},\ prickar ,w_{i-1},w_{i},w_{i+1},\dots ,w_{m}){\xrightarrow {a}}_{\mathtt {perf}}(q',w_{ 1},\dots ,w_{i-1},w_{i}u,w_{i+1},\dots ,w_{m})} , där steget lägger till en bokstav u {\$ displaystyle $}$ till slutet av det $i$ -te ordet. På liknande sätt, givet en övergång $(q,c_{i},?,u,q')$ , finns det ett perfekt steg ${\displaystyle (q,w_{1},\dots ,w_{i-1},uw_{i},w_{i+1},w_{m}){\xrightarrow {a}}_{\mathtt {perf}}(q',w_{1},\dots ,w_{i-1},w_{i},w_{i+1},\dots ,w_{m})} där den första bokstaven$ i $i$ -te ordet är $u$ och har tagits bort under steget.

Springa

En perfekt körning är en sekvens av perfekta steg, av formen $\gamma _{0}{\xrightarrow {a_{0}}}_{\mathtt {perf}} \gamma _{1}\dots$ . Vi låter $\gamma {\xrightarrow[{\mathtt {perf}}]{*}}\gamma '$ beteckna att det finns en perfekt körning som börjar vid $\ gamma$ och slutar på $\gamma '$ .

språk

Givet ett perfekt eller ett förlustkanalsystem $S$ kan flera språk definieras.

Ett ord över $A^{*}$ accepteras av $S$ om det är sammanlänkningen av etiketterna för en körning av $S$ . Språket som definieras av $S$ är den uppsättning ord som accepteras av $S$ .

Uppsättningen av nåbar konfiguration av $S$ , betecknad $R(S)$ definieras som uppsättningen av konfiguration $\gamma$ som kan nås från initialtillståndet. Dvs som uppsättningen av konfigurationer $\gamma '$ så att $(q_{0},\epsilon ,\dots ,\epsilon ){\ xrightarrow {*}}\gamma '$ .

Givet en kanal $c$ , är kanalen för $c$ uppsättningen av tupler $(w_{1},\dots w_{m})$ såsom att $(c,w_{1},\dots ,w_{m})\in R(S)$ .

Kanalsystem och Turingmaskin

De flesta problem relaterade till perfekt kanalsystem är oavgjorda. Detta beror på det faktum att en sådan maskin kan simulera körningen av en Turing-maskin . Denna simulering är nu skissad.

Givet en Turing-maskin $M$ finns det ett perfekt kanalsystem $S$ så att varje körning av $M$ av längden $n$ kan simuleras med en körning av $S$ av längden $O(n^{2})$ . Intuitivt består denna simulering helt enkelt av att ha hela bandet från den simulerade Turing-maskinen i en kanal. Innehållskanalen läses sedan i sin helhet och skrivs omedelbart om i kanalen, med ett undantag ändras den del av innehållet som representerar Turing-maskinens huvud, för att simulera ett steg i Turing-maskinens beräkning.

Varianter

Flera varianter av kanalsystem har introducerats. De två varianterna som introduceras nedan tillåter inte att simulera en Turing-maskin och gör att flera problem av intresse kan avgöras.

Enkanalsmaskin

En enkanalsmaskin är ett kanalsystem som använder en enda kanal. Samma definition gäller även för alla varianter av kanalsystem.

Räknarmaskin

När alfabetet i ett kanalsystem innehåller ett enda meddelande, är varje kanal i huvudsak en räknare. Av detta följer att dessa system i huvudsak är Minsky - maskiner . Vi kallar sådana system för räknarmaskiner . Samma definition gäller för alla varianter av kanalsystem.

Fullständigt specificerat protokoll

Ett fullständigt specificerat protokoll (CSP) definieras exakt som ett kanalsystem. Men begreppen steg och körning definieras olika.

En CSP tillåter två typer av steg. Perfekta steg, enligt definitionen ovan, och ett övergångssteg för meddelandeförlust . Vi betecknar en meddelandeförlustövergång steg med $(q,w_ {1},\dots ,a\cdot w_{i},\dots ,w_{m})\rightsquigarrow (q,w_{1},\dots ,w_{i},\dots ,w_{m})$ .

Löshet

Ett förlustkanalsystem eller maskin som kan göra förlustfel är en förlängning av ett fullständigt specificerat protokoll där bokstäver kan försvinna var som helst.

Ett förlustkanalsystem tillåter två typer av steg. Perfekta steg, enligt definitionen ovan, och förluststeg. Vi betecknar ett förluststeg, ${\ displaystyle (q,w_{1},\dots ,w_{i}\cdot a\cdot w'_{i}\dots ,,w_{m})\rightsquigarrow (q,w_{1},\dots ,w_ {i}\cdot w'_{i},w'_{m})}$ .

En körning där kanal töms så snart meddelanden skickas in i dem är en giltig körning enligt denna definition. Av denna anledning kan vissa skälighetsvillkor införas för dessa system.

Kanalens rättvisa

Givet ett meddelande en kanal $c$ sägs en körning vara kanal rättvis med avseende på $c$ om, förutsatt att det finns oändligt många steg i vilka ett brev skickas till $c$ då finns det oändligt många steg där en bokstav läses från $c$ .

En beräkning sägs vara rättvis kanal om den är rättvis kanal med avseende på varje kanal $c$ .

Opartiskhet

Opartiskhetsvillkoret är en begränsning av kanalens rättvisa villkor där både kanalen och brevet beaktas.

Givet ett meddelande $m$ och en kanal $c$ sägs en körning vara opartisk med avseende på $c$ och $m$ om, förutsatt att det finns oändligt många steg där $m$ skickas till $c$ så finns det oändligt många steg där $m$ läses från $c$ .

En beräkning sägs vara opartisk med avseende på en kanal $c$ om den är opartisk med avseende på $c$ och meddelanden $m$ . Det sägs vara opartiskt om det är opartiskt med avseende på alla kanaler $c$ .

Budskapens rättvisa

Message fairness-egenskapen liknar opartiskhet, men villkoret måste bara gälla om det finns ett oändligt antal steg där $m$ kan läsas. Formellt sägs en körning vara meddelande rättvist med avseende på $c$ och $m$ om, förutsatt att det finns oändligt många steg i vilka $m$ skickas till $c$ , och oändligt många steg $i$ som inträffar i ett tillstånd $q$ så att det finns en övergång $(q,m,q')$ , då finns det oändligt många steg där $m$ läses från $c$ .

Begränsadhet

Körningen sägs ha begränsad förlust om antalet bokstav som tas bort mellan två perfekta steg är begränsat.

Införande av fel

En maskin som kan infoga fel är en förlängning av kanalsystem där bokstäver kan förekomma var som helst.

En maskin som kan infoga fel tillåter två typer av steg. Perfekta steg, enligt definitionen ovan, och insättningssteg. Vi betecknar en infogning steg med ${\ displaystyle (q,w_{1},\dots ,w_{i}\cdot w'_{i}\dots ,,w_{m})\rightsquigarrow (q,w_{1},\dots ,w_{i} \cdot a\cdot w'_{i},w'_{m})}$ .

Dupliceringsfel

En maskin som kan duplicera fel är en förlängning av maskin som kan infoga fel där den infogade bokstaven är en kopia av den föregående bokstaven.

En maskin som kan infoga fel tillåter två typer av steg. Perfekta steg, enligt definitionen ovan, och dupliceringssteg. Vi betecknar en infogning steg med $(q,w_{1},\dots ,w_{i}\cdot a\cdot w'_{i}\dots ,,w_{m})\rightsquigarrow (q,w_{1}, \dots ,w_{i}\cdot a\cdot a\cdot w'_{i},w'_{m})$ .

En icke-duplicerad maskin som kan duplicera fel är en maskin som säkerställer att bokstäverna i varje kanal växlar mellan en speciell ny bokstav # och en vanlig bokstav från meddelandets alfabet. Om det inte är fallet betyder det att en duplicering inträffade och körningen avvisas. Denna process gör det möjligt att koda vilket kanalsystem som helst till en maskin som kan duplicera fel, samtidigt som den tvingar den att inte ha fel. Eftersom kanalsystem kan simulera maskiner, följer det att maskiner som kan duplicera fel kan simulera Turing-maskin.

Egenskaper

Uppsättningen av konfigurationer som kan nås är igenkännbara för maskiner med förlust av kanaler och maskiner som kan infoga fel. Den är rekursivt uppräknad för maskin som kan duplicera fel.

Problem och deras komplexitet

Det här avsnittet innehåller en lista över problem över kanalsystem och deras bestämbarhet av komplexitet över varianter av sådana system.

Uppsägningsproblem

Avslutningsproblemet består i att bestämma, givet ett kanalsystem $S$ och en initial konfiguration $\gamma$ om alla körningar av $S$ som börjar vid $\gamma$ är ändliga. Detta problem kan inte avgöras över perfekta kanalsystem, även när systemet är en motmaskin eller när det är en enkanalsmaskin.

Detta problem är avgörbart men icke primitivt rekursivt över förlustkanalsystem. Detta problem är trivialt avgörbart över maskin som kan infoga fel.

Nåbarhetsproblem

Nåbarhetsproblemet består i att bestämma, givet ett kanalsystem $S$ och två initiala konfigurationer $\gamma$ och $\gamma '$ om det finns en körning av $S$ från $\gamma$ till $\gamma '$ . Detta problem är oavgörbart över perfekta kanalsystem och avgörbart men icke primitivt rekursivt över förlustkanalsystem. Detta problem kan avgöras över maskin som kan infoga fel.

Nåbarhetsproblem

Deadlock -problemet består i att bestämma om det finns en nåbar konfiguration utan efterföljare. Detta problem kan avgöras över förlustkanalsystem och trivialt avgörbart över maskin som kan infoga fel. Det är också avgörbart över disk maskin.

Problem med modellkontroll

Modellkontrollproblemet består i att avgöra om det ges ett system $S$ och en CTL* * -formel eller en LTL -formel $\phi$ eller om språket som definieras av $S$ uppfyller $\phi$ . Detta problem är oavgörbart över förlustkanalsystem.

Återkommande tillståndsproblem

Det återkommande tillståndsproblemet består i att bestämma, givet ett kanalsystem $S$ och en initial konfiguration $\gamma$ och ett tillstånd $s$ om det finns en körning av $S$ , börjar vid $\gamma$ , går oändligt ofta genom tillstånd $s$ . Detta problem kan inte avgöras över förlustkanalsystem, även med en enda kanal.

Motsvarande finita tillståndsmaskin

Givet ett system $S$ finns det ingen algoritm som beräknar en finit tillståndsmaskin som representerar $R(S)$ för klassen av förlustkanalsystem. Detta problem kan avgöras över maskin som kan infoga fel.

Begränsningsproblem

Begränsningsproblemet består i att bestämma om uppsättningen av nåbara konfigurationer är ändlig . Dvs längden på innehållet i varje kanal är begränsad. Detta problem är trivialt avgörbart över maskin som kan infoga fel. Det är också avgörbart över disk maskin.

Så småningom fastigheter

Eventualitetsegenskapen , eller ofrånkomlighetsegenskapsproblemet består i att bestämma, givet ett kanalsystem $S$ och en uppsättning $\Gamma$ av konfigurationer om alla körs av $S$ med början på $\gamma$ går igenom en konfiguration av $\Gamma$ . Detta problem är oavgörligt för förlustkanalsystem med opartiskhet och med de två andra rättvisa begränsningarna.

Säkerhetsegenskap

Säkerhetsegenskapsproblemet består i att, givet ett kanalsystem $S$ och en vanlig uppsättning $\displaystyle R},$ { avgöra om

Strukturell avslutning

Det strukturella avslutningsproblemet består i att, givet ett kanalsystem ${\displaystyle S}, avgöra$ om termineringsproblemet gäller för $S$ för varje initial konfiguration. Detta problem kan inte avgöras även över diskmaskin.

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 hade 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.

^ ^a ^b Abdulla, Parosh Aziz; Jonsson, Bengt (1996). "Verifiera program med opålitliga kanaler" . Information och beräkning . 127 (2): 91–101. doi : 10.1006/inco.1996.0053 .
^ ^a ^b ^c ^d Schnoebelen, Ph (15 september 2002). "Att verifiera förlustkanalsystem har icke-primitiv rekursiv komplexitet". Informationsbehandlingsbrev . 83 (5): 251–261. doi : 10.1016/S0020-0190(01)00337-4 .
^ ^a ^b ^c ^d ^e ^f ^g ^h ⁱ ^j ^k ^l ^m ⁿ ^o Cécé, Gérard; Finkel, Alain (10 januari 1996). "Otillförlitliga kanaler är lättare att verifiera än perfekta kanaler" . Information och beräkning . 124 (1): 20–31. doi : 10.1006/inco.1996.0003 .
^ ^a ^b ^c ^d Mayr, Richard (17 mars 2008). "Oavgörliga problem i opålitliga beräkningar" . Teoretisk datavetenskap . 297 (1–3): 337–354. doi : 10.1016/S0304-3975(02)00646-1 .
^ ^a ^b ^c ^d ^e ^f ^g Abdulla, Parosh Aziz; Jonsson, Bengt (10 oktober 1996). "Oavgörliga verifieringsproblem för program med opålitliga kanaler" . Information och beräkning . 130 (1): 71–90. doi : 10.1006/inco.1996.0083 .
^ ^a ^b Rosier, Louis E.; Gouda, Mohamed G (1983). Bestämma framsteg för en klass av kommunicerande finita tillståndsmaskiner (Rapport).
^ Alur, Rajeev; Kannan, Sampath; Yannakakis, Mihalis. "Kommunicera hierarkiska tillståndsmaskiner," Automater, Språk och Programmering. Prag: ICALP, 1999

[decidable-1] Abdulla, Parosh Aziz; Jonsson, Bengt (1996). "Verifiera program med opålitliga kanaler" . Information och beräkning . 127 (2): 91–101. doi : 10.1006/inco.1996.0053 .

[Nonprimitive_recursive-2] Schnoebelen, Ph (15 september 2002). "Att verifiera förlustkanalsystem har icke-primitiv rekursiv komplexitet". Informationsbehandlingsbrev . 83 (5): 251–261. doi : 10.1016/S0020-0190(01)00337-4 .

[easier-3] ^ ^a ^b ^c ^d ^e ^f ^g ^h ⁱ ^j ^k ^l ^m ⁿ ^o Cécé, Gérard; Finkel, Alain (10 januari 1996). "Otillförlitliga kanaler är lättare att verifiera än perfekta kanaler" . Information och beräkning . 124 (1): 20–31. doi : 10.1006/inco.1996.0003 .

[Counter-4] Mayr, Richard (17 mars 2008). "Oavgörliga problem i opålitliga beräkningar" . Teoretisk datavetenskap . 297 (1–3): 337–354. doi : 10.1016/S0304-3975(02)00646-1 .

[Undecidable_over_unreliable_channels-5] ^ ^a ^b ^c ^d ^e ^f ^g Abdulla, Parosh Aziz; Jonsson, Bengt (10 oktober 1996). "Oavgörliga verifieringsproblem för program med opålitliga kanaler" . Information och beräkning . 130 (1): 71–90. doi : 10.1006/inco.1996.0083 .

[Rosier,_Gouda-6] Rosier, Louis E.; Gouda, Mohamed G (1983). Bestämma framsteg för en klass av kommunicerande finita tillståndsmaskiner (Rapport).

[7] Alur, Rajeev; Kannan, Sampath; Yannakakis, Mihalis. "Kommunicera hierarkiska tillståndsmaskiner," Automater, Språk och Programmering. Prag: ICALP, 1999