Simulering (datavetenskap)

Inom teoretisk datavetenskap är en simulering en relation mellan tillståndsövergångssystem som associerar system som beter sig på samma sätt i den meningen att det ena systemet simulerar det andra.

Intuitivt simulerar ett system ett annat system om det kan matcha alla dess drag.

Den grundläggande definitionen relaterar tillstånd inom ett övergångssystem, men detta är lätt att anpassa för att relatera två separata övergångssystem genom att bygga ett system som består av den disjunkta föreningen av motsvarande komponenter.

Formell definition

Givet ett märkt tillståndsövergångssystem ( $S$ , ${\displaystyle \Lambda } ,$ →), där $S$ är en uppsättning tillstånd, är $\Lambda$ en uppsättning etiketter och → är en uppsättning märkta övergångar (dvs. en delmängd av $S\times \Lambda \times S$ ), en relation $R\subseteq S\times S$ är en simulering om och endast om för varje par av tillstånd $(p,q)$ i $R$ och alla etiketter α i $\Lambda$ :

om ${\displaystyle p{\overset {\alpha }{\rightarrow }}p'} ,$ så finns det $q{\overset {\alpha }{\rightarrow }} q'$ så att $(p',q')\in R$

På motsvarande sätt, när det gäller relationssammansättning :

$R^{-1}\,;\,{\overset {\alpha }{\rightarrow }}\quad {\subseteq }\quad {\overset {\alpha }{\rightarrow }}\ ,;\,R^{-1}$

Givet två tillstånd $p$ och $q$ i $S$ , simulerar $p$$q$ , skrivet $p\,\leq \,q$ , om och endast om det finns en simulering $R$ så att $(p,q)\in R$ . Relationen $\leq$ kallas simuleringsförordningen och det är föreningen av alla simuleringar: $(p,q)\in \,\leq \,$ exakt när $(p,q)\in R$ för någon simulering $R$ .

Uppsättningen av simuleringar är stängd under union; därför är simuleringsförbeställningen i sig en simulering. Eftersom det är föreningen av alla simuleringar är det den unika största simuleringen. Simuleringar stängs också under reflexiv och transitiv stängning; därför måste den största simuleringen vara reflexiv och transitiv. Av detta följer att den största simuleringen - simuleringsförbeställningen - verkligen är en förbeställningsrelation . Observera att det kan finnas mer än en relation som är både en simulering och en förbeställning; termen simuleringsförbeställning syftar på den största av dem (som är en superset av alla andra).

Två tillstånd $p$ och $q$ sägs vara lika , skrivna $p\leq \geq q$ , om och endast om $p$ simulerar ${ \displaystyle q}$ och $q$ simulerar $p$ . Likhet är alltså den maximala symmetriska delmängden av simuleringsförordningen, vilket betyder att den är reflexiv, symmetrisk och transitiv; därav ett ekvivalensförhållande . Det är dock inte nödvändigtvis en simulering, och just i de fall då det inte är en simulering är den strikt grövre än bisimilaritet (vilket betyder att det är en superset av bisimilaritet). För att bevittna, överväg en likhet som är en simulering. Eftersom det är symmetriskt är det en bisimulering . Det måste då vara en delmängd av bisimilaritet, vilket är föreningen av alla bisimuleringar. Ändå är det lätt att se att likhet alltid är en superuppsättning av bisimilaritet. Av detta följer att om likhet är en simulering är den lika med bisimilaritet. Och om det är lika med bisimilaritet är det naturligtvis en simulering (eftersom bisimilaritet är en simulering). Därför är likhet en simulering om och endast om den är lika med bisimilaritet. Om det inte gör det måste det vara dess strikta superset; därav ett strikt grövre ekvivalensförhållande.

---

Likhet mellan separata övergångssystem

När man jämför två olika övergångssystem (S', Λ', →') och (S", Λ", →"), kan de grundläggande begreppen simulering och likhet användas genom att bilda den osammansättningen av de två maskinerna, (S , Λ, →) med S = S' ∐ S", Λ = Λ' ∪ Λ" och → = →' ∪ →", där ∐ är den disjunkta unionsoperatorn mellan mängder.

Se även

• Statligt övergångssystem
• Bisimulering
• Saminduktion
• Operationell semantik

1.   Park, David (1981). "Samtidighet och automatik på oändliga sekvenser" (PDF) . I Deussen, Peter (red.). Proceedings of the 5th GI-Conference, Karlsruhe . Föreläsningsanteckningar i datavetenskap . Vol. 104. Springer-Verlag . s. 167–183. doi : 10.1007/BFb0017309 . ISBN 978-3-540-10576-3 .
2. van Glabbeek, RJ (2001). "Den linjära tiden - förgrenande tidsspektrum I: semantiken för konkreta, sekventiella processer". Handbok i processalgebra . Elsevier. s. 3–99.