Övergångssystem

Inom teoretisk datavetenskap är ett övergångssystem ett begrepp som används i studiet av beräkningar . Det används för att beskriva det potentiella beteendet hos diskreta system . Den består av tillstånd och övergångar mellan tillstånd, som kan märkas med etiketter valda från en uppsättning; samma etikett kan förekomma på mer än en övergång. Om etikettuppsättningen är en singleton är systemet i huvudsak omärkt, och en enklare definition som utelämnar etiketterna är möjlig.

Övergångssystem sammanfaller matematiskt med abstrakta omskrivningssystem (som förklaras vidare i den här artikeln) och riktade grafer . De skiljer sig från finita-tillståndsautomater på flera sätt:

Uppsättningen av tillstånd är inte nödvändigtvis ändlig, eller ens räknebar.
Uppsättningen av övergångar är inte nödvändigtvis ändlig eller ens räknebar.
Inga "start"-tillstånd eller "slutliga" tillstånd ges.

Övergångssystem kan representeras som riktade grafer.

Formell definition

Formellt är ett övergångssystem ett par $(S,\rightarrow )$ där $S$ är en uppsättning tillstånd och $\rightarrow$ är en relation mellan tillståndsövergångar ( dvs en delmängd av $S\times S$ ). En övergång från tillstånd $p$ till tillstånd $q$ (dvs $(p,q)\in \rightarrow$ ) skrivs som ${\ displaystyle p\rightarrow q}$ .

Ett märkt övergångssystem är en tupel $(S,\Lambda ,\rightarrow )$ där $S$ är en uppsättning tillstånd, $\Lambda$ är en uppsättning av etiketter, och $\rightarrow$ är en relation av märkta övergångar (dvs en delmängd av ${\displaystyle S\times \Lambda \times S} )$ . $(p,\alpha ,q)\i \högerpil$ skrivs som

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

och representerar en övergång från tillstånd $p$ till tillstånd $q$ med etiketten $\alpha$ . Etiketter kan representera olika saker beroende på språket av intresse. Typiska användningar av etiketter inkluderar att representera förväntad input, villkor som måste vara sanna för att utlösa övergången eller åtgärder som utförs under övergången. Märkta övergångssystem introducerades ursprungligen som namngivna övergångssystem.

Speciella fall

Om, för någon given $p$ och $\alpha$ , det bara finns en enda tupel $(p,\alpha ,q)$ i $\rightarrow$ , då säger man att $\alpha$ är deterministisk (för ${\displaystyle p} )$ .
Om, för någon given $p$ och $\alpha$ , det finns minst en tupel $(p,\alpha ,q)$ i $\rightarrow$ , då säger man att $\alpha$ är körbar (för ${\displaystyle p} )$ .

Kategoriteoretisk formalisering

Den formella definitionen kan omformuleras i termer av kategoriteori. Varje märkt tillståndsövergångssystem $(S,\Lambda ,\rightarrow )$ är bijektivt en funktion $\xi _{\rightarrow }$ från $S$ till kraftmängden för $S$ indexerad av $\Lambda$ skriven som ${\displaystyle {\mathcal {P}}(\Lambda \times S)} ,$ definierad av

p\mapsto \{(\alpha ,q)\in \Lambda \times S:p{\overset {\alpha }{\ högerpil }}q\}

.

Därför är ett märkt tillståndsövergångssystem en F-koalgebra för funktorn $P(\Lambda \times \rightarrow )$ .

Samband mellan märkt och omärkt övergångssystem

Det finns många samband mellan dessa begrepp. Vissa är enkla, som att observera att ett märkt övergångssystem där uppsättningen etiketter består av endast ett element är ekvivalent med ett omärkt övergångssystem. Men alla dessa relationer är inte lika triviala.

Jämförelse med abstrakta omskrivningssystem

Som ett matematiskt objekt är ett omärkt övergångssystem identiskt med ett (oindexerat) abstrakt omskrivningssystem . Om vi betraktar omskrivningsrelationen som en indexerad uppsättning relationer, som vissa författare gör, så är ett märkt övergångssystem likvärdigt med ett abstrakt omskrivningssystem där indexen är etiketterna. Studiens inriktning och terminologin är dock olika. I ett övergångssystem är man intresserad av att tolka etiketterna som handlingar, medan man i ett abstrakt omskrivningssystem fokuserar på hur objekt kan omvandlas (skrivas om) till andra.

Tillägg

I modellkontroll definieras ibland ett övergångssystem för att även inkludera en extra märkningsfunktion för staterna, vilket resulterar i en föreställning som omfattar den Kripke-struktur .

Handlingsspråk är förlängningar av övergångssystem, som lägger till en uppsättning flytande F , en uppsättning värden V och en funktion som mappar F × S till V .

Se även