نظام حالة الانتقال

يعرّف نظام حالة انتقال في المعلوماتية النظرية على أنه آلة افتراضية تستخدم في الاحتساب. تحتوي هذه الآلة على مجموعة من الحالات والانتقالات بين هذه الحالات، من الممكن تعريف مجموعة من العناوين وعنونة الانتقالات بها، من الممكن أن يستخدم العنوان لأكثر من انتقال واحد. لا يتم عنونة النظام في حال احتوت مجموعة العناوين على عنصر واحد فقط، ومن الممكن استخدام تعريف بسيط للنظام يتم به حذف العناوين.

تتطابق أنظمة حالة انتقال رياضيات مع أنظمة إعادة الكتابة المجردة. بالمقابل فهي تختلف عن أوتومات الحالة المنتهية بعدة أمور:

• ليس من الضروري أن تكون مجموعة الحالات منتهيةً، أو حتى قابلةً للعد في أنظمة حالة-انتقال.
• ليس من الضروري أن تكون مجموعة الانتقالات منتهيةً، أو حتى قابلةً للعد في أنظمة حالة-انتقال.
• في أوتومات الحالة المنتهية يتم التمييز بين حالة «بداية» وحيدة، ومجموعة من حالات «النهاية».

من الممكن تمثيل نظام حالة-انتقال كـبيان موجه.

تعريف المصطلح

من الناحية الرسمية، فإن النظام الانتقالي هو زوج (S, →) حيث S هي مجموعة من الحالات و → هي علاقة انتقالات الحالة (أي مجموعة فرعية من S × S). يتم كتابة الانتقال من الحالة p إلى الحالة q، أي (p, q) ∈ →، على النحو p → q.

نظام الانتقال المسمى الصف هو (S, Λ, →) حيث S هي مجموعة من الحالات، Λ هي مجموعة من التسميات و → هي علاقة بالتحولات المسمى (أي مجموعة فرعية من S × Λ × S). (p,α,q) ∈ → مكتوب على النحو:

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

ويمثل الانتقال من الحالة p إلى الحالة q مع التسمية α. يمكن أن تمثل التصنيفات أشياء مختلفة اعتمادًا على اللغة محل الاهتمام. تتضمن الاستخدامات النموذجية للعلامات تمثيل المدخلات المتوقعة، أو الشروط التي يجب أن تكون صحيحة لبدء النقل، أو الإجراءات التي يتم تنفيذها أثناء النقل. تم تقديم أنظمة الانتقال المسمى في الأصل كنظم انتقال مسماة.[1]

إذا، بالنسبة لأي p و α معين، لا يوجد سوى مجموعة واحدة (p ،α ،q) في →، ثم يقول أحدهم أن α حتمية (لـ p). في حالة وجود p و α معينين، يوجد على الأقل صف واحد (p,α,q) في →، ثم يقول أحدهم أن α قابل للتنفيذ (لـ p).

يمكن إعادة صياغة ذلك من حيث نظرية الفئات. كل نظام انتقال الحالة المسمى ${\displaystyle (S,\Lambda ,\rightarrow )}$ هي تقابل ${\displaystyle \xi _{\rightarrow }}$ من ${\displaystyle S}$ إلى المجموعة الجزئية ${\displaystyle S}$ مفهرسة بواسطة ${\displaystyle \Lambda }$ مكتوب كـ ${\displaystyle {\mathcal {P}}(\Lambda \times S)}$, معرفة بواسطة ${\displaystyle p\mapsto \{(\alpha ,q)\in \Lambda \times S:p{\overset {\alpha }{\rightarrow }}q\}.}$.

لذا فإن نظام الانتقال المسمى بالعلامة هو F-Coalgebra للممر ${\displaystyle P(\Lambda \times -)}$.

المراجع

1. M, KellerRobert (1 Jul 1976). "Formal verification of parallel programs". Communications of the ACM (بالإنجليزية). Archived from the original on 2020-05-22.