شهدت السنوات الأخيرة اهتماماً متزايداً بتعريف نماذج من الآلات المتحكمة مدعمة بمفهوم الزمن. فعلى سبيل المثال، تم تقديم الآلات الزمنية كآلات موسعة بساعات زمنية. في هذا البحث، ندرس نماذج من آلات الحالات المحدودة الزمنية (TFSMs)، أي آلات الحالات المحدودة المدعمة بالزمن، والتي تقبل كلمات إدخال زمنية وتنتج كلمات إخراج زمنية. نناقش هنا بعض نماذج TFSMs بساعة واحدة: آلات الحالات المحدودة الزمنية ذات الحراس الزمنيين، وآلات الحالات المحدودة الزمنية ذات مهلات الانتظار (Timeouts)، وآلات الحالات المحدودة الزمنية التي تجمع بين الحراس الزمنيين والمهلات. نقوم بحل مسألة التحقق من التكافؤ لجميع النماذج الثلاثة، ونقارن بين قوة تعبيرها، ونحدد الفئات الفرعية من آلات الحالات المحدودة الزمنية ذات الحراس الزمنيين وتلك ذات المهلات التي تكون متكافئة مع بعضها البعض.
تُعد الآلات المحدودة (FA) وآلات الحالات المحدودة (FSMs) نماذجاً شكلية واسعة الاستخدام في الهندسة والعلوم، على سبيل المثال في مجالات تتراوح بين الدوائر التسلسلية، وبروتوكولات الاتصال، والأنظمة المدمجة والتفاعلية، إلى النمذجة الحيوية.
منذ تسعينيات القرن الماضي، تم إثراء الفئات القياسية للآلات المحدودة بإدخال قيود زمنية لتمثيل سلوك الأنظمة في الزمن المتقطع أو المستمر بشكل أكثر دقة. وتُعد الآلات الزمنية (TA) مثالاً على ذلك: فهي آلات محدودة مدعمة بعدد من الساعات الزمنية الحقيقية القابلة لإعادة الضبط، حيث يتم تفعيل الانتقالات بناءً على شروط تتعلق بقيم الساعات .
ومؤخراً، تم اقتراح نماذج زمنية لآلات الحالات المحدودة في الأدبيات من خلال إدخال قيود زمنية مثل الحراس الزمنيين أو المهلات. الحراس الزمنيون يقيدون انتقالات الإدخال/الإخراج لتحدث ضمن فترات زمنية معينة. على وجه الخصوص، يتميز نموذج آلة الحالات المحدودة الزمنية المقترح في بما يلي: متغير ساعة واحد، وقيود زمنية لتحديد الزمن المنقضي في الحالة، وإعادة ضبط الساعة عند تنفيذ الانتقال.
أما نموذج آلة الحالات المحدودة الزمنية المقترح في فيتميز بوجود متغير ساعة واحد، وقيود زمنية لتحديد الزمن المنقضي عند الحاجة لإنتاج إخراج بعد تطبيق إدخال على الآلة، وإعادة ضبط الساعة عند إنتاج الإخراج، بالإضافة إلى المهلات. ومعنى المهلات هو: إذا لم يتم تطبيق أي إدخال في الحالة الحالية خلال فترة المهلة، تنتقل الآلة من الحالة الحالية إلى حالة أخرى باستخدام دالة المهلة؛ على سبيل المثال، المهلات شائعة في بروتوكولات وأنظمة الاتصالات.
تُستخدم الآلات الزمنية وآلات الحالات المحدودة الزمنية أيضاً عند اشتقاق اختبارات للأنظمة الحدثية المتقطعة. ومع ذلك، فإن طرق اشتقاق مجموعات اختبارات منتهية وكاملة مع ضمان تغطية الأخطاء متوفرة فقط لآلات الحالات المحدودة الزمنية، ولذلك تُفضل هذه الآلات على الآلات الزمنية وغيرها من النماذج عندما يكون اشتقاق اختبارات كاملة مطلوباً.
في هذا البحث، ندرس بعض نماذج آلات الحالات المحدودة الزمنية بساعة واحدة: آلات الحالات المحدودة الزمنية ذات الحراس الزمنيين فقط، وآلات الحالات المحدودة الزمنية ذات المهلات فقط، وآلات الحالات المحدودة الزمنية التي تجمع بين الحراس الزمنيين والمهلات. نقوم بحل مسألة التحقق من التكافؤ لجميع النماذج الثلاثة، ونقارن بين قوة تعبيرها، ونحدد الفئات الفرعية من آلات الحالات المحدودة الزمنية ذات الحراس الزمنيين وتلك ذات المهلات التي تكون متكافئة مع بعضها البعض. تم الحصول على هذه النتائج من خلال تقديم علاقات محاكاة متبادلة (bisimulation) تُعرّف آلات حالات محدودة غير زمنية تشمل حالاتُها معلومات عن مناطق الساعة. وهذا يذكرنا ببناء رسم المناطق (region graph) المستخدم لإثبات أن مسائل التحقق في الآلات الزمنية (مثل الخصائص الأمنية) لها نفس الإجابة لجميع تقييمات الساعة في نفس المنطقة . في حالتنا، نستطيع إثبات نتيجة أقوى: سلوك آلتين زمنيتين متكافئ إذا وفقط إذا كان سلوك الآلتين غير الزمنيتين المرافقتين متكافئاً. وهكذا، تحقق نماذجنا من آلات الحالات المحدودة الزمنية توازناً جيداً بين قوة التعبير والتعقيد الحسابي.
ليكن \(A\) أبجدية منتهية، ولتكن \(\mathbb{R}^+\) مجموعة الأعداد الحقيقية غير السالبة. يُسمى الرمز الزمني زوجاً \((a,t)\) حيث \(t \in \mathbb{R}^+\) هو الطابع الزمني للرمز \(a\in A\). تُعرّف الكلمة الزمنية بأنها تسلسل منتهٍ \((a_1,t_1)(a_2,t_2)(a_3,t_3)\dots\) من الرموز الزمنية حيث تسلسل الطوابع الزمنية \(t_1 t_2 t_3 \dots\) متزايد. جميع النماذج الزمنية المدروسة في هذا البحث هي آلات إدخال/إخراج تعمل بقراءة كلمة إدخال زمنية \((i_1,t_1)(i_2,t_2)\dots(i_k,t_k)\) معرفة على أبجدية إدخال \(I\)، وتنتج كلمة إخراج زمنية مقابلة \((o_1,t_1)\) \((o_2,t_2)\dots(o_k,t_k)\) على أبجدية إخراج \(O\). يُفترض أن إنتاج الإخراجات لحظي: الطابع الزمني للإخراج \(o_j\) هو نفسه طابع الإدخال \(i_j\). النماذج التي يوجد فيها تأخير بين قراءة الإدخال وإنتاج الإخراج ممكنة ولكنها غير مدروسة هنا. إذا أعطيت كلمة زمنية \((a_1,t_1)(a_2,t_2)\dots(a_k,t_k)\)، فإن \(\mathop{\mathrm{Untime}}((a_1,t_1)(a_2,t_2)\dots(a_k,t_k)) = a_1 a_2 \dots a_k\) تمثل الكلمة الناتجة بعد حذف الطوابع الزمنية.
آلة الحالات المحدودة الزمنية (TFSM) قد تكون غير حتمية وجزئية، وهي آلة حالات محدودة مدعمة بساعة زمنية. الساعة هي عدد حقيقي يقيس التأخير الزمني في الحالة، وتُعاد إلى الصفر عند تنفيذ الانتقال. في هذا القسم، نقدم أولاً نموذج TFSM مع الحراس الزمنيين كما في ونموذج TFSM مع المهلات كما في . ثم نعرّف نموذج TFSM يجمع بين الحراس الزمنيين والمهلات ويحتوي النماذج الأخرى. بالإضافة إلى ذلك، ندرس مسألة التكافؤ لكل من النماذج الثلاثة.
يُعرّف الحارس الزمني الفترة الزمنية التي يمكن فيها تنفيذ الانتقال. بشكل حدسي، إذا كانت الآلة في الحالة \(s\) وتستقبل الإدخال \(i\) عند الزمن \(t\) الذي يحقق الحارس الزمني، فإنها تستجيب بالإخراج \(o\) وتنتقل إلى الحالة التالية \(s'\)، مع إعادة ضبط الساعة إلى الصفر وبدء تقدمها في الحالة \(s'\).
تعريف 1 (TFSM مع الحراس الزمنيين ). TFSM مع الحراس الزمنيين هو خماسية \(M = (S, I, O, \lambda_S, s_0)\) حيث \(S\)، \(I\)، و\(O\) مجموعات منتهية منفصلة وغير فارغة من الحالات، والإدخالات، والإخراجات على التوالي، \(s_0\) هي الحالة الابتدائية، \(\lambda_S \subseteq S \times I \times \Pi \times O \times S\) هي علاقة الانتقال حيث \(\Pi\) هي مجموعة الحراس الزمنيين للإدخال. كل حارس في \(\Pi\) هو فترة \(g = \langle t_{min}, t_{max} \rangle\) حيث \(t_{min}\) عدد صحيح غير سالب، و\(t_{max}\) إما عدد صحيح غير سالب أو \(\infty\)، \(t_{min} \leq t_{max}\)، و\(\langle \in \{ (, [ \}\) بينما \(\rangle \in \{ ), ] \}\).
الحالة الزمنية للآلة هي زوج \((s,x)\) حيث \(s \in S\) حالة من \(M\) و\(x \in \mathbb{R}^+\) هو القيمة الحالية للساعة. الانتقالات بين الحالات الزمنية نوعان:
المسار الزمني لآلة الحالات المحدودة الزمنية مع الحراس الزمنيين \(M\) يتناوب بين الانتقالات الزمنية وانتقالات الإدخال/الإخراج. إذا أعطيت كلمة إدخال زمنية \(v = (i_1,t_1)(i_2,t_2)\dots(i_k,t_k)\)، فإن المسار الزمني لـ\(M\) على \(v\) هو تسلسل منتهٍ \(\rho = (s_0,0) \xrightarrow{t_1} (s_0,t_1) \xrightarrow{i_1,o_1} (s_1,0) \xrightarrow{t_2-t_1} (s_1,t_2-t_1) \xrightarrow{i_2,o_2} (s_2,0) \xrightarrow{t_3-t_2} \dots \xrightarrow{i_k,o_k} (s_k,0)\) بحيث \(s_0\) هي الحالة الابتدائية، ولكل \(j \geq 0\) \((s_j,0) \xrightarrow{t_{j+1}-t_j} (s_j,t_{j+1}-t_j) \xrightarrow{i_{j+1},o_{j+1}} (s_{j+1},0)\) هو تسلسل صحيح من الانتقالات. يُقال إن المسار الزمني \(\rho\) يقبل كلمة الإدخال الزمنية \(v= (i_1,t_1)(i_2,t_2)\dots(i_k,t_k)\) وينتج كلمة الإخراج الزمنية \(u = (o_1,t_1)(o_2,t_2)\dots(o_k,t_k)\). يُعرّف سلوك \(M\) من خلال كلمات الإدخال/الإخراج التي تقبلها وتنتجها الآلة.
تعريف 2. سلوك آلة الحالات المحدودة الزمنية \(M\) هو دالة جزئية \(B_M: (I\times \mathbb{R})^* \mapsto 2^{(O\times \mathbb{R})^*}\) تربط كل كلمة إدخال \(w\) مقبولة من \(M\) بمجموعة كلمات الإخراج \(B_M(w)\) التي تنتجها \(M\) تحت الإدخال \(w\). إذا كانت \(M\) آلة غير زمنية، يُعرّف السلوك كدالة جزئية \(B_M: I^* \mapsto 2^{O^*}\).
تُعتبر آلتان \(M\) و\(M'\) لهما نفس أبجديات الإدخال والإخراج متكافئتين إذا وفقط إذا كان لهما نفس السلوك، أي \(B_M = B_{M'}\).
يمكن تعميم التعاريف المعتادة للآلات المحدودة (الحتمية، غير الحتمية، الآلة الجزئية، إلخ) على جميع نماذج آلات الحالات المحدودة الزمنية المدروسة هنا. على وجه الخصوص، تكون الآلة كاملة إذا كان لكل حالة \(s\)، ولكل إدخال \(i\)، ولكل قيمة للساعة \(x\) يوجد على الأقل انتقال واحد \((s,x) \xrightarrow{i,o} (s',0)\)، وإلا فهي جزئية. وتكون الآلة حتمية إذا كان لكل حالة \(s\)، ولكل إدخال \(i\)، ولكل قيمة للساعة \(x\) يوجد على الأكثر انتقال إدخال/إخراج واحد، وإلا فهي غير حتمية.
لأغراض التبسيط، سنقتصر من الآن فصاعداً على دراسة الآلات الكاملة والحتمية، ونترك معالجة الآلات الجزئية وغير الحتمية لأعمال مستقبلية. عندما تكون الآلة \(M\) حتمية وكاملة، يكون \(B_M(w)\) مجموعة أحادية لكل كلمة إدخال \(w\). لذا يمكننا إعادة تعريف السلوك \(B_M\) كدالة \(B_M: (I\times \mathbb{R})^* \mapsto (O\times \mathbb{R})^*\) تربط كل كلمة إدخال \(w = (i_1,t_1)(i_2,t_2)\dots(i_k,t_k)\) بكلمة الإخراج الوحيدة \(B_M(w)\) التي تنتجها \(M\) تحت الإدخال \(w\).
علاوة على ذلك، يمكننا اعتبار علاقة الانتقال للآلة كدالة كاملة \(\lambda_S: S \times I \times \mathbb{R}^+ \mapsto S \times O\) تأخذ كمدخل الحالة الحالية \(s\)، والتأخير \(t\)، ورمز الإدخال \(i\) وتنتج الحالة التالية والإخراج \(\lambda_S(s,t,i) = (s',o)\) بحيث \((s,0)\xrightarrow{t}(s,t)\xrightarrow{i,o}(s',0)\). مع بعض التجاوز في الترميز، يمكننا تعميمها إلى دالة \(\lambda_S: S \times (I \times \mathbb{R}^+)^* \mapsto S \times O^*\) تأخذ كمدخل الحالة الابتدائية \(s\) وكلمة زمنية \(w\)، وتعيد الحالة التي تصل إليها الآلة بعد قراءة \(w\) وكلمة الإخراج الناتجة. سنستخدم الترميز \(s \xrightarrow{w,u} s'\) اختصاراً لـ\(\lambda_S(s,w) = (s',u)\).
في هذا القسم نوضح كيفية حل مسألة التكافؤ لآلات الحالات المحدودة الزمنية مع الحراس الزمنيين عن طريق اختزالها إلى مسألة التكافؤ لآلات الحالات المحدودة غير الزمنية. نقوم بذلك عبر ثلاث خطوات: أولاً، نبين كيفية بناء آلة حالات محدودة "مجردة" من آلة الحالات المحدودة الزمنية مع الحراس؛ ثم نعرّف مفهوماً مناسباً للمحاكاة المتبادلة (bisimulation) لمقارنة آلات الحالات المحدودة الزمنية مع الحراس مع الآلات غير الزمنية؛ وأخيراً، نستنتج من خصائص علاقة المحاكاة المتبادلة أن آلتين مع الحراس الزمنيين متكافئتان إذا وفقط إذا كان تجريدهما متكافئاً.
الآن، لنفترض أن \(M\) آلة حالات محدودة زمنية مع الحراس. نعرّف \(\max(M)\) بأنه أكبر ثابت صحيح (مختلف عن \(\infty\)) يظهر في الحراس في \(\lambda_S\). لأي عدد طبيعي \(N \geq \max(M)\)، نعرّف \(\mathbb{I}_N\) كمجموعة الفترات \(\mathbb{I}_N = \{[n,n] \mid n \leq N\} \cup \{(n,n+1) \mid 0 \leq n < N\} \cup \{(N,\infty)\}\). التجريد المتقطع لآلة الحالات المحدودة الزمنية مع الحراس سيأخذ كمدخل أزواجاً من الشكل \((i,\langle n,n'\rangle)\) حيث \(i\) هو الإدخال الفعلي و\(\langle n,n'\rangle \in \mathbb{I}_N\) فترة تمثل التأخير الزمني.
تعريف 3. إذا كانت \(M = (S, I, O, \lambda_S, s_0)\) آلة حالات محدودة زمنية مع الحراس، و\(N \geq \max(M)\) عدداً طبيعياً، فإن آلة الحالات المحدودة المجردة \(A^N_M = (S, I\times \mathbb{I}_N, O, \lambda_A, s_0)\) هي آلة غير زمنية بحيث \((s, (i,\langle n,n'\rangle), o, s') \in \lambda_A\) إذا وفقط إذا \((s, i, \langle t,t'\rangle, o, s') \in \lambda_S\) لبعض الحارس \(\langle t,t'\rangle\) بحيث \(\langle n,n'\rangle \subseteq \langle t,t'\rangle\).
لا يمكننا مقارنة سلوك آلة الحالات المحدودة الزمنية مباشرة مع سلوك تجريدها غير الزمني، لأن الأولى تقبل كلمات إدخال زمنية على \(I\) والثانية تقبل كلمات إدخال غير زمنية على \(I \times \mathbb{I}_N\). لذلك، نحتاج لتعريف مفهوم تجريد الكلمة الزمنية.
تعريف 4. إذا كانت \(A\) أبجدية منتهية، و\(v = (a_1,t_1)(a_2,t_2)(a_3,t_3)\dots(a_m,t_m)\) كلمة زمنية منتهية، و\(N\) عدداً صحيحاً، و\(\mathbb{I}_N\) مجموعة الفترات، فإن تجريدها \(\mathbb{I}_N\) هو الكلمة \(\mathbb{I}_N(v) = (a_1,\langle n_1,n_1'\rangle)(a_2,\langle n_2,n_2'\rangle)\ldots(a_m,\langle n_m,n_m'\rangle)\) بحيث \(t_i - t_{i-1} \in \langle n_i,n_i'\rangle\) لكل \(1 \leq i \leq m\).
تربط المحاكاة المتبادلة \(\mathbb{I}_N\) حالات آلة الحالات المحدودة الزمنية مع حالات آلة غير زمنية.
تعريف 5. إذا كانت \(T = (S, I, O, \lambda_S, s_0)\) آلة حالات محدودة زمنية مع الحراس، و\(U = (R, I\times \mathbb{I}_N, O, \lambda_R, r_0)\) آلة غير زمنية، و\(N \geq \max(T)\)، و\(\mathbb{I}_N\) مجموعة الفترات، فإن محاكاة متبادلة \(\mathbb{I}_N\) هي علاقة \(\sim \subseteq S \times R\) تحقق الشروط التالية:
تُسمى \(T\) و\(U\) متشابهتين بمحاكاة متبادلة \(\mathbb{I}_N\) إذا وجدت علاقة محاكاة متبادلة \(\sim \subseteq S \times R\) بحيث \(s_0 \sim r_0\).
الآلات المتشابهة بمحاكاة متبادلة \(\mathbb{I}_N\) لها نفس السلوك، كما يثبت ذلك رسمياً في اللمّة التالية.
لمّة 1. إذا كانت \(T = (S, I, O, \lambda_S, s_0)\) آلة حالات محدودة زمنية مع الحراس، و\(U = (R, I\times \mathbb{I}_N, O, \lambda_R, r_0)\) آلة غير زمنية، ووجدت علاقة محاكاة متبادلة \(\mathbb{I}_N\) \(\sim\) بحيث \(s_0 \sim r_0\)، فعندئذ لكل كلمة إدخال زمنية \(v = (i_1,t_1)(i_2,t_2)(i_3,t_3)\dots(i_m,t_m)\) لدينا \(\mathop{\mathrm{Untime}}(B_T(v)) = B_U(\mathbb{I}_N(v))\).