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

ระบบการเปลี่ยนสถานะสอดคล้องทางคณิตศาสตร์กับระบบการเขียนใหม่แบบนามธรรม (ดังที่อธิบายเพิ่มเติมในบทความนี้) และกราฟแบบมีทิศทางแต่แตกต่างจากออโตมาตาแบบสถานะจำกัดในหลายด้าน:

• เซตของสถานะต่างๆ ไม่จำเป็นต้องมีจำนวนจำกัด หรือแม้แต่สามารถนับได้
• เซตของการเปลี่ยนสถานะไม่จำเป็นต้องมีจำนวนจำกัด หรือแม้กระทั่งนับได้
• ไม่มีการระบุสถานะ "เริ่มต้น" หรือสถานะ "สุดท้าย"

ระบบการเปลี่ยนสถานะสามารถแสดงได้ในรูปกราฟแบบมีทิศทาง

ในทางทฤษฎีระบบการเปลี่ยนสถานะคือคู่โดยที่เป็นเซตของสถานะ และความสัมพันธ์การเปลี่ยนสถานะเป็นเซตย่อยของเรากล่าวว่ามีการเปลี่ยนสถานะจากสถานะไปยังสถานะถ้า และ เรา ใช้สัญลักษณ์ แทน${\displaystyle (S,T)}$${\displaystyle S}$${\displaystyle T}$${\displaystyle S\times S}$${\displaystyle p}$${\displaystyle q}$${\displaystyle (p,q)\in T}$${\displaystyle p\rightarrow q}$

ระบบการเปลี่ยนสถานะแบบมีป้ายกำกับคือทูเปิลโดยที่คือเซตของสถานะคือเซตของป้ายกำกับ และคือความสัมพันธ์การเปลี่ยนสถานะแบบมีป้ายกำกับ ซึ่ง เป็นเซตย่อยของเรากล่าวว่ามีการเปลี่ยนสถานะจากสถานะหนึ่งไปยังอีกสถานะหนึ่งด้วยป้ายกำกับก็ต่อเมื่อและใช้สัญลักษณ์ แทน ${\displaystyle (S,\Lambda ,T)}$${\displaystyle S}$${\displaystyle \Lambda }$${\displaystyle T}$${\displaystyle S\times \Lambda \times S}$${\displaystyle p}$${\displaystyle q}$${\displaystyle \alpha }$${\displaystyle (p,\alpha ,q)\in T}$

${\displaystyle p\xrightarrow {\alpha } q\,.}$

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

• ถ้าสำหรับและ ใดๆ ที่กำหนดให้ มีเพียงคู่ลำดับเดียวในแล้วเราจะกล่าวว่าเป็นแบบกำหนดได้ (สำหรับ)${\displaystyle p}$${\displaystyle \alpha }$${\displaystyle (p,\alpha ,q)}$${\displaystyle T}$${\displaystyle \alpha }$${\displaystyle p}$
• ถ้าสำหรับและ ที่กำหนดใดๆ มีอย่างน้อยหนึ่งทูเปิลในแล้วเราจะกล่าวว่าสามารถดำเนินการได้ (สำหรับ)${\displaystyle p}$${\displaystyle \alpha }$${\displaystyle (p,\alpha ,q)}$${\displaystyle T}$${\displaystyle \alpha }$${\displaystyle p}$

นิยามอย่างเป็นทางการสามารถเขียนใหม่ได้ดังนี้ ระบบการเปลี่ยนสถานะที่มีป้ายกำกับบน ที่มีป้ายกำกับจากสอดคล้องกันแบบหนึ่งต่อหนึ่งกับฟังก์ชันโดยที่ คือ ฟังก์ชันกำลังเซต (แบบแปรผันร่วม) ภายใต้การจับคู่แบบหนึ่งต่อหนึ่งนี้จะถูกส่งไปยังซึ่งกำหนดโดย ${\displaystyle S}$${\displaystyle \Lambda }$${\displaystyle S\to {\mathcal {P}}(\Lambda \times S)}$${\displaystyle {\mathcal {P}}}$${\displaystyle (S,\Lambda ,T)}$${\displaystyle \xi _{T}:S\to {\mathcal {P}}(\Lambda \times S)}$

${\displaystyle p\mapsto \{\,(\alpha ,q)\in \Lambda \times S\mid p\xrightarrow {\alpha } q\,\}}$.

กล่าวอีกนัยหนึ่ง ระบบการเปลี่ยนสถานะที่มีป้ายกำกับคือโคอัลจีบราสำหรับ ฟังก์ชัน${\displaystyle P(\Lambda \times {-})}$

มีความสัมพันธ์มากมายระหว่างแนวคิดเหล่านี้ บางอย่างก็เรียบง่าย เช่น การสังเกตว่าระบบการเปลี่ยนสถานะที่มีป้ายกำกับซึ่งชุดของป้ายกำกับประกอบด้วยองค์ประกอบเพียงหนึ่งเดียวจะเทียบเท่ากับระบบการเปลี่ยนสถานะที่ไม่มีป้ายกำกับ อย่างไรก็ตาม ความสัมพันธ์เหล่านี้ไม่ได้เรียบง่ายเท่ากันทั้งหมด

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

ในการตรวจสอบแบบจำลองบางครั้งระบบการเปลี่ยนสถานะจะถูกกำหนดให้รวมฟังก์ชันการติดป้ายเพิ่มเติมสำหรับสถานะต่างๆ ด้วย ส่งผลให้เกิดแนวคิดที่ครอบคลุม โครงสร้าง ของKripke ^{[ 3 ]}

ภาษาการกระทำเป็นส่วนขยายของระบบการเปลี่ยนผ่าน โดยเพิ่มชุดของฟลูเอนท์Fชุดของค่าVและฟังก์ชันที่แมปF × SไปยังV ^{[ 4 ]}

• ความสัมพันธ์แบบไบนารี
• ความสัมพันธ์สามฝ่าย
• โมโนอิดทรานซิชัน
• โมโนอิดการแปลง
• การกระทำของกลุ่มย่อย
• การสั่งซื้อล่วงหน้าสำหรับการจำลอง
• การจำลองแบบไบซิเมชั่น
• ความหมายเชิงปฏิบัติการ
• โครงสร้างของคริปเก้
• เครื่องจักรสถานะจำกัด
• แคลคูลัส μ แบบโมดอล