ในวิทยาการคอมพิวเตอร์เชิงทฤษฎีบิซิมูเลชัน (bisimulation)คือความสัมพันธ์แบบไบนารีระหว่างระบบการเปลี่ยน สถานะ โดยเชื่อมโยงระบบที่มีพฤติกรรมเหมือนกัน กล่าวคือ ระบบหนึ่งจำลองอีกระบบหนึ่ง และในทางกลับกัน

โดยทั่วไปแล้ว ระบบสองระบบจะมีความคล้ายคลึงกันแบบทวิภาวะ (bisimilar) หากสมมติว่าเรามองว่าระบบทั้งสองกำลังเล่นเกมตามกฎบางอย่าง ระบบทั้งสองจะมีท่าทีที่ตรงกัน ในแง่นี้ ผู้สังเกตการณ์จะไม่สามารถแยกแยะระบบแต่ละระบบออกจากกันได้

เมื่อกำหนดระบบการเปลี่ยนสถานะที่มีป้ายกำกับ( S , Λ, →)โดยที่Sคือเซตของสถานะ Λ คือเซตของป้ายกำกับ และ → คือเซตของการเปลี่ยนสถานะที่มีป้ายกำกับ (กล่าวคือ เซตย่อยของ Λ ) การจำลอง แบบคู่ (bisimulation) คือความสัมพันธ์แบบไบนารีโดยที่ทั้งRและส่วนกลับ ของ R เป็นการจำลองจากนี้จึงสรุปได้ว่า การปิด แบบสมมาตรของการจำลองแบบคู่เป็นการจำลองแบบคู่ และการจำลองแบบสมมาตรแต่ละครั้งเป็นการจำลองแบบคู่ ดังนั้นผู้เขียนบางคนจึงกำหนดการจำลองแบบคู่เป็นการจำลองแบบสมมาตร^{[ 1 ]}${\displaystyle \Lambda }$${\displaystyle S\times \Lambda \times S}$${\displaystyle R\subseteq S\times S}$${\displaystyle R^{T}}$

กล่าวอีกนัยหนึ่งRเป็นบิซิมูเลชันก็ต่อเมื่อสำหรับทุกคู่สถานะในRและป้ายกำกับλ ทั้งหมด ใน: ${\displaystyle (p,q)}$${\displaystyle \Lambda }$

• ถ้าเช่นนั้นจะมีอยู่จริงที่ ทำให้ ;${\displaystyle p\mathrel {\overset {\lambda }{\rightarrow }} p'}$${\displaystyle q\mathrel {\overset {\lambda }{\rightarrow }} q'}$${\displaystyle (p',q')\in R}$
• ถ้าเช่นนั้นจะมีอยู่จริงที่ทำให้${\displaystyle q\mathrel {\overset {\lambda }{\rightarrow }} q'}$${\displaystyle p\mathrel {\overset {\lambda }{\rightarrow }} p'}$${\displaystyle (p',q')\in R}$

กำหนดให้ pและqเป็นสถานะคู่ขนานกับqเขียนแทนด้วย ก็ต่อเมื่อมีคู่ขนานRที่ทำให้ ซึ่งหมายความว่าความสัมพันธ์ของคู่ขนาน∼ คือการรวมกันของคู่ขนานทั้งหมดกล่าวคือ เมื่อสำหรับคู่ขนานR บางตัว${\displaystyle p\,\sim \,q}$${\displaystyle (p,q)\in R}$${\displaystyle (p,q)\in \,\sim \,}$${\displaystyle (p,q)\in R}$

เซตของการจำลองแบบคู่ปิดภายใต้การรวมกัน^{[หมายเหตุ 1 ]}ดังนั้น ความสัมพันธ์ความคล้ายคลึงแบบคู่จึงเป็นการจำลองแบบคู่ด้วยตัวมันเอง เนื่องจากเป็นผลรวมของการจำลองแบบคู่ทั้งหมด จึงเป็นการจำลองแบบคู่ที่ใหญ่ที่สุดเพียงหนึ่งเดียว การจำลองแบบคู่ยังปิดภายใต้การปิดแบบสะท้อน สมมาตร และถ่ายทอด ดังนั้น การจำลองแบบคู่ที่ใหญ่ที่สุดจะต้องสะท้อน สมมาตร และถ่ายทอด จากนี้จึงสรุปได้ว่าการจำลองแบบคู่ที่ใหญ่ที่สุด—ความคล้ายคลึงแบบคู่ — เป็นความสัมพันธ์สมมูล^{[ 2 ]}

การจำลองแบบคู่ (Bisimulation) สามารถนิยามได้ในแง่ของการประกอบความสัมพันธ์ดังต่อไปนี้

เมื่อกำหนดระบบการเปลี่ยนสถานะที่มีป้ายกำกับแล้ว ความสัมพันธ์แบบบิซิมูเลชันคือความสัมพันธ์ทวิภาคRบนS (กล่าวคือR ⊆ S × S ) โดยที่${\displaystyle (S,\Lambda ,\rightarrow )}$${\displaystyle \forall \lambda \in \Lambda }$

$${\displaystyle R\ ;\ {\overset {\lambda }{\rightarrow }}\quad {\subseteq }\quad {\overset {\lambda }{\rightarrow }}\ ;\ R}$$ และ $${\displaystyle R^{-1}\ ;\ {\overset {\lambda }{\rightarrow }}\quad {\subseteq }\quad {\overset {\lambda }{\rightarrow }}\ ;\ R^{-1}}$$

จากความเป็นเอกภาคและความต่อเนื่องของการประกอบความสัมพันธ์ ทำให้สรุปได้ทันทีว่าเซตของการจำลองแบบคู่ปิดภายใต้การรวม ( การเชื่อมต่อในเซตลำดับของความสัมพันธ์) และการคำนวณทางพีชคณิตอย่างง่ายแสดงให้เห็นว่าความสัมพันธ์ของความคล้ายคลึงแบบคู่—การเชื่อมต่อของการจำลองแบบคู่ทั้งหมด—เป็นความสัมพันธ์สมมูล คำจำกัดความนี้และการจัดการความคล้ายคลึงแบบคู่ที่เกี่ยวข้อง สามารถตีความได้ในควอนทาล ผกผันใดๆ ก็ได้

ความคล้ายคลึงแบบทวิภาค (Bisimilarity) สามารถนิยามได้ในเชิงทฤษฎีลำดับโดยใช้ทฤษฎีจุดตรึง (Fixpoint Theory ) กล่าวคือ จุดตรึงที่ใหญ่ที่สุดของฟังก์ชันบางอย่างที่กำหนดไว้ด้านล่าง

กำหนดระบบการเปลี่ยนสถานะที่มีป้ายกำกับ ( , Λ, →) ให้เป็นฟังก์ชันจากความสัมพันธ์ทวิภาคบน ไปยังความสัมพันธ์ทวิภาคบนดังต่อไปนี้: ${\displaystyle S}$${\displaystyle F:{\mathcal {P}}(S\times S)\to {\mathcal {P}}(S\times S)}$${\displaystyle S}$${\displaystyle S}$

ให้เป็นความสัมพันธ์ทวิภาคใดๆ บนโดยกำหนดให้ เป็นเซตของคู่ทั้งหมดใน× ที่มีคุณสมบัติดังนี้: ${\displaystyle R}$${\displaystyle S}$${\displaystyle F(R)}$${\displaystyle (p,q)}$${\displaystyle S}$${\displaystyle S}$

$${\displaystyle \forall \lambda \in \Lambda .\,\forall p'\in S.\,p{\overset {\lambda }{\rightarrow }}p'\,\Rightarrow \,\exists q'\in S.\,q{\overset {\lambda }{\rightarrow }}q'\,{\textrm {and}}\,(p',q')\in R}$$ และ $${\displaystyle \forall \lambda \in \Lambda .\,\forall q'\in S.\,q{\overset {\lambda }{\rightarrow }}q'\,\Rightarrow \,\exists p'\in S.\,p{\overset {\lambda }{\rightarrow }}p'\,{\textrm {and}}\,(p',q')\in R}$$

ความคล้ายคลึงแบบทวิภาค (Bisimilarity ) ถูกกำหนดให้เป็นจุดคงที่ที่ใหญ่ที่สุดของ${\displaystyle F}$

การจำลองแบบสองมิติยังสามารถคิดได้ในแง่ของเกมระหว่างผู้เล่นสองคน: ผู้โจมตีและผู้ป้องกัน^{[ 3 ]}

"ผู้โจมตี" จะเป็นฝ่ายเริ่มก่อนและสามารถเลือกการเปลี่ยนสถานะที่ถูกต้องใดๆ ก็ได้จากนั่นคือ หรือ ${\displaystyle \lambda }$${\displaystyle (p,q)}$$${\displaystyle (p,q){\overset {\lambda }{\rightarrow }}(p',q)}$$$${\displaystyle (p,q){\overset {\lambda }{\rightarrow }}(p,q')}$$

จากนั้น "ฝ่ายป้องกัน" จะต้องพยายามจับคู่การเปลี่ยนแปลงนั้นไม่ว่าจะจากหรือขึ้นอยู่กับการเคลื่อนไหวของฝ่ายโจมตี กล่าวคือ พวกเขาต้องหา ที่ทำให้: หรือ ${\displaystyle \lambda }$${\displaystyle (p',q)}$${\displaystyle (p,q')}$${\displaystyle \lambda }$$${\displaystyle (p',q){\overset {\lambda }{\rightarrow }}(p',q')}$$$${\displaystyle (p,q'){\overset {\lambda }{\rightarrow }}(p',q')}$$

ผู้โจมตีและผู้ป้องกันจะผลัดกันเล่นไปเรื่อยๆ จนกระทั่ง:

• ฝ่ายป้องกันไม่สามารถหาการเปลี่ยนผ่านที่เหมาะสมเพื่อรับมือกับการเคลื่อนไหวของฝ่ายโจมตีได้ ในกรณีนี้ ฝ่ายโจมตีเป็นฝ่ายชนะ
• เกมจะเข้าสู่สถานะที่ "ตาย" ทั้งคู่ (กล่าวคือ ไม่มีการเปลี่ยนสถานะจากสถานะใดสถานะหนึ่ง) ในกรณีนี้ ฝ่ายป้องกันจะเป็นฝ่ายชนะ${\displaystyle (p,q)}$
• เกมดำเนินต่อไปเรื่อยๆ ไม่มีวันจบ ในกรณีนั้นฝ่ายรับจะเป็นผู้ชนะ
• เกมจะดำเนินไปถึงสถานะที่เคยเล่นมาแล้ว ซึ่งเทียบเท่ากับการเล่นแบบไม่สิ้นสุด และถือเป็นชัยชนะของฝ่ายป้องกัน${\displaystyle (p,q)}$

ตามคำจำกัดความข้างต้น ระบบจะเป็นการจำลองแบบสองด้าน (bisimulation) ก็ต่อเมื่อมีกลยุทธ์ที่ทำให้ฝ่ายป้องกันชนะเท่านั้น

การจำลองแบบคู่สำหรับระบบการเปลี่ยนสถานะเป็นกรณีพิเศษของการจำลองแบบคู่เชิงโคอัลจีบรา สำหรับ ฟังก์ชัน กำลังเซตแบบโคแวเรียนต์ โปรดทราบว่าระบบการเปลี่ยนสถานะทุกระบบสามารถแมปแบบหนึ่งต่อหนึ่งไปยังฟังก์ชันจากไปยังกำลังเซตของที่มีดัชนีโดยเขียนเป็น ซึ่งกำหนดโดย ${\displaystyle (S,\Lambda ,\rightarrow )}$${\displaystyle \xi _{\rightarrow }}$${\displaystyle S}$${\displaystyle S}$${\displaystyle \Lambda }$${\displaystyle {\mathcal {P}}(\Lambda \times S)}$$${\displaystyle p\mapsto \{(\lambda ,q)\in \Lambda \times S:p{\overset {\lambda }{\rightarrow }}q\}.}$$

ให้เป็นการฉายภาพที่ n ซึ่งแมป ไปยังและตามลำดับสำหรับ; และ ภาพส่งต่อของที่กำหนดโดยการตัดส่วนประกอบที่สามออก โดยที่เป็นเซตย่อยของ ในทำนองเดียวกันสำหรับ ${\displaystyle \pi _{i}\colon S\times S\to S}$${\displaystyle i}$${\displaystyle (p,q)}$${\displaystyle p}$${\displaystyle q}$${\displaystyle i=1,2}$${\displaystyle {\mathcal {P}}(\Lambda \times \pi _{1})}$${\displaystyle \pi _{1}}$$${\displaystyle P\mapsto \{(\lambda ,p)\in \Lambda \times S:\exists q.(\lambda ,p,q)\in P\}}$$${\displaystyle P}$${\displaystyle \Lambda \times S\times S}$${\displaystyle {\mathcal {P}}(\Lambda \times \pi _{2})}$

โดยใช้สัญลักษณ์ข้างต้น ความสัมพันธ์จะเป็นการจำลองแบบคู่บนระบบการเปลี่ยนสถานะก็ต่อเมื่อมีระบบการเปลี่ยนสถานะบนความสัมพันธ์นั้น อยู่ ซึ่ง แผนภาพ จะเป็นไปตามเงื่อนไข ดังกล่าว${\displaystyle R\subseteq S\times S}$${\displaystyle (S,\Lambda ,\rightarrow )}$${\displaystyle \gamma \colon R\to {\mathcal {P}}(\Lambda \times R)}$${\displaystyle R}$

สลับตำแหน่งกันได้ กล่าวคือ สำหรับสมการ จะเป็นจริง โดยที่คือการแสดงฟังก์ชันของ ${\displaystyle i=1,2}$$${\displaystyle \xi _{\rightarrow }\circ \pi _{i}={\mathcal {P}}(\Lambda \times \pi _{i})\circ \gamma }$$${\displaystyle \xi _{\rightarrow }}$${\displaystyle (S,\Lambda ,\rightarrow )}$

ในบริบทพิเศษ แนวคิดของการจำลองแบบคู่ขนานบางครั้งได้รับการปรับปรุงโดยการเพิ่มข้อกำหนดหรือข้อจำกัดเพิ่มเติม ตัวอย่างเช่นการจำลองแบบคู่ขนานแบบกระตุกซึ่งการเปลี่ยนผ่านหนึ่งครั้งของระบบหนึ่งอาจจับคู่กับการเปลี่ยนผ่านหลายครั้งของอีกระบบหนึ่งได้ โดยมีเงื่อนไขว่าสถานะระหว่างกลางต้องเทียบเท่ากับสถานะเริ่มต้น ("กระตุก") ^{[ 4 ]}

รูปแบบที่แตกต่างออกไปจะถูกนำมาใช้หากระบบการเปลี่ยนสถานะรวมถึงแนวคิดของการกระทำเงียบ (หรือภายใน ) ซึ่งมักจะแสดงด้วย เช่น การกระทำที่ไม่สามารถมองเห็นได้โดยผู้สังเกตภายนอก ในกรณีนี้ การจำลองแบบคู่ (bisimulation) สามารถผ่อนคลายลงเป็นการจำลองแบบคู่ที่อ่อน (weak bisimulation ) ซึ่งหากสถานะสองสถานะและมีความคล้ายคลึงกันแบบคู่ (bisimilar) และมีการกระทำภายในจำนวนหนึ่งที่นำจาก ไปยังสถานะใดสถานะหนึ่งก็จะต้องมีสถานะ อยู่เช่นกันที่มีการกระทำภายในจำนวนหนึ่ง (อาจเป็นศูนย์) ที่นำจาก ไปยังความสัมพันธ์บนกระบวนการเป็นการจำลองแบบคู่ที่อ่อนหากเงื่อนไขต่อไปนี้เป็นจริง (โดยที่และเป็นการเปลี่ยนสถานะที่สังเกตได้และเงียบตามลำดับ): ${\displaystyle \tau }$${\displaystyle p}$${\displaystyle q}$${\displaystyle p}$${\displaystyle p'}$${\displaystyle q'}$${\displaystyle q}$${\displaystyle q'}$${\displaystyle {\mathcal {R}}}$${\displaystyle {\mathcal {S}}\in \{{\mathcal {R}},{\mathcal {R}}^{-1}\}}$${\displaystyle a,\tau }$

$${\displaystyle \forall p,q.\quad (p,q)\in {\mathcal {S}}\Rightarrow p{\stackrel {\tau }{\rightarrow }}p'\Rightarrow \exists q'.\quad q{\stackrel {\tau ^{\ast }}{\rightarrow }}q'\wedge (p',q')\in {\mathcal {S}}}$$$${\displaystyle \forall p,q.\quad (p,q)\in {\mathcal {S}}\Rightarrow p{\stackrel {a}{\rightarrow }}p'\Rightarrow \exists q'.\quad q{\stackrel {\tau ^{\ast }a\tau ^{\ast }}{\rightarrow }}q'\wedge (p',q')\in {\mathcal {S}}}$$

สิ่งนี้มีความเกี่ยวข้องอย่างใกล้ชิดกับแนวคิดของการจำลองแบบคู่ " จนถึง " ความสัมพันธ์^{[ 5 ]}

โดยทั่วไป หากระบบการเปลี่ยนสถานะให้ความหมายเชิงปฏิบัติการของภาษาโปรแกรมแล้ว คำจำกัดความที่แม่นยำของบิซิมูเลชันจะขึ้นอยู่กับข้อจำกัดของภาษาโปรแกรมนั้นๆ ดังนั้น โดยทั่วไปแล้ว อาจมีความสัมพันธ์แบบบิซิมูเลชัน (หรือบิซิมิลาริตี) มากกว่าหนึ่งประเภท ขึ้นอยู่กับบริบท

เนื่องจากแบบจำลอง Kripkeเป็นกรณีพิเศษของระบบการเปลี่ยนสถานะ (ที่มีป้ายกำกับ) การจำลองแบบคู่จึงเป็นหัวข้อหนึ่งในตรรกศาสตร์เชิงโมดอลด้วย อันที่จริง ตรรกศาสตร์เชิงโมดอลเป็นส่วนหนึ่งของตรรกศาสตร์ลำดับที่หนึ่งที่ไม่เปลี่ยนแปลงภายใต้การจำลองแบบคู่ ( ทฤษฎีบทของ van Benthem )

การตรวจสอบว่าระบบการเปลี่ยนผ่านแบบจำกัดสองระบบมีความคล้ายคลึงกันแบบไบซิมิลาร์สามารถทำได้ในเวลาพหุนาม [ ^{6 ] อั}ลกอริทึมที่เร็วที่สุดใช้เวลากึ่งเชิงเส้น โดย ใช้การปรับปรุงพาร์ติชันผ่านการลดปัญหาพาร์ติชันที่ หยาบที่สุด

• การสั่งซื้อล่วงหน้าสำหรับการจำลอง
• ความสัมพันธ์ที่สอดคล้องกัน
• การจำลองแบบความน่าจะเป็น

หมายเหตุ

เอกสารอ้างอิง

• CADP : เครื่องมือสำหรับลดขนาดและเปรียบเทียบระบบสถานะจำกัดตามการจำลองแบบต่างๆ
• mCRL2 : เครื่องมือสำหรับย่อและเปรียบเทียบระบบสถานะจำกัดตามการจำลองแบบต่างๆ
• เกมจำลองชีวภาพ